k-os/docs/ipc.md

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 an unbadged capability with a badge and narrower permissions. A badge cannot be changed once set.

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

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 its permissions and badge unchanged. 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.
• AckInterrupt(irq): unmask the line after handling.

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, reply slot and IRQ route.

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