IPC: calls, sends and replies

Processes talk only through the kernel’s IPC. A client calls an endpoint and blocks until a server replies, or sends one-way. The kernel carries a few words, a few handles and at most one run of pages, and it stamps every message with who sent it. There is no message queue: a queued message is a sender blocked on the endpoint.

Purpose

IPC is how authority is used. Holding an endpoint handle is the right to call the server behind it; the handle’s badge tells the server which grant is in use. Everything a server offers (a file, a socket, a key operation) is a call on an endpoint. So IPC has to do three things well: say truthfully who is calling, keep one caller from crowding out the others, and never let a page change hands in a way either side did not agree to.

Interface

Messages

A message carries:

• WORDS (4) machine words, widened to 64 bits in records so one layout serves rv32 and rv64;
• up to MAX_MSG_HANDLES (4) handles, copied: the sender keeps its own, and each copy keeps its stamp (the budget whose destruction revokes it; objects);
• at most one buffer of whole pages: a lend on a call, or a transfer on a send.

A message’s pages move by ownership: every page has one owner at a time, and only its owner touches it.

• A lend is up to MAX_LEND_PAGES (16 pages, 64 KiB) of pages the caller owns and may write. From the call until it returns, the caller has given them up: it may not read, write, lend, transfer, map or unmap them. A server that takes the call may read and write them, at an address the kernel picks, until it replies. The call’s return says who owns them: returned, as before the call; consumed, the server, whose reply frees them (R3).
• A transfer is pages the sender owns, given away for good: the sender gives them up at the send, and when a receiver takes the message they become the receiver’s, owner and payer both. A send that fails before a receiver takes it gives them back. A receiver takes a transfer only if its receive named a max_transfer at least that large.

On this kernel giving pages up removes them from the giver’s address space, so a touch is a fault (I9 (pages W^X, zeroed, lends unmapped)), and taking them maps them in the taker’s (memory). A backend without an MMU may hand the same buffer over instead, as long as every rule above holds.

sequenceDiagram
    participant C as caller
    participant S as server
    C->>S: call: four words, up to four handles, a lend of pages
    Note over C,S: the caller gives the lent pages up until the reply;<br/>the server reads and writes them at an address the kernel chose
    S-->>C: reply: four words, copies of the handles
    Note over C,S: the pages are the caller's again

Figure: what a call carries. The lent pages have one owner at a time.

The kernel attaches three facts the sender cannot choose (R14): the badge of the handle the message came through, the sender budget’s account (the principal it bills to; 0 for none) and its label set (the information-flow labels, containment). It also gives each message a message id, non-zero and never reused within the receiving process, which reply and serve name.

The calls

A server that holds a call without answering it yet holds it open: receive took it, and nothing forces a prompt reply. The thread may keep receiving. Each call it holds is an open call, and the one it is working on is its current call: receive sets it to the call just taken (or to none), serve switches it, and replying to it clears it.

Every blocking call takes a timeout in microseconds; FOREVER never expires (timer, I13 (every blocking call returns by its timeout)). Argument checks run in a fixed order, the same in the kernel and the model; the full rows are in the ABI reference.

What receive returns

One record layout for every result: (kind, msg_id, badge, account, labels, words, handles, buffer, pages). A field a kind does not use is 0.

Timeout is an error, not a record. Notices come before messages: first an abandoned-call notice for the receiving thread, then an exit notice, then the next message by R2. Receivers waiting on one endpoint are served in the order they began to wait; a receiver at MAX_OPEN_CALLS is passed over while no group has a send. An abandoned-call notice goes to the holder that began waiting first, and exit notices go in the order their processes ended. A handle revoked while its message was queued arrives as 0 in its slot, so slots keep their positions.

The record is checked when receive starts, and again just before a message or exit notice is delivered, because another thread of the process may have unmapped it meanwhile. If it can no longer be written, the receiver gets InvalidArgument and the message or notice stays pending for the next receive: nothing is taken that the receiver cannot be told about. Interrupts and abandoned-call notices follow the same rule (a bad record takes nothing).

flowchart TD
    R[receive on endpoint E] --> A{abandoned call held<br/>by this thread on E?}
    A -- yes --> NA[return abandoned notice]
    A -- no --> X{exit notice<br/>pending on E?}
    X -- yes --> NX[return exit notice]
    X -- no --> P{"next sender by R2<br/>(calls skipped if the process<br/>holds MAX_OPEN_CALLS)"}
    P -- none --> W[block until one arrives<br/>or the timeout]
    P -- found --> C{"R4: can the receiving<br/>budget pay for it all?"}
    C -- no --> RF[sender gets Refused,<br/>try the next sender]
    RF --> P
    C -- yes --> D[deliver: map buffer,<br/>install handles, return record]

Figure: what one receive on an endpoint returns, in order.

A bad record takes nothing

An interrupt or an abandoned-call notice is kept like a message: the record is checked just before either is delivered, and if it can no longer be written the receiver gets InvalidArgument and the item stays pending, the interrupt still fired (and its source masked) and the call’s notice still owed. The next receive that can write its record gets it, in the order above. So the one report of I15 (abandoned calls reported once) is always received, and a driver never loses an interrupt to its own thread’s unmap.

How a call completes

Status: built · partly tested: completion races between harts are not attacked by a case · tested: bench:ipc-outcomes, bench:timeouts, host:redoubt-sys::ipc_outcomes_round_trip_and_reject_impossible_combinations

A call returns three separate facts, and a caller must read all three (R13):

• the status: success or an error;
• the lend disposition, who owns the lent pages now: none (no lend), returned (as before the call) or consumed (the server, until its reply frees them; never touch them again);
• the reply disposition: present (the whole reply record was written) or absent (the record holds nothing; never decode it).

A successful reply tells the server delivered or discarded, and a mask of the reply’s handle slots that were installed in the caller.

With no lend every row reports none. The dispositions come back in registers, outside user memory, on every return including errors:

Registers a3-a7 are 0. redoubt_sys::decode_result refuses any other combination: for call, present with a status other than success or OutOfMemory, success without present, present with a consumed lend, and consumed without Timeout or Dead; for reply, a mask bit past the fourth handle, or any mask bit with discarded. The runtime then checks the mask against the handles its reply actually supplied.

The Rust runtime (libs/rt/src/ipc.rs) makes the rules hard to break. Endpoint::call takes the lend as an owned Buffer and returns a CallOutcome holding the status, the buffer only if it was returned, and the reply only if it is present. Request::reply consumes the request, and hands it back with the error if the reply is refused, so the server can still answer it.

sequenceDiagram
    participant C as Client thread
    participant K as Kernel
    participant S as Server thread
    S->>K: receive(E, timeout, max_transfer)
    Note over S,K: blocks: nothing queued
    C->>K: call(E, words, handles, lend 4 pages, timeout)
    Note over K: checks, R1 labels, R2 cap,<br/>client gives the lend up
    K->>S: record: kind=call, msg_id, badge,<br/>account, labels, words, handles, lend at A
    Note over K: open call page charged to server (R4a),<br/>lend charged to both sides (R3)
    S->>S: read and write the lend at A
    S->>K: reply(msg_id, words, handles)
    Note over K: lend the client's again,<br/>reply record written
    K-->>C: status 0, lend returned, reply present
    K-->>S: delivered, mask

Figure: a call with a lend, from receive to reply.

Authority

Status: built · tested: bench:redoubt-ipc-attack, mutation:R1ChecksReceiverNotOwner

• An endpoint handle with badge 0 is the receive right. Only it may receive, and only its holder can mint handles with other badges. endpoint_create returns it.
• Any other endpoint handle is the right to call or send, identified to the server by its badge. Handles carry no rights bits: whoever holds a copy may use it. A server narrows a grant by minting a new badge and meaning less by it.
• IPC can grant only what the sender already holds: a message copies the sender’s handles, each with its own stamp. It creates no authority.
• IPC never gives the receiver anything of the sender’s but the words, the copied handles and the buffer: not the sender’s other handles, budget, address or identity beyond the three attached facts. The raw budget id never travels.
• Handing a receive right to another budget is delegation of the whole endpoint, and it is never handed across label sets (I7 (every flow obeys R1)).

Security properties

R1 (flow)

Information flows from budget A to budget B only if B is class system or B’s labels include all of A’s. A message is a flow from the sender’s budget to the endpoint’s owner (the budget that created it), whoever takes it, so the check is made when the message is sent. Because every call is answered or refused, it is also a flow back. So between two user-class budgets the label sets must be equal, or the call gets LabelDenied. When either side is system class the kernel does not check: system servers serve many label sets and check them themselves (servers). An exit notice is a flow from the exiting budget to the owner of the exit endpoint; one that fails the rule is dropped. A budget_usage read is a flow from the budget read to the reader (budgets).

R2 (fair waiting)

Senders blocked on an endpoint are grouped by their budget’s account and label set, and, for account 0 (no principal: the boot budgets, and any budget carved without one, of either class), by budget as well. Each receive takes the oldest message of the group served least recently: a group’s turn is due from when it was last served, or from when its oldest message arrived if it has not been served since. Ties go to the lower group key. A group’s turn is read from one kernel counter no process reads: its oldest queued message’s arrival, or the group’s last take if that came later, kept with the group only while it has a message queued, so a group with nothing queued keeps nothing. Each endpoint keeps its waiting groups in the order their turns fall due, and apart those with a send queued in the order their oldest sends fall due, for a receiver at MAX_OPEN_CALLS (R4a); a take moves its group behind the others on both, one write whatever the group holds. A group’s place therefore depends only on its own history, so the order in which one label set’s groups are served is the same whatever other label sets send. A single cursor over all groups would not keep that: a vault session’s take would move the cursor, and with it which unlabelled caller is served next, which crash blame then shows to unlabelled readers (R37 (vault non-interference)). A group that already has WAIT_CAP (32) messages queued on the endpoint gets Busy at once. Only queued messages count; a taken call is bounded by R4a instead. Keying by label set keeps a vault session and its owner’s ordinary session, which share an account, from sharing a turn or a cap. Keying account-0 callers by budget keeps one busy system server from filling another’s cap. With k groups waiting and the receiver below its open-call limit, each group’s oldest message is taken within k receives (I11 (fair turns)).

R3 (lends and abandoned calls)

A lend’s range must be the caller’s own writable RAM. Pages in it that were never touched are backed first, charged to the caller like map_anon’s; a caller that cannot pay for them gets InvalidArgument, since call has no OutOfMemory of its own. A lent page stays charged to the caller. Taking the call charges it to the receiving process’s budget as well, until reply gives it back. The page tables that map the lend in the receiver are charged to the receiver too, and go at the reply that leaves them mapping nothing (memory).

A taken call is abandoned when its caller dies, times out, or is failed by revocation. Then:

• the caller’s charge ends and the lend becomes the server’s alone: it may still read and write it until its reply;
• the thread holding the call gets one abandoned-call notice, on the endpoint the call arrived on (I15 (abandoned calls reported once));
• the call stays open, and counts against the server’s limit, until the server replies; that reply reaches nobody, and replying frees the lend.

A thread owed several notices gets one per receive, each exactly once, in no promised order.

A reply that comes before the abandonment is delivered, and nothing is abandoned. If the abandonment comes first and the server replies before it has received the notice, reply returns discarded, mask 0, and no notice follows: the reply closed the call.

The destruction of the endpoint a call arrived on (budgets) also abandons the calls taken through it, and fails their callers with Dead and their lends consumed, but no notice follows: there is no endpoint left to receive one on. Dead from receive reaches only a thread already blocked in receive on the endpoint; the sure sign is the reply: a reply to one of those calls returns discarded, mask 0, and frees its lend, as for any abandoned call.

stateDiagram-v2
    [*] --> Queued: call
    Queued --> [*]: Refused / Timeout / Dead<br/>(lend returned)
    Queued --> Open: receive takes it
    Open --> [*]: reply (delivered)<br/>lend returned
    Open --> [*]: server dies<br/>caller gets Dead, lend returned
    Open --> Abandoned: caller dies, times out,<br/>or is revoked
    Abandoned --> [*]: server replies<br/>(discarded, lend freed)
    Abandoned --> [*]: server dies<br/>(lend freed)

Figure: the life of a call. The lend has exactly one owner in every state.

R4 (delivery)

A message is delivered only if the receiving process’s budget can pay for everything it brings: the handle-table pages for its handles, a call’s open-call page, its lent or transferred pages and the page tables to map them. A lend is charged to the receiver even when both sides share a budget (R3). A transfer is charged to the receiver instead of the sender, so between two processes of one budget it moves no charge and costs nothing. A transfer also needs a max_transfer at least its size. Handles that would take the receiver past MAX_HANDLES (4096) are a cost it cannot pay, and so is a buffer with no free run of pages for it in the receiver’s message area. Otherwise the sender gets Refused and the kernel moves on to the next sender. A receive never fails for want of pages.

A reply is never refused: its caller is blocked and has nowhere else to put the error. Reply handles that do not fit the caller are dropped, each 0 in its slot. The words and the other handles arrive, and the caller’s call returns OutOfMemory with the reply present.

R4a (open calls)

Status: built · tested: bench:redoubt-ipc, bench:net-pinned-ssh, mutation:R4aOpenCallsPerThread, mutation:R4aFullTakesNothing

Taking a call opens it and charges one page to the receiving process’s budget; reply closes it and frees the page. A process holding MAX_OPEN_CALLS (256) open calls takes no more: calls stay queued and R2’s turns skip them, while its receive still delivers sends, interrupts and notices. A send is never an open call, so reply to a send’s id is InvalidArgument.

R4b (a server dies)

When a thread or process exits, faults or is killed holding open calls, each waiting caller gets Dead and its lend back intact; the lend of an abandoned call is freed. Senders still queued on the endpoint keep waiting: the endpoint outlives the server, and a restarted server receives them (init). A thread of a doomed process (one the destruction will kill: its budget is dying, or its creator’s is) is offered nothing (no message, exit notice or abandoned-call notice): nothing is delivered while the destruction runs, and the deliveries at its end find it gone. What it would have taken stays for the next receiver outside the destruction.

R13 (one outcome per call)

Every call ends in exactly one row of the completion table, and the caller and server agree on it. present means the whole reply record was written, and only then may the caller decode it. consumed means the lend’s mapping and charge have ended. The body record is checked readable and writable before anything is delivered, and checked again at completion, because another thread may have unmapped it while the call waited. If the reply cannot be written, every handle this reply installed in the caller is closed again and its table pages released; the caller gets InvalidArgument, its lend back and absent, and the server gets discarded. Checking the record, copying, installing or rolling back handles and publishing the outcome are one step: the kernel runs with interrupts off and holds the memory manager’s guard throughout, so no unmap, remap or teardown can fall between them.

The clients keep it above the kernel: the client library’s typed call, and a session’s generated Elixir client, return a reply’s handles to the caller and keep none that an error reply, or one that does not decode, brought (wire).

R14 (unforgeable sender)

The badge, account and labels a receiver sees are the kernel’s: the badge of the handle used, and the sender budget’s account and labels at the time of sending. No argument of call or send can set them. Message ids are per receiving process, so they reveal nothing of anyone else’s traffic, and a stale id cannot reach a later message (I12 (ids never reused)).

Failure and restart

• The server dies holding calls: callers get Dead and their lends back (R4b). Queued senders wait for the restarted server on the same endpoint.
• The caller dies, times out or is revoked after the server took the call: the call is abandoned (R3). The server keeps the lend until it replies and pays for it.
• A budget is destroyed: endpoints it owns are destroyed and everything waiting on them gets Dead; queued messages sent through a handle it stamped fail with Dead; a taken call sent through one is abandoned (R10 (destruction)). A taken call on a destroyed endpoint is abandoned with no notice (R3): a thread blocked in receive on it gets Dead, and the reply’s discarded is the sure sign.
• Crash blame: when a server process faults, or exits while it holds open calls, the exit notice blames the account and labels of the sender of the ending thread’s current call, or nobody if it has none (R21 (crash blame)). A send is never blamed. A server calls serve before resuming a held call so that a crash blames the right caller.
• No argument to any IPC call can make the kernel panic (I14 (no call panics the kernel)).

Residual risks

• System-class servers are trusted to check labels. R1 does not constrain a flow into or out of a system budget. A system server that serves two label sets and mixes their data breaks label separation, and the kernel cannot see it (servers).
• Refused and Busy are signals. Refused tells a sender one bit about the receiver’s budget; Busy tells it its own group is full. A sender with a clock learns as much from timing. Covert and timing channels are out of scope (TENETS).
• A server pays for the calls it holds. An abandoned call’s lend stays charged to the server until it replies; a server that never replies keeps paying. That is the server’s own cost, never another budget’s.
• A consumed lend is gone. A caller whose taken call times out loses those pages. Callers that cannot afford that must not lend them with a short timeout.
• Completion races between harts are argued from the code, not attacked by a case. On one hart the kernel runs with interrupts off. On several (a build for more than one hart), each kernel global is guarded by its own lock, and the completion holds the memory manager’s for the whole step.

Why

• No queue, no allocation for the queue. A queued message is its blocked sender, and the sender’s own thread page (already paid for) holds it. So queueing a call or send allocates no kernel memory and cannot make the kernel allocate on a receiver’s behalf. The only pages they may allocate are the sender’s own untouched buffer pages, backed and charged to the sender (R3). Finding a message’s parties costs a few links in pages already paid for: the endpoint’s frame heads its receivers and its groups, and the links are in the waiting threads’ own pages.
• Lend, not copy. A 9P message is up to 64 KiB. Moving pages costs page-table updates, not copies, and unmapping them from the caller means neither side can see the other change them mid-call.
• The reply is never refused, because the caller is blocked and has no other way to learn the outcome; dropping the handles that do not fit, and saying so, is the only safe partial.
• An abandoned lend stays with the server so the server never has a page pulled from under it mid-request; it frees the page by replying.
• Owner, not receiver, for R1. The check is made at send time against the endpoint’s owner, so it cannot depend on which thread later receives, and a receive right cannot be passed across label sets to get around it.
• Groups, not senders, for fairness. One principal with many processes gets one turn, not one per process, and a full group gets Busy at once instead of blocking others.