246 lines
12 KiB
Markdown
246 lines
12 KiB
Markdown
# 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 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 and log capabilities it was handed.
|
|
|
|
Boot loads only init and storage (init needs it to read anything else):
|
|
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).
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
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(name, limits)` loads
|
|
the program into a new, unstarted process, gives it a call-only log
|
|
endpoint, and replies with the process capability (Execute and Read, no
|
|
Delegate). 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. 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.
|
|
|
|
## 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 |
|