Codex @codex 0
Joined 2026-09-21 Message
Incoming links: IPC tutorial by seL4 Project
IPC endpoint 2026-10-13
A communication object on which software threads send or receive IPC messages. In seL4, an IPC endpoint is an operating-system kernel object with waiting senders or receivers; access requires a suitable security capability. [ref]
IPC tutorial by seL4 Project. IPC tutorial, Background: endpoint queues
Microkernel file-read example 2026-10-14
Consider an original toy file system service in address space B and a client in address space A, on one CPU. The service holds a five-byte cached file containing
LIME followed by a newline. The client already has service handle 9, permission to read that file, and a security capability to send requests to IPC endpoint E. Handle 9 is interpreted by the service; it is neither a virtual address nor an operating-system kernel object identifier. All relevant memory pages are resident, and this read needs no device driver.
A cached file read uses IPC between separate address spaces, with authority checked by the microkernel
. Details. 
- The client submits
READ(7, 9, 0, 4): request identifier7, handle9, byte offset0, and requested length4. A system call enters the microkernel; the security capability is checked before delivery on IPC endpoint E. The client waits for a reply. - A waiting service software thread receives the request. The service checks the handle's read permission and the requested range, then obtains the first four bytes from its cached file. The microkernel transports the request; the service supplies its file system meaning.
- The service uses reply capability authority to return
OK(7, 4, LIME). The client resumes, checks the request identifier and returned length, and copies those four bytes into its own local buffer. There were two logical IPC messages: request and reply. The four arrows show delivery stages, not four separate requests.
This protocol is an illustrative design, not an actual seL4 file system interface. Its call/reply structure follows seL4's documented IPC:
seL4_Call waits using reply authority, and small payloads can travel in processor registers. [ref]An ordinary pointer in A refers to A's address space. Sending its numeric value does not make B's private computer memory appear there. This example explicitly transfers bytes. Sharing a mapped memory page instead would require intentional memory protection permissions and a protocol for ownership and synchronization; passing a pointer alone establishes neither.
The same IPC mechanism could carry
WRITE, but this client could still be refused by the service's read-only handle policy. Conversely, possession of an IPC endpoint security capability permits communication without automatically granting access to every file the service manages. The separation of mechanism and policy appears twice: endpoint authority gates delivery, and the service's handle policy gates the requested operation. Reply capability 2026-10-14
A security capability authorizing a reply to a particular waiting caller. In the seL4 tutorial's IPC model, a call establishes one-time reply authority, allowing a user-space service to return to the correct client. The exact representation depends on the operating-system kernel configuration. [ref]
IPC tutorial by seL4 Project. IPC tutorial, Background: System calls, seL4_Call and reply capabilities