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. Articles by others on the same topic
There are currently no matching articles.