IPC

Synchronous message passing modelled on classic (non-MCS) seL4: endpoints for rendezvous messages, notifications for asynchronous signals, an implicit per-thread reply slot for Call. This document is the contract the kernel tests and proofs check.

Objects

Endpoint. A rendezvous point. Holds a FIFO of blocked senders and a FIFO of blocked receivers; never both non-empty. Owned by its creator and destroyed with it.

Notification. A word of signal bits plus a FIFO of blocked waiters and at most one bound thread. Owned by its creator and destroyed with it.

Both are named by capabilities whose generation must match (see P2).

Capabilities

A capability to an endpoint or notification carries a badge (a word; 0 means unbadged). Mint copies a capability with narrower permissions and, for endpoints and notifications, a badge. A badge cannot be changed once set: a badged capability cannot be minted again.

Derivation and revocation

Every capability made from another (by Mint, Delegate or an IPC transfer) records it as its parent; capabilities the kernel creates directly have none. Revoke(cap) deletes every capability derived from cap, transitively and across processes, and keeps cap itself. Any holder may revoke, but only its own subtree.

Deleting a capability (DropCap, or its process dying) makes its parent adopt its children, so stepping out of the chain never shields anyone from a revocation further up.

A region mapping made with MapRegion(cap, va, perms) lasts only as long as cap: deleting or revoking cap unmaps it. perms needs Read, plus Write for read-write or Execute for read-execute. W^X holds across processes: while a region is mapped read-write anywhere it cannot be mapped read-execute anywhere, and the other way round (PermissionDenied). To load code, map it writable, fill it, drop that mapping, then map it executable.

Object	Permission	Allows
Endpoint	Execute	`Send`, `Call`
Endpoint	Read	`Receive`, `ReplyRecv`
Endpoint	Delegate	transfer a capability through it; `Mint`
Notification	Write	`Signal`
Notification	Read	`Wait`, `Poll`, `BindNotification`
Notification	Delegate	`Mint`
Interrupt	Execute	`SetIrqNotification`, `AckInterrupt`
Region	Read	`MapRegion` (read-only), `RegionAddress`
SystemControl	Execute	`Halt`

Boot authority

No process is privileged by its id. At boot the kernel gives init:

a ProcessCreate capability in slot 0;
for every device in the board table, a capability to its MMIO region (Read, Write, Delegate; never Execute) and, if it interrupts, one to its IRQ line (Execute, Delegate);
one SystemControl capability (Execute, Delegate);
one Console capability (Write, Delegate).

DebugPutchar(console, byte) needs a Console capability with Write; there is no other way to reach the UART. Init lends its console to the servers it starts (snake gets none). Until the log server owns the console, boot code also grants one to the servers it loads itself.

A thread made by SpawnThread/SpawnThreadIn starts with the caller's arg in a0. A process's first thread reads it as types::start_arg: the slots of the console and log capabilities it was handed.

The board capabilities come after the capabilities boot code hands out for the built-in servers, so those slots are unchanged. Device regions never overlap each other or the frame pool, and each device has exactly one region, so delegating or revoking it means the same thing everywhere.

RegionAddress(cap) returns a region's physical base so a driver can program a device's DMA; pool regions are physically contiguous.

Boot also maps one read-only page into init at types::bootinfo::BOOT_INFO_VA listing, for each board device, its kind, physical base, IRQ line and the slots holding its region and IRQ capabilities, plus the SystemControl and Console slots. It is the only page boot writes for userspace.

Devices

Init decides which driver gets which device: it asks each virtio slot for its device id (mapping a minted copy of the region capability, then dropping it), and hands the disk, GPU and keyboard (or, with no keyboard, the UART) to their drivers before anything else (libkos::device):

init Calls the driver's endpoint [SETUP, MMIO, kind] carrying the region capability, then [SETUP, IRQ] with the IRQ capability, then [SETUP, DONE]. A driver with no device gets only DONE.
The driver maps the region, allocates its own DMA memory (CreateRegion, MapRegion, RegionAddress) and resets the device.
A driver with an IRQ routes it to a notification bound to its thread (SetIrqNotification, BindNotification) and acknowledges once to arm it. Lines start masked, are masked again by the kernel on every interrupt, and are re-armed by AckInterrupt.

Messages

A message is 4 words and at most one capability. The capability is transferred only if the sender's endpoint capability has Delegate and the transferred capability itself has Delegate; it is copied (the sender keeps its own) with the same badge and permissions minus Delegate: the receiver can use it but not pass it on. To let a process pass a capability on, give it with the Delegate syscall and explicit rights. If the receiver's table is full, or the capability is no longer valid at delivery time, the message is delivered without it.

The receiver learns the badge of the capability the sender used. The kernel never reveals the sender's process or thread id.

Operations

Send(ep, msg): if a receiver waits, deliver and continue; otherwise block until one arrives.
Receive(ep): if the caller has a bound notification with bits set, return those bits (and clear them). Else if a sender waits, take its message. Else block until a sender arrives or the bound notification is signalled.
Call(ep, msg): like Send, but the caller then blocks awaiting a reply. The receiving thread's reply slot now names the caller.
Reply(msg): deliver msg to the thread in the caller's reply slot and clear the slot. Error if the slot is empty. Never blocks.
ReplyRecv(ep, msg): Reply if the slot is full, then Receive(ep).
Signal(ntfn): let b be the capability's badge, or 1 if unbadged. If a waiter is blocked, wake the first with b. Else if the bound thread is blocked in Receive, wake it with b. Else bits |= b.
Wait(ntfn): if bits != 0 return and clear them; else block.
Poll(ntfn): return and clear bits (possibly 0); never blocks.
BindNotification(ntfn): bind to the calling thread. One binding per thread and per notification.
SetIrqNotification(irq, ntfn): deliver interrupt irq as Signal through the given (badged) notification capability. The first process to route a line owns it; other holders of the IRQ capability get IrqAlreadyOwned until the owner dies or its notification is destroyed.
AckInterrupt(irq): unmask the line after handling (owner only).

An interrupt masks its line and signals its notification. If no route is set it stays masked.

Reply slot rules

A server thread has at most one pending reply. Receive (not ReplyRecv) with a pending reply drops it: the caller wakes with NoReply instead of blocking forever.
A reply slot names the caller by thread id and generation, so a reply can never reach a different thread that reused the id.
If the server thread dies, its pending caller wakes with NoReply.
If the caller dies, the reply slot is simply stale and Reply is a successful no-op.

Death

Destroying an endpoint or notification wakes every thread blocked on it with InvalidCap. Destroying a thread removes it from every queue, binding and reply slot; a dying process loses every IRQ route it set.

Register ABI (RISC-V)

Inputs: a7 = syscall number, arguments in a0..a5. A capability argument of NONE (usize::MAX) means "no capability".

Outputs: a0 = status (0 = ok, else an ErrorCode), a1.. = results. Receiving operations (Receive, Call, ReplyRecv, Wait) return:

Register	Value
a0	status
a1	badge (message) or signal bits (notification)
a2..a5	message words 0..3
a6	received capability slot, or `NONE`
a7	kind: 0 = message, 1 = call (reply expected), 2 = signal

8.8 KiB Raw Blame History

IPC