# 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)` returns how many
pages it mapped (so userspace never reaches past them) and 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 prints with it only until it
has started the log server, then hands it over and drops its own; from then
on the log server is the only holder, and every other process prints by
calling it (`types::log`) if init gave it a log endpoint.

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, log and storage capabilities it was handed, and
whether its parent put an arguments page at `ARGS_VA` (NUL-separated, the
program's name first; the parent fills a page and `MapPage`s it over, so
the program owns it and it goes when the program does).

Boot loads only init and storage, both packed into the kernel image (they
are what reads the disk, so they cannot come from it). The disk is one ext4
filesystem; storage refuses one with features it does not understand, and
mounts read-only one it could not keep consistent.
init gets storage's process and endpoint in slots 1 and 2, before the
board capabilities. Everything else init starts from its manifest
(`init/src/manifest.rs`), handing each program only the endpoints, device
and budget listed there. Storage, started before the log server, receives
its log endpoint from init later (`SET_LOG`, accepted only from the
unbadged holder of its endpoint).

Nothing that touches a user's files starts before someone has signed in.
Init starts the log, input, display and terminal servers, then the
gatekeeper (`types::gatekeeper`), handing it only the terminal, the keystore
(a small disk of its own, told from the data disk by its size) and the
virtio-rng device. Init calls `UNLOCK`, which returns once someone is in:
`[OK, flags, user id, role]`, a guest (`GUEST`) or a new keystore
(`FRESH`) among the flags. Then `KEY` (their master key), `SEED` (32 fresh
random bytes for storage this sign-in), `NAME`, and `REMOVED` until `DONE`
(users the owner removed just now). The gatekeeper exits.

Each user's files are in `users/<id>/` (`types::user`: the id in hex, or
`guest`): `home/`, `permissions/`, and per app `apps/<id>/` and
`data/<id>/`, each sealed under its own key derived from that user's
master key (crate `filecrypt`, layer `storage_server::encrypted`); the rest
of the disk is plaintext. While storage is still locked, init removes what
must go (`PURGE`, init only, only in `users/`, only while locked): every
user's folder on a new keystore, a removed user's, the last guest's. Then
it tells storage who is in (`SET_USER`) and hands over the key and seed
(`SET_KEY`, `SET_SEED`, a half per call, each once a sign-in; init only).
Only the signed-in user's folder opens; anyone else's is refused. Init
seeds whatever area of theirs is missing from the plaintext `factory/`,
then starts the session: the permission manager (the user's folder, and
`apps/` read-only) and the desktop. If the gatekeeper cannot unlock, init
stops there.

Signing out (`types::spawn::SIGN_OUT`, sent one way through the copy of
init's endpoint the shell holds) stops everything the session ran (the
shell, the permission manager, every app), locks storage (`LOCK`, init only: every grant
taken back, every file closed, the key forgotten), removes a guest's
files, and runs the gatekeeper again.

Init restarts what dies (`init/src/supervise.rs`): every server, and the
session's programs, except the gatekeeper and storage. A restarted server
gets the same endpoint, so its clients' capabilities reach the new one;
what it held in memory is gone. One whose clients keep state in it
(`restarts_clients`: input, display, terminal, the permission manager) has
them restarted after it, in turn. Crashes in a row wait longer each time
(at once, 1 s, 5 s, 30 s), then init gives up on it; a minute's run
forgives earlier crashes. What init gave a program through itself (its
storage grants, its spawn allowance and the children spawned from it) is
taken back as soon as it stops or dies. Storage's death stops the system:
it holds the key and every grant. Init's main thread never waits on a
server it restarts: its own output goes through a thread of its own
(`init/src/output.rs`), which waits on the log server instead.

A program's `uses` endpoints arrive as badged copies with `Execute` and
`Delegate`: the badge (unique per copy) tells the server which client is
calling, and `Delegate` lets the client send capabilities with its calls
and hand its access to programs it starts.

Storage is the exception: it mints every badged copy of its own endpoint,
and each badge names a *scope*, a subtree (or one file) and whether it may
write. For `uses: ["storage"]` init asks it for the whole disk, read-write.
Any holder can ask for a narrower one (`GRANT(path, write)`: inside its own
scope, writable only if it is) and gets it with `Delegate` kept, so it can
pass it on. Paths resolve inside the scope; `..` is refused. `RELEASE`,
called through a grant, takes it and everything granted from it back from
every holder (storage revokes its own copy, so the kernel deletes the
rest), closes their files and unmaps their buffers. Badge 0 (init) is the
whole disk; a badge storage did not issue, or took back, is `DENIED`.

Input reaches apps through the display server, the input server's only
client. It subscribes to the input server with a notification, drains it
when signalled, and passes events on to the app in focus: the last one to
subscribe (`types::display::input`). Apps out of focus get nothing.

The terminal server takes focus and draws text with the display server's
font. Its output side is the log protocol (`types::log`), so a program whose
log endpoint is the terminal prints there with `println!`: standard output
is whatever text endpoint a program was given. `READ` (`types::terminal`)
blocks until a line is typed and returns it in chunks, the last ending in
`\n`. Ctrl+C there drops the line. Keys typed while no line is read are
kept for the next one, except Ctrl+C, which signals the notification the
latest `ON_INTERRUPT` caller gave. Only a terminal copy whose badge has
`CONTROL` may register: init mints one for the shell alone, and the copy
the shell passes on to apps is its plain one. `REDRAW` repaints the screen and takes
input focus back.

The desktop is the shell, given the terminal, the permission manager,
the user's `home/` (its `/`) and signing out. Everything the owner runs is an app (docs/apps.md): a
command that is not a built-in asks the permission manager (`types::apps`,
client `libkos::apps`) to run it, passing the terminal as its output and a
read-only grant to the current folder (`cd`, `pwd`). The permission manager
adds what the app's manifest asks for and the owner allowed (the display,
its own data folder), runs it, and hands back the process; the shell waits
for its death (Ctrl+C kills it), releases the grant, and has the terminal
redraw if the app had the display. `install`, `apps`, `allow` and `revoke`
manage apps.

Only init holds `ProcessCreate`. Everyone else runs programs through init's
spawn service (`types::spawn`, client `libkos::spawn`), which init serves
once boot is done. A manifest entry with `spawns` gets a badged copy of
init's endpoint, the badge naming its allowance. `SPAWN(limits)` carries a
read-only storage grant to the program file itself; init loads it through
that grant (it needs no path, and loads nothing its requester could not
read) into a new, unstarted process, gives it a call-only log endpoint, and
replies with the process capability (Execute and Read, Delegate kept, so
the caller may pass it on to whoever it runs the program for). The caller delegates whatever else the child should hold and
starts it with `SpawnThreadIn`. The child's limits come out of the caller's
allowance (`OVER_ALLOWANCE` if they do not fit) and go back when init hears
the child die (`WatchDeath`, up to four watchers per process, so the caller
can watch too).

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

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 the same badge and permissions minus `Delegate`: the
receiver can use it but not pass it on. A sender that means the receiver
to pass it on sets `KEEP_DELEGATE` in the capability register
(`syscall_abi::Give`): the copy then keeps exactly the sender's rights,
`Delegate` included. Or it gives the capability 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.

## Budgets

Every process has a budget: frames (its pages, page tables and regions'
pages) and how many endpoints, notifications and regions it may own. Init
starts with the whole frame pool and every table's capacity.
`CreateProcess(create, pages, endpoints, notifications, regions)` carves
the child's limits out of the caller's unused budget (`OutOfMemory` if it
does not fit); boot carves the servers it loads out of init's. Over budget,
page requests fail with `OutOfMemory` and object creation with `NoFreeSlot`.
The limits of all live processes never add up to more than init got.

When a process dies its limits go back to its parent, and its children
pass to that parent, so their budgets return there in turn.

## 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 and its timer.

## Events

Two things the kernel notices itself, and reports by signalling a
notification (with that notification capability's badge, or bit 0 if it
has none). Both need `Write` on the notification, the right to signal it.

- `WatchDeath(process, notification)`: needs `Execute` on the process
  capability. The notification is signalled when that process dies, whether
  by `Exit`, a fault or `Kill`. One watcher per process; a new one replaces
  the old. Badge the notification per child to tell children apart.
- `SetTimer(notification, deadline)`: signals once `GetTime` reaches
  `deadline` (absolute, in `GetTime` ticks). One timer per process; setting
  it again replaces it, a zero deadline cancels it, a past one fires at once.
  The adapter programs the hardware for the earliest deadline, so a timer
  fires on time rather than on the next scheduling tick.

A target whose notification has since been destroyed is never signalled,
even if its id was reused.

## 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 |