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 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`).

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 slot.
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`):

1. init `Call`s 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`.
2. The driver maps the region, allocates its own DMA memory
   (`CreateRegion`, `MapRegion`, `RegionAddress`) and resets the device.
3. 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 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 |