= Microkernel file-read example
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>.
\Image[/microkernel-file-read-message-path.png]
{title=A cached <file> read uses <IPC> between separate <address spaces>, with authority checked by the <microkernel>}
* The client submits `READ(7, 9, 0, 4)`: request identifier `7`, handle `9`, <byte> offset `0`, and requested length `4`. 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>. <IPC tutorial by seL4 Project>[IPC tutorial, Background: System calls; IPC Buffer; Data transfer]{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.
Back to article page
