Reading this book

Redoubt is a headless, multi-user operating system for RISC-V, built so that hostile agents can run on it, do real work, and not get out. This book describes the whole system from its code: what each part does, which rule it keeps, which test attacks that rule, and what is still planned. The tenets outrank every other page.

Reading order

1. The tenets: what Redoubt is, the threat model, the guarantees and the walls that hold them, the non-goals.
2. The glossary: the one vocabulary every page uses. Skim it once; come back to it.
3. The kernel: handles, IPC, memory, budgets, scheduling, the timer, processes, devices, boot, and the model that checks them.
4. The servers: trust tiers and labels, then one page per server, from init and the steward to the network path.
5. Userland: what a person, an agent and a developer see.
6. The security register: every security property on one table, with the code that enforces it, the test that attacks it and its residual risks. An auditor starts here.
7. The plan: one page per milestone, then the follow-ups in todo/ and the ideas past the plan in beyond/.
8. The test bench: how every claim in this book is tested.

To build and run Redoubt, see GETTING-STARTED.md. How the work itself is organised, and in what order, is outside this book: AGENTS.md is the way in.

Written as if complete

Every page describes the system as it will be at the end of the plan. Whether a part exists today is said by the status line at the top of its section, never by the prose. A section that is part built and part planned is split in two.

A status with four or more tests folds them away, so the section opens on its claim and not on a list: the status sits in a <summary> with the count of tests, and the tests follow as a bullet list inside the <details>, one per line. The checker holds the count to the list.

<details><summary>Status: built · tested (3)</summary>

- bench:redoubt-ipc
- host:redoubt-sys::every_call_round_trips
- mutation:R2OneCursor

</details>

“Built” means the code exists and its named tests pass. A host test or a build case is not a boot: code built and host-tested is not thereby running in the integrated system, and running there is its own planned section.

A section without its own status line inherits its nearest parent’s. Purpose, Residual risks and Why sections carry none: they say why and what is left, not what is claimed. Status lines appear on the kernel, server and userland pages and on the test bench page; plan, follow-up and idea pages do not use them, and the security register has a status column instead.

A test is named by its kind:

The milestones

A milestone is always written with its name.

Anything past M6 (persist, install, share) is beyond M6: an idea, not a goal, one page each under beyond/.

Rule IDs

Every security property has an ID, defined once by a heading on the page that owns it and cited everywhere else with its short name the first time on a page:

• Rules are one series, R and a number. The kernel’s come first, on the kernel pages, such as R3 (lends and abandoned calls); the server, network and policy rules take the numbers after them, on the server pages, such as R25 (the label check). A letter after the number refines a rule: R4a (open calls).
• Invariants are I and a number, all on invariants, such as I9 (pages W^X, zeroed, lends unmapped). The model checks every one after every step.
• Rule F (trusted verdicts) is the bench’s own: a verdict comes only from a party the attacker cannot impersonate (the test bench).

IDs are cited one at a time, never as ranges, and never reused: a withdrawn rule keeps its heading, marked withdrawn. The security register lists every ID.

Rendering

The pages are plain Markdown and read on GitHub as they are. mdBook renders them as a book with navigation and search:

mdbook build docs      # output in target/book
mdbook serve docs      # the same, served on localhost with live reload

Diagrams are text inside the pages: Mermaid for flows, sequences, state machines and the packet diagrams that draw a record’s words and bits, which GitHub renders too; and memmap blocks for address maps, which the book’s own preprocessor (tools/mdbook-memmap) draws to scale on a log axis, one region per line with its first address, its name and a note per column, and which read as a table on GitHub. Solid lines are built; dashed lines are planned. The book needs the mdbook-mermaid preprocessor and cargo for its own. The docs checker, redoubt-doccheck, holds every page to these rules (the test bench).

The search index

The book’s search index (target/book/searchindex-<hash>.js) is held to a ceiling of 7,000,000 bytes, 30 % under the 10,000,000 at which mdbook warns and the build check fails; the_book_builds fails over the ceiling naming the size and the three largest pages, so the failure says what grew. The index is about three times the pages’ text (3.2× in October 2026: a term’s postings for every section it appears in), and the three largest pages hold a fifth of the text. The ceiling moves only by a stated, measured decision in the same change as the measurement, and never past mdbook’s 10,000,000. Headroom is kept by keeping the pages to their argument: measurements, evidence tables, transcripts and reasoning beyond what a rule or a design needs stay outside the book, in the working notes or a case’s comment, not on the page. A page leaving the book, or splitting, is the owner’s decision, never a way to pass the check. The index needs an mdbook built with elasticlunr-rs 3.1.0 or later (an older indexer doubles every field’s tokens into the next field; scripts/setup.sh installs the right one and the same check reads the version from the binary).

A tour of Redoubt

Redoubt is a prison: a headless RISC-V operating system that the most capable and most malicious agents can run on, do real work on, and not get out of. This tour shows the whole in five pictures, each with a link to the page that gives the detail. In every figure solid lines and boxes are built; dashed ones are planned.

The prison walls

An agent sits innermost, and each wall around it holds only what the wall outside it gave. The one door in is SSH; the one way to move authority or data across a wall is an approval by a human, on a channel nothing inside can draw on. The host’s device emulation and the human’s judgment are walls the OS rests on but does not own.

flowchart TB
    subgraph host["the host: virtio emulation"]
      FW["firmware (RustSBI)"] --> LD["loader: verifies the bundle"] --> K["kernel"]
      K -.-> INIT["init"]
      K --> KD["keyd"]
      K --> SH["shared servers: files, disk, network, console"]
      K -.-> ST["the steward"]
      K -.-> SSHD["sshd"]
      ST -.-> SE["sessions: one Elixir VM each"]
      SE -.-> AG["agents, each in a lease"]
    end
    P(["a person"]) -.->|"SSH, the one door"| SSHD
    H(["the approving human"]) -.->|"approve@box"| ST
    classDef planned stroke-dasharray: 5 5
    class INIT,ST,SSHD,SE,AG,P,H planned

Figure: the prison walls. init’s manifest handling, the steward, sshd and sessions are planned for M1 (sessions over SSH, kept apart), agents and approvals for M3 (agents, approvals and the attack suite); the servers drawn solid are built and attacked in host tests or on the kernel.

Detail: the walls

The layers

The kernel keeps five things: memory, threads, IPC, interrupt delivery and the timer. Everything else (drivers, file systems, the network, keys, logins and policy) is an unprivileged server that reaches hardware, other servers and the kernel only through the handles it was given. A person’s session is one more process above them: an Elixir VM that holds narrowed connections to the servers and nothing else.

flowchart TB
    SESS["a session: an Elixir VM, beamlet"]
    SRV["unprivileged servers: drivers, files, network, keys, logins, policy"]
    KER["kernel: memory, threads, IPC, interrupts, the timer"]
    HW["RISC-V hart and virtio devices"]
    SESS -.->|"IPC through its handles"| SRV
    SRV -->|"system calls"| KER
    KER --> HW
    classDef planned stroke-dasharray: 5 5
    class SESS planned

Figure: the layers. Only the kernel and the firmware below it run privileged; a server holds no authority it was not handed.

Detail: the kernel, the servers, sessions and namespaces

One IPC call

A client calls a server through an endpoint handle, and may lend it pages for the length of the call. The kernel, not the client, tells the server who is calling: it stamps each message with the handle’s badge, the caller’s account and its labels, which the client cannot forge. The reply hands the lent pages back.

sequenceDiagram
    participant C as Client
    participant K as Kernel
    participant S as Server
    S->>K: receive
    C->>K: call, lending pages
    Note over K: checks labels,<br/>unmaps the lend from the client
    K->>S: message stamped with badge, account, labels
    S->>K: reply
    K->>C: reply, lend returned

Figure: one IPC call. The stamp is the server’s only knowledge of its caller.

Detail: IPC

Capability delegation

Authority flows down a tree and narrows at every step. The steward mints each launch fresh, narrower connections: a person’s session gets its own, an agent gets a subset of its launcher’s under a lease, and a sub-agent a subset of that. A lease is a budget with a deadline; when it ends, everything below it ends too.

flowchart TB
    ST["the steward: mints fresh, narrower connections"]
    L["launcher: a person's session"]
    A["agent, in a lease: a subset of the launcher's"]
    SA["sub-agent: a subset of the agent's"]
    LE["the lease ends: its deadline, or the sponsor"]
    ST -.-> L
    L -.->|"narrower"| A
    A -.->|"narrower again"| SA
    LE -.-x A
    LE -.-x SA
    classDef planned stroke-dasharray: 5 5
    class ST,L,A,SA planned

Figure: capability delegation. Every step holds less than the one above it. The tree is planned; the kernel’s deadlines, which end a lease, are built.

Detail: agents, leases and labels

The road

The plan is six milestones, each a whole working system. M1 (sessions over SSH, kept apart) is in progress: the kernel, the drivers, the network server and the serving library are built and attack-tested, and the steward and SSH logins are next; the contained agent is M3 (agents, approvals and the attack suite)’s.

flowchart LR
    m1["M1 (sessions over SSH, kept apart)<br/>in progress"]
    m2["M2 (usable shell)"]
    m3["M3 (agents, approvals and the attack suite)"]
    m4["M4 (files in and out)"]
    m5["M5 (self-hosted development)"]
    m6["M6 (persist, install, share)"]
    m1 -.-> m2 -.-> m3 -.-> m4 -.-> m5 -.-> m6
    classDef planned stroke-dasharray: 5 5
    class m2,m3,m4,m5,m6 planned

Figure: the road. M1 (sessions over SSH, kept apart) is part built (solid box); the rest are planned.

Detail: M1 (sessions over SSH, kept apart), the milestones

Tenets

This page outranks every other page in the book. When a change conflicts with a tenet, either the change loses or the tenet is amended here first, with its reason (changing a tenet). Other pages say how a mechanism works; this one says what the whole must achieve, against whom, and where its limits are.

What Redoubt is

Redoubt is a prison: a headless, multi-user operating system built so that the most capable and most malicious agents can run on it, do real work, and not get out.

• It runs on RISC-V softcores, nearly always over virtio (block, network, console). It never has a local display, keyboard or mouse. People reach it over SSH.
• Auditable by construction. Everything that runs on the machine is Rust, with assembly only where Rust cannot reach. No C and no shell script runs on the machine, userland included. The trusted computing base (the firmware interface, the loader and the kernel) is small enough to read like a textbook.
• Authority is capabilities. There is no ambient authority: no root, no user IDs that grant access, no global file tree. A child’s capabilities are its launcher’s or narrower. An agent never inherits network access.
• The network is closed by default. What a principal may reach is written as names, and an agent reaches the outside only through gateways that hold its keys and check its requests.
• Residual risks are stated, never hidden. Every guarantee below names the walls it rests on and the test that attacks each one. No page says “impossible”.

Every page is written as if M1 (sessions over SSH, kept apart) through M6 (persist, install, share) were complete; each section’s status line says what is built today (reading this book).

Threat model

The adversary has the full source, automates its exploit attempts, and has as much time as it likes. It controls every process it runs, including its whole Elixir VM (beamlet is outside the trusted computing base), and it may compromise a server it talks to. It may be an agent, a person logged in over SSH, or several of them colluding with a pre-arranged code. It has a perfect clock: secrets are protected by isolation, and by constant-time code where a rule claims it (side channels), never by hiding time.

Trusted: the firmware interface, the loader and the kernel; the servers that hold system authority (init, the steward, keyd) and sshd, which carries each channel’s labels; a driver that programs DMA, unless the hardware confines its DMA; the host that emulates the virtio devices; and the approving human’s judgment, but never the channel the approval travels on (see the walls).

A compromised shared server exposes what its clients entrusted to it, and no more: it holds only its own handles, and the kernel stamps every message with its sender (R14 (unforgeable sender)).

Out of scope:

• physical attacks and malicious hardware;
• microarchitectural side channels (caches, branch predictors, memory bandwidth);
• covert communication between co-located budgets through power, heat, electromagnetic emission, a shared clock or any other physical coupling. On one machine these couple any two domains, so no operating system can close or bound them; the only zero is placement, which is a deployment’s choice (the FPGA platform).

Not claimed: the boot bundle’s confidentiality. Verified boot proves the bundle’s integrity; it does not hide it. Seeds and anything else in the bundle are readable by whoever reads the bundle image (boot’s residual risks).

Software closes every intentional path: a message, a write, a read up, a sink, metadata, a counter or a shared cap. An intentional path across a label boundary is a design hole, whatever its bandwidth. Timing that software can reduce is reduced (limits are carved, never overcommitted; caps are counted per account and label set; no global counter is visible), and what remains is listed under side channels.

Adversarial agents and real attacks test the design; review alone cannot bound the damage a bug does.

Guarantees

Redoubt makes three guarantees. Each is a set of rules, defined on the page that enforces them and listed with their tests in the security register.

Capability closure

An agent’s reachable authority never exceeds its initial grants, plus what a steward action a human approved adds, plus what a holder already able to reach it passes to it inside its trust domain. Every delegation step through a launcher narrows.

• A handle names an object, a badge and a stamp; the kernel holds it, and a process can copy or close it but never forge or widen it. A minted handle keeps the stamp of the one it came from, so revoking the source revokes it (R9 (stamps)).
• A child budget’s limits are carved from its parent’s and never add up to more (R7 (carving)); destroying a budget revokes everything under it (R10 (destruction)).
• A launcher passes fresh, narrower connections, never its own; a grant is made in a revocation scope and dies with it (R41 (narrowing by revocation scope)).
• No server is given a system budget to hand out (R33 (no server holds a system budget)), a restart never widens what a service holds (R73 (a restart never widens)), and code a principal did not choose to trust gets no authority (R71 (no new authority without trust)).

Open: the closure is stated with its same-label qualification: a holder inside the agent’s trust domain may pass it a handle it already has, with no approval. Whether the guarantee should instead be stated per trust domain, or same-label delegation be recorded by the steward, is not decided.

Label non-interference

No intentional path crosses a label boundary: not a call or a send, a write, a read up, a sink, metadata, a counter or a shared cap. The label set, not the capability set, is the isolation unit. Two budgets with equal label sets are one trust domain, and a handle passed between them crosses nothing. Two budgets with differing label sets have no path the OS carries, except one item at a time through the steward, after the label’s owner approves it.

The residual is stated: there is no non-collusion guarantee within one label set. Two agents with different handle sets but the same label set are not kept from cooperating; the kernel carries messages between whoever holds each other’s handles. Agents that must not collude get different labels (labels and vaults).

• The kernel refuses a call or send between two user budgets whose label sets differ, and checks exit notices and usage reads the same way (R1 (flow)); servers in system budgets check labels themselves. Labels only grow downward the budget tree (I6 (labels only grow downward)).
• A shared server applies the same check to every object it serves (R25 (the label check)), and a sink refuses every labelled caller (R60 (a sink refuses labels)).
• Nothing a vault session does is visible to its principal’s unlabelled sessions (R37 (vault non-interference)): caps are counted per account and label set (R26 (admission fairness)), budgets are split into fixed sub-budgets per label set, and crash blame is kept per label set (R40 (blame by label set)).
• Data leaves a label only by declassification, and enters a confined domain only by a push: one approved item each, snapshotted, audited (R42 (one approved item)).

Confinement. In a confined deployment no two label sets share a server instance, volume, endpoint, network instance or device, and no labelled domain reads a shared unlabelled volume; a manifest that would place them so fails the boot (R34 (confined placement)). R34 names the one exception, the control plane: the steward and sshd, and only by three kinds of edge.

• the request and owner-approval path;
• per-item reader and writer budgets, each carrying exactly one label set and dying after one item (declassification and push);
• lease supervision: ending a lease, and learning that it ended.

No data server or device is exempt. init checks the declared graph at boot, and the steward checks every budget and grant it creates later against the same rule. The residual is stated: the named mediators are trusted across the labels they serve. A bug in the steward or sshd reaches every label set it mediates.

Human control

Every increase in authority and every declassification is an out-of-band human approval, leases bound time, and the sponsor can always end a lease.

• An approval happens only where nothing the requester runs can draw, type or listen: on the approval channel the steward alone drives, like a second factor (R38 (out-of-band approval), R68 (only the steward on approve@box)).
• A lease is a budget with a deadline: when it passes, the kernel destroys the budget and everything in it, whether or not the steward is running (R39 (leases end)).
• The sponsor ends a lease sooner, and a request to do so is answered ahead of admission, so an agent flooding its sponsor’s share of a server cannot block it (R26). How fast the steward answers under load is a measured target, not a proven bound (scheduling).

The design protects the approval channel from the requester. It does not protect the human’s judgment: see the approval human.

The walls

The prison is layers, and each layer holds only what the one inside it was given. An agent sits innermost: in its own VM, in a lease, with narrowed connections and no socket.

flowchart TB
    subgraph HOST["host: virtio emulation (a wall the OS does not own)"]
      subgraph M["the machine"]
        FW["RustSBI firmware (M-mode)"]
        LD["loader: verifies the bundle"]
        K["kernel: handles, IPC, budgets, W^X"]
        subgraph SYS["system servers"]
          INIT["init"]
          ST["steward"]
          KD["keyd"]
        end
        subgraph SH["shared servers"]
          FS["bootfsd, littlefsd, consoled"]
          DRV["blkd, netd (drivers)"]
          IPD["ipd, resolver"]
          GW["gatewayd"]
          SSHD["sshd"]
        end
        subgraph SESS["sessions (user budgets)"]
          S["a person's session"]
          subgraph LEASE["a lease"]
            AG["agent"]
          end
        end
      end
    end
    HUMAN(["the approving human"])
    NET(["the internet: allowed egress"])
    FW --> LD --> K
    K --> SYS
    K --> SH
    K --> SESS
    S --> SSHD
    AG -.-> GW
    GW -.-> IPD
    IPD --> DRV
    DRV --> NET
    SSHD --> HUMAN
    HUMAN -.->|"approve@box"| ST

Figure: the prison walls. Solid lines are built, dashed lines planned. Each box holds only the handles the box around it gave it; four walls (the host’s emulation, the human, allowed egress and side channels) are not the OS’s own, and are named below.

Inside the machine each wall is a rule with a test. Four walls are not the OS’s own. They are named here, and every page that rests on one says so in its residual risks.

The approval human

An approval is only as good as the human’s judgment. The requester can persuade, repeat until the human tires, or phrase a request that reads one way and means another. The design shows the whole request on a channel the requester cannot draw on, keeps each declassified item small and printable (R42), and audits every approval; it does not decide for the human. The escape room attacks this wall with collusion through the human (agents).

Host virtio emulation

Redoubt’s devices are virtio devices emulated by the host (QEMU, or a softcore’s host side). Only the drivers (blkd, netd, consoled) touch a device, each through its own device objects (R18 (device authority)), and they treat everything a device says as hostile: a disk’s lie is a failure, never corruption (R52 (a lie is a failure, never corruption)), and a bad frame is content (R55 (a bad frame is content, not a lie)). But a bug in the host’s emulation that a driver’s requests can reach is outside the OS, and a driver that programs DMA is trusted unless the hardware confines it. No agent or session holds a device.

Allowed egress

Every allowed channel out of the box can carry data. A model API an agent may call, a git remote it may push to, and the upstream DNS resolver’s shared cache (which serves everyone outside the box, so its timing is visible to anyone) are paths out that the design narrows but cannot close. gatewayd checks and meters every request against the capability it came through (R65 (a request only within its capability)) and logs it; the resolver answers only allowed names (R63 (only allowed names)). No labelled caller reaches any egress (R60). What an unlabelled agent sends through an allowed channel is the sponsor’s to allow.

Side channels

Timing, shared caches and shared hardware couple budgets in ways software can reduce but not close:

• the kernel and the scheduler, which every label set shares, confined or not, and server CPU spent on a caller’s behalf;
• CPU caches, the shared second-level cache and memory bandwidth; on QEMU and ordinary hardware none of these is partitioned;
• a shared server’s caches and the disk: a vault’s reads warm a cache an unlabelled session can time, unless the deployment is confined;
• a shared server’s service slot: if it crashes on its own, whose call it was serving depends on what was queued ahead. A vault’s queued calls therefore change an unlabelled caller’s result (Dead, or a later reply) and the crash blame it can read, unless the deployment is confined (steward);
• a server sized for fewer buckets than the label sets it serves, which refuses latecomers (serving).

A confined deployment removes the shared servers, endpoints and devices. What is left is the kernel’s and the hardware’s: every label set shares the one kernel and its cores, because the kernel is the trusted base and a core’s timing is no more partitioned than the caches around it. Hardware placement is beyond M6.

Constant time is claimed for one thing: keyd’s signing, whatever the key and the nonce (R45 (constant-time signing)). That claim is partly tested: its timing tests need an optimised build that no bench case runs. No other code that handles a secret is claimed constant-time; such a secret rests on isolation alone, and its timing is a side channel like the others above.

Network policy

The network is where a prison most easily leaks, so its rules are stated here once.

• Default deny. A principal reaches only what its grants allow; an agent inherits no network access at all.
• Allowlists are written as names. A name rule covers a domain or a suffix, matched only at a label boundary; a blocklist only subtracts from an allowlist and always wins.
• DNS is mediated. The resolver answers only names in the caller’s allowlist (R63), and a connection made by name is pinned to the address that was checked (R64 (connections by name are pinned)).
• Agents get gateway capabilities, not sockets. gatewayd holds the keys, speaks TLS, checks each request against the grant and logs it; no credential ever reaches the agent (R66 (no credential leaves gatewayd)).
• Only people get name-scoped TCP, through ipd with a resolver connection: a scope reaches only what it allows (R58 (a scope reaches only what it allows)), and a grant only narrows it (R61 (scopes only narrow)).
• Always forbidden, whatever a grant says: the host’s and cloud metadata addresses, the box’s own services from inside (R59 (never the box’s own addresses)), and inbound traffic other than SSH (with SFTP and SCP inside it).
• Web serving, when it comes, terminates TCP, TLS and HTTP in separate trusted servers split by privilege; applications get parsed requests, and inbound access is only through SSH forwarding (the web stack).

The network path, from an agent through gatewayd and ipd to netd, is drawn on the servers.

The tenets

1. Simple enough to audit in full

A competent reader can read the whole trusted computing base and hold it in their head. It reads like a textbook example of each mechanism.

• The kernel keeps memory, threads, IPC, interrupt delivery and the timer. Nothing else. Drivers, file systems and policy are unprivileged servers (the kernel).
• One obvious way to do each thing. A trick needs a comment that says why the obvious way does not work; if the comment is hard to write, the trick goes.
• Size is budgeted, not just observed. Growing the trusted computing base needs a stated reason.
• Deleting code beats adding configuration. A feature nobody uses on our targets is removed, not carried.
• Every design decision is written down where a newcomer can follow it: in this book.

2. Secure by construction

• No ambient authority. A process touches only what it was given: memory it mapped, connections it holds, devices it was granted. “First to ask gets it” is not a policy.
• Least privilege all the way down. The kernel does not trust processes, servers do not trust clients, the loader does not trust images, and nothing trusts input it has not checked.
• W^X everywhere, the kernel’s own mappings included: no page is ever writable and executable under any alias (R11 (memory), R19 (kernel W^X)).
• Verified boot. Every byte that runs in a privileged mode is authenticated before it runs (R15 (verified boot)).
• Fail closed and loudly. On a violated invariant the kernel stops; it never limps on. An insecure fallback (a guessable random seed, a missing signature) is a boot failure, not a warning (R17 (fail closed)).
• unsafe is a budget. Every unsafe block states the invariant it relies on; unsafe code lives in few, small modules with safe interfaces; the count is tracked by the bench and goes up only with a reason (the unsafe budget).
• The requester never influences the approval channel. Any convenience that puts approval inside a session must first amend this tenet.
• Non-interference across labels, by construction (label non-interference).

3. Rust, and assembly only where Rust cannot reach

• Everything that runs on the machine is Rust: the RustSBI firmware, the loader, the kernel, the servers and the applications, userland runtimes included. RustSBI is the only supported firmware and is always trusted.
• Assembly is limited to what the language cannot express (trap entry and exit, the context switch, the first instructions after reset) and is written inside Rust sources, never as prebuilt objects.
• No C, no C toolchain in the build, no binary blobs, and no bindings to C libraries. No C and no shell script runs on the machine. One exception, on the build host only: test oracles and fuzz drivers (the littlefs C reference, libFuzzer) may be C or C++, in crates outside the workspace build, never linked into anything that runs on the machine.
• This tenet governs what runs on the machine; the build host is outside it and may run shell scripts that drive the build, the bench and the tools. The reason: the tenet keeps what the adversary can reach auditable in one language, and a build-host script never runs on the machine; what it builds is signed and verified before it runs (R15).
• The build is one pinned toolchain (rustc and cargo), and reproducible.

4. Open, auditable standards

• Hardware interface: ratified RISC-V specifications only (the privileged architecture, SBI, the PLIC, Sv32 and Sv39, Sstc). A board’s vendor extension sits behind a capability with a standards-based alternative.
• Machine description: the device tree. Devices: virtio.
• Formats and protocols: published ones with independent implementations (ELF, tar, 9P2000, SSH, TLS). A format is invented only when no open one fits, and then it is specified in this book.
• Everything needed to rebuild and audit the system is public: sources, specifications, toolchain.

5. Dependencies are part of the trusted computing base

A crate linked into the kernel or the loader is our code, as far as the adversary is concerned.

• Reuse beats writing our own when the crate is small, no_std, pure Rust, maintained, and read. Otherwise we write the fifty lines.
• Privileged code keeps a short, reviewed dependency list, pinned by the lockfile and vendored. A new dependency there needs a stated reason.
• Servers have more latitude than the kernel; applications more than servers.
• A dependency that panics on malformed input is a denial-of-service bug in us.

6. Tested to hell and back

If it is not tested, it does not work; we just have not found out yet. The harness is part of the system, held to the same standard as the kernel (the test bench).

• One simple harness, real boots. The bench boots the real kernel under QEMU with chosen programs and judges the console. No mock of the kernel and no special test build of it; a build of the same sources with debug assertions and overflow checks on is the kernel checked harder, not a special build.
• Every behaviour has a case. New kernel or loader behaviour lands with a test; a bug fix lands with the test that would have caught it.
• Attack tests, not just happy paths. Hostile images, hostile call arguments, hostile messages, exhaustion, malformed device trees. The expected outcome is a clean refusal, never a kernel panic and never silent corruption. A verdict comes only from a party the attacker cannot impersonate (rule F).
• The harness can fail. It is checked against known-bad runs, so a green result means something; the model’s checks are shown to catch deliberate breaks (the model).
• Fuzz what parses. Anything that parses untrusted bytes (ELF, tar, the device tree, call arguments, messages) gets a fuzz target.
• A flaky test is a bug, in the test or in the system, and is fixed rather than retried.

7. Devices speak virtio

Drivers are virtio, unless the device is trivial (a UART, a real-time clock: small, no DMA). A driver that does DMA is in the trusted computing base unless the hardware confines its DMA; the platform states which. On hardware too messy to drive, Redoubt writes no drivers: it takes reserved cores and lets Linux run the hardware and serve virtio to it, and there Linux is trusted (Linux on reserved cores).

Every dimension we claim

A configuration the bench does not boot is not supported.

• Widths. Every milestone, M1 (sessions over SSH, kept apart) to M6 (persist, install, share), requires rv64 boots and rv32 compilation. Most kernel cases boot on rv32 as well; a full rv32 system is beyond M6.
• Harts. The kernel runs user code on every hart, up to 8, under one big lock, with a budget on one hart at a time until one process’s threads may run on several. M2 (usable shell) brings several harts: the kernel runs user code on every hart, first under one big lock, and one process’s threads on several harts at once, so a beamlet VM’s schedulers run in parallel (several harts). The reason: the FPGA platform’s cores have two hardware threads each, and by the end of M1 (sessions over SSH, kept apart) the kernel’s rules are attacked on one hart, so a second hart multiplies what can go wrong only in rules already attacked.
• Firmware. RustSBI’s prototyper, built from source, on both widths.
• Machine. QEMU’s virt machine, with virtio block, network and console devices.

Non-goals

These are not missing features. Each is left out because it would widen what an attacker can reach or what an auditor must read.

• No display, keyboard, mouse or GUI. The box is headless; people use SSH.
• No Unix signals, fork, setuid or root. A process is ended by destroying its budget; authority is only ever narrowed.
• No POSIX shell. The shell is Elixir.
• No symlinks or hard links. Namespaces are built from binds, per process.
• No swap and no IPv6.
• No inbound services except SSH, with SFTP and SCP inside it.

Changing a tenet

A tenet changes before the code does. The change is made on this page, with the reason next to it, and every page that rests on the old wording is updated in the same change. A proposal that conflicts with a tenet and does not amend it is refused. Weakening a guarantee, or moving a wall from “attacked” to “assumed”, needs the owner’s explicit decision.

The security register

This is where an audit of Redoubt starts. Every security property the book claims is one row below: what it is, the rule that states it, the code that enforces it, the tests that attack it, whether it is built, and what it leaves open. Nothing else is claimed. The rules are defined on the pages that own them; this register is derived from those pages, and the docs checker holds it to them (the test bench). The guarantees the rules add up to, and the walls they rest on, are on the tenets.

How to audit

1. Start from a guarantee on the tenets: capability closure, label non-interference, human control. Each names the rules it rests on.
2. Find the rule’s row. The Rule column links the section that defines it; read that section whole. It states the rule, says why, and opens with its status line. For example, R1 (flow) is the kernel’s half of label non-interference, and I7 (every flow obeys R1) is the model’s check of it after every step.
3. Read the enforcing code. The Enforced in column names the files where the rule is kept. The kernel’s files are small enough to read in full; each cites the rules it keeps.
4. Read the tests that attack it. A bench: test is tests/<name>.toml: most are a boot under QEMU whose verdict comes from a party the attacker cannot impersonate (rule F), and the rest run a host check and judge its exit status (wire-host-tests, for one, runs host tests; the kinds); a host: test is a Rust test in that crate; a mutation: is the rule deliberately broken in the model, which its checks must catch (the model); a fuzz: test is a fuzz target.
5. Read what is left open. “Built, partly tested” means the section’s status line names what no test attacks yet; the Residual risks column names what the rule does not stop, and links the page’s full list.

Status reads the same as on the pages (reading this book): built (every claim attacked by the tests listed), built, partly tested (the gap is on the page), or planned for a named milestone, with nothing built yet. Built means the code exists and its named tests pass. A host test or a build case is not a boot: a server whose rows are built from host tests is not thereby running in the integrated system, and running there is its own planned section on its page.

The walls

The rows fall into groups, one per wall of the prison. From outside in: the boot chain that decides what runs, the kernel that separates processes, the servers that separate principals, and the network that is the way out. Four walls are not the OS’s own: they are named, with what rests on them, below.

flowchart TB
    subgraph HOST["host: virtio emulation"]
      BOOT["Boot<br/>verified bundle, confined images, init's checks"]
      subgraph K["Kernel"]
        KI["IPC and objects"]
        KM["memory"]
        KB["budgets, scheduling and time"]
        KP["processes and devices"]
        KV["invariants (the model)"]
      end
      subgraph SV["Servers"]
        SL["the serving library and wire formats"]
        SS["the steward"]
        SK["keys, files and devices"]
        SP["packages and services"]
      end
      NET["Network<br/>netd, ipd, resolver, gatewayd, sshd"]
    end
    HUMAN(["the approval human"])
    OUT(["allowed egress"])
    BOOT --> K
    K --> SV
    SV --> NET
    NET --> OUT
    SS -.-> HUMAN

Figure: the register’s row groups as walls, outermost first. Solid lines are built, dashed lines planned. Side channels cross every box and are listed below.

The register

Residual risks by wall

What each wall leaves open, gathered from the pages’ residual risks. The four walls that are not the OS’s own are described on the tenets.

Boot.

• On QEMU the loader itself is not verified, and whoever controls the host’s files chooses what boots; the development signing key is public; there is no rollback protection until the version counter (boot, packages).
• The device tree is not signed, and the firmware is trusted. A device tree that hides a controller from the loader’s controller search and its device list defeats the kernel’s Ctrl check, whose list of controllers comes from the same tree (boot, devices).
• The boot bundle’s confidentiality is not claimed: seeds in it are readable by whoever reads the image (boot).
• A confined boot is checked once; a capability handed across label sets later is the handing server’s fault, not the kernel’s (init).

The kernel.

• System-class servers are trusted to check labels; the kernel checks only between user budgets (IPC).
• Destruction is uninterruptible kernel time, which follows the dying subtree (budgets, scheduling).
• A driver that programs DMA is trusted: there is no IOMMU, and reset-before-reuse does not confine a live driver (devices).
• Only virtio-mmio devices are reset: any other DMA device is never reset, so every process end that reaches it quarantines, and such a platform gets no driver restart (devices).
• A co-holder keeps its mapping of a quarantined device, and of a device whose handle was revoked: the kernel does not unmap device ranges (devices).
• A crash can blame nobody: corruption left by an answered call can crash a thread later, when it has no current call (processes).
• PIDs are one global pool that untaken exit notices can hold (processes).
• The kernel runs on one hart; completion races and flushes across harts are argued, not attacked (the kernel), until M2 (usable shell) brings several harts (several harts).

The servers.

• The named mediators, the steward and sshd, are trusted across the labels they serve (the steward, sshd).
• There is no non-collusion guarantee within one label set: agents with the same label set and each other’s handles can cooperate (the tenets).
• A dead launcher leaks its children’s connections until its own connection is freed, against its own account and label set (serving).
• An account-0 client can spend every bucket of a 9P server, and a server sized for fewer buckets than the label sets it serves is a channel (serving).
• Server work is paid by the server’s weight, not the requester’s (the servers).

The session. A session is per-principal code: a bug in it reaches that principal’s own capabilities, which the kernel contains (trust tiers).

• beamlet’s own code is memory-safe, but crates it links hold unsafe and parse hostile data (compressed streams, patterns, certificates) with the session’s authority, as any program’s libraries do. A memory bug there, reached by a file another principal wrote, an agent’s opened by its sponsor above all, has the sponsor’s session, whichever of its tools read it; the kernel keeps it to that principal, and keys and approvals out of its reach (beamlet, the shell).
• The terminal guard stops hostile text, not the session’s own code, which can write to its own console; and it draws the bidirectional marks, which only settle weak and neutral characters (the shell).
• The terminal guard draws every character that is there, not its likeness: a name made of look-alike letters (Cyrillic а for a) can still look like another (the shell).
• Ed25519 is checked cofactored everywhere on the box, so signatures are malleable; nothing that holds a wall takes one as an identifier (beamlet, boot).
• Until M6 (persist, install, share) a session has no wall clock and counts from 1970 at boot: a check that a date has begun fails, but a check only that one has not passed, a token’s expiry, passes whatever the token, and times from two boots cannot be ordered (beamlet).
• A console that stops answering a write stops the session’s VM, until writes move to its I/O threads (beamlet).
• A session makes a fixed number of waiting calls at once, and one past it is refused; memory off the Erlang heap, a large binary, is bounded only by the session’s own page limit (beamlet, the shell).

The supply chain.

• Vendored crates are checked against checksums taken from the tree itself: that proves they have not changed since vendoring, not that they match their upstream release (vendored dependencies).
• The vendored crates’ unsafe is outside the ratchet; recorded Miri runs cover their own tests and ipd’s (ipd under Miri).
• The unsafe ratchet counts only what its budgets name; it fails when a no_std workspace member has a source in no budget, but a member it lists as uncounted is trusted to be off the target (the unsafe budget).

The network.

• Upstream DNS answers are believed, and an allowed name’s address may host other services (the resolver).
• A shared ipd is shared state; connection rates are observable (ipd).
• The model service sees what an agent sends, and metering trusts the provider’s figures (gatewayd).

Walls the OS does not own.

• The approval human: the requester can persuade, repeat until the human tires, or phrase a request that reads one way and means another; an approved text can carry a hidden message, and a push is one human action (the tenets, the steward).
• Host virtio emulation: a bug in the host’s emulation reachable through a driver is outside the OS (the tenets).
• Allowed egress: every allowed channel out can carry data: a model API, a git remote, the upstream resolver’s shared cache (the tenets).
• Side channels: scheduling is observable, and so is server CPU spent on a caller’s behalf; every process has a perfect clock; CPU caches, the shared second-level cache and memory bandwidth are not partitioned; a shared server’s caches and the disk are shared unless the deployment is confined (scheduling, timer, the tenets).

Glossary

One vocabulary, used the same way on every page. Each entry says what the term means here, the nearest Unix idea where there is one (and how it differs), and the page that defines it. When a page and this list disagree, the page that owns the term is right and this list is fixed.

A/B slots

Two places for the signed bundle. An update writes the new bundle to the inactive slot, and the loader verifies it on the next boot; a system that does not boot, or does not reach a healthy state before any session starts, falls back to the other slot. A version counter kept outside both slots stops a rollback below it. Unix: A/B partitions on a phone. Defined in packages.

abandoned call

An open call whose caller has gone: it died, timed out, or was failed by revocation after the server took the call. The server keeps the call, and any lend, until it replies; the reply reaches nobody. Unix: none. Defined in IPC.

account

A 64-bit number carried by a budget that says which principal the budget bills to; 0 means none. A new budget inherits its parent’s account unless the parent has none. Servers see the caller’s account on every message. Unix: a user ID, but it grants nothing by itself. Defined in budgets.

agent

A program that acts for a principal and is assumed hostile: an AI agent or any other automated worker. It is its own principal with a sponsor, runs under a lease, and holds only capabilities narrowed from its launcher’s. Unix: none. Defined in agents.

approval

A human’s out-of-band yes to a request that would add authority or move data across a label boundary. The requester cannot draw, type or listen on the channel where it happens. Unix: none (sudo’s prompt is in-band). Defined in the steward.

attach root

The directory a 9P connection is rooted at. Nothing above it can be named through that connection. Unix: a chroot, per connection. Defined in the wire protocol.

attack case

A bench case that tries to break a security property and passes only on a verdict the attacker cannot produce: the kernel’s own output, a victim’s, or a clean power-off. Defined in the test bench.

badge

A 64-bit number attached to an endpoint handle, chosen by the server that minted it. The kernel delivers it with every message sent through that handle, so the server knows which grant is in use. Badge 0 is the receive right. Unix: none; closest to a file descriptor’s open-file description as the server sees it. Defined in handles and objects.

bench case

One test the bench runs: a file tests/<name>.toml that boots the real kernel under QEMU with chosen programs, or runs host tests or a source check. Defined in the test bench.

bind

Making a capability the process already holds appear at another path in its namespace. It creates no authority. Unix: mount --bind, but per process and with no global mount table. Defined in files and binds.

boot manifest

The one strict-JSON file in the signed bundle that tells init which servers to start, with which devices, labels, weights, volumes and arguments, and which principals exist. Unix: /etc/fstab, /etc/inittab, /etc/passwd and the service files, as one signed document. Defined in init.

boot pack

One file on the verified system volume, boot.pack, holding again the modules and resources the shell loads to its prompt, behind an index of name, offset and length. beamlet reads it whole before its VM starts and takes those names from it, in place of one lookup each; any other name is the volume’s file. It is per VM and never written at run time. Unix: none close; a little like an initramfs that is only ever read whole. Defined in beamlet on Redoubt.

budget

The kernel object that holds resources: page, process and CPU-weight limits, a class, a label set, an account and an optional deadline. Every process runs in one; every kernel object is charged to one; destroying one revokes everything under it. Budgets form a tree. Unix: a cgroup, a revocation list and a security label in one object. Defined in budgets.

bundle

The signed archive the loader boots: the kernel, init, the boot manifest, every other server’s program and any data entries. Defined in boot.

call

A message that waits for a reply. It may lend pages to the server for the length of the call. Defined in IPC.

capability

The right to use something, held as a handle. There is no other authority: no user IDs, no paths that grant access by name, no root. Unix: a file descriptor, if file descriptors were the only way to reach anything. Defined in handles and objects.

carve

Giving part of a budget’s limits to a new child budget. The children’s limits never add up to more than the parent’s. Unix: none. Defined in budgets.

class

system or user, fixed for a budget and inherited by its children. It decides trust (a flow into a system budget is not label-checked by the kernel) and never scheduling order. Defined in budgets.

commandlet

One of the shell’s commands (cat, cp, grep): an Elixir function declared once, with defcommand, with typed parameters and its help, which it does not compile without. Imported at the prompt and called as plain Elixir. Unix: a shell builtin, but an ordinary function with no syntax of its own. Defined in the shell.

confined deployment

A boot in which init refuses any manifest that lets two different label sets share a server instance, volume, endpoint, network instance or device, except the two named control-plane mediators. The kernel and the cores stay shared. Defined in init.

connection

One client’s session with a server: an endpoint handle with its own badge, and the server state keyed to it (for 9P, its fid table). Copies of the handle share the connection; a launcher gives each child a fresh one. Unix: an open socket or file description. Defined in the servers.

context

A named session of one principal in one label set, chosen by the SSH user name: ssh alice.work@box is Alice’s context work, ssh alice@box her default one. One session at a time. Defined in sessions and namespaces.

crash blame

When a server crashes while working on a call, the exit notice names the account and labels of that call’s sender. The steward counts blame and ends sessions that keep crashing shared servers. Defined in processes.

current call

The open call a server thread is working on: the call its last receive took, or the one it named with serve; none once it replies to it or receives anything else. A crash blames its sender. Defined in IPC.

declassification

Moving one item of data out of a label to an unlabelled volume, done only by the steward after the label’s owner approves that exact snapshot out of band. Unix: none. Defined in the steward.

device object

The kernel’s record of one device resource: an MMIO range (possibly able to do DMA), an interrupt line, or the right to power off. A driver reaches a device only through a handle to one. Unix: a device node, but held as a capability rather than found by path. Defined in devices.

DMA

Direct memory access: a device reading and writing RAM itself. A driver that programs DMA is trusted unless hardware confines it. Defined in devices.

endpoint

The kernel object clients call and servers receive on. It holds no queue: its waiting messages are its blocked senders. Unix: a listening socket, with the badge in place of the peer address. Defined in IPC.

escape room

The standing game in which real agents, told to get out, attack a confined deployment while a referee decides from the record, never from an agent’s own output. It tests what nobody thought to write a bench case for. Unix: none; a capture-the-flag run continuously. Defined in agents.

exit notice

The message the kernel sends to a process’s exit endpoint when it exits, faults or is killed: its PID, cause, code, and who is blamed. Unix: SIGCHLD and wait, as a message. Defined in processes.

fid

A number a 9P client uses to name a file it has walked to, within one connection. Unix: a file descriptor, scoped to the connection. Defined in the wire protocol.

fixed sub-budget

One of the budgets the steward splits a principal’s top budget into at boot, one per label set the manifest names for that principal. Every session and lease of one (principal, label set) is carved from its own sub-budget, so a vault’s activity never shows in what the unlabelled side can carve. Unix: none. Defined in the steward.

founding handle

The root badge of a server that is filled once at setup and then only served: bootfsd’s is the one init uses to add the public entries and seal them. No connection minted for a client can fill it. Unix: none. Defined in bootfsd.

gateway

A server that does a network job for an agent so the agent never holds a socket or a key: TLS, credentials, request checks and logging. gatewayd is the first. Defined in gatewayd.

gateway capability

A connection to gatewayd whose badge names one grant (the model gateway, a git remote), optionally narrowed to some of its hosts, with a meter. It is what an agent holds instead of a socket. Unix: none; closest to a scoped API token the holder can use but never read. Defined in gatewayd.

grant and release

The two operations of a typed protocol that mints a narrower capability for a client: a grant replies with the new endpoint handle and a random id; a release frees it by that id, and only for the client that received it. A 9P server’s pair is new_connection and disconnect. Unix: open and close, where only the opener may close. Defined in the wire protocol.

handle

An index into a process’s handle table, which the kernel holds. It names an object, a badge and a stamp. It cannot be forged; it can be copied and closed. Unix: a file descriptor. Defined in handles and objects.

hart

A RISC-V hardware thread: one core, or one thread of a multithreaded core. Unix: a CPU.

job

The native stages one shell command started, each running in a budget of its own carved from the session’s. Killing a job destroys those budgets; there is no signal. Unix: a shell job, killed by budget destruction rather than SIGKILL. Defined in native programs.

label

A name owned by a principal, marking data that must not leave a set of budgets. The kernel sees it as a 64-bit number. Defined in the servers.

label set

The labels on a budget, fixed when it is created. It is the isolation unit: two budgets with different label sets have no path between them that the OS carries, except through the steward’s approved moves. Defined in IPC.

lease

A budget with a deadline, made by the steward for an agent or session. When the deadline passes, the kernel destroys the budget and everything in it; the sponsor can end it sooner. Unix: none. Defined in the steward.

lend

Pages a caller hands to a server for the length of one call. They leave the caller’s address space until the reply brings them back. Defined in IPC.

loader stub

A small program mapped into a new process that reads the program’s ELF image and maps its segments, so the launcher never parses an ELF. Unix: the ELF loader in execve, moved out of the kernel and the parent. Defined in init.

meter

The part of a gateway capability that says how much the holder may spend: tokens and money, carved from its principal’s own. Unix: a quota. Defined in gatewayd.

mint

Making a new endpoint handle with a chosen badge, and optionally a narrower stamp. Only the holder of the receive right can. Defined in handles and objects.

model

The executable model: the Rust crate redoubt-model, which states the kernel’s objects, calls, rules and invariants as code, drives them with random call sequences and checks every invariant after each step. Its traces replay on the real kernel. Unix: none. Defined in the model.

mutation

A deliberate break of one rule planted in the executable model, to show the model’s checks catch it. Defined in the model.

name rules

What a resolver connection may have answered: an allowlist of domain names and suffixes, and a blocklist that subtracts from it and always wins. A suffix matches only at a label boundary. A grant only narrows them. Unix: none; closest to a filtering DNS proxy per client. Defined in the resolver.

namespace

A process’s own map from path prefixes to capabilities, built by its launcher. Nothing is inherited and there is no global file tree. Unix: a mount namespace with no root to fall back on. Defined in sessions and namespaces.

native program

A Rust program built for Redoubt and started from a session in a budget of its own, through the loader stub, with the namespace its launcher binds. Unix: an executable, but with no inherited descriptors or environment. Defined in native programs.

9P

The Plan 9 file protocol (9P2000), used for every service a person or program sees as files. Defined in the wire protocol.

open call

A call a server has taken with receive and not yet replied to. Each costs the server a page and counts against its limit of open calls. Defined in IPC.

pass

A budget’s position in the stride scheduler: the lowest pass runs next, and running raises it in inverse proportion to the budget’s weight. Defined in scheduling.

person

A principal who is a human: logs in with a key over SSH and can approve. Only a person gets name-scoped TCP, and every chain of sponsors ends at one. Unix: a user. Defined in the steward.

physmap

The kernel’s mapping of all RAM at a fixed offset, so it can reach any frame. Supervisor-only and never executable. Defined in memory layout.

PID

A process’s number, 2 to 64 (1 is the kernel), which is also its hardware address-space id. It is drawn at random from the free ones and held until the process’s exit notice is taken or dropped. No authority is keyed by it. Unix: a PID, but it names; it grants nothing. Defined in processes.

pipe

A file that somebody serves over 9P, bound into two programs’ namespaces as one’s standard output and the other’s standard input. There is no pipe object in the kernel and no inherited descriptor. Unix: pipe(2), as a served file. Defined in native programs.

powerbox

The steward’s service that grants authority a principal lacks, or confirms a principal’s own high-stakes step, through an out-of-band approval, and if approved hands back a narrow capability. Unix: none (sudo grants everything and asks in-band). Defined in the steward.

principal

A named, accountable identity the steward knows: a person, an agent or a project. It has an authentication method, a set of capabilities and an audit identity, and its top budget carries its account. Unix: a user account, without root and without ambient rights. Defined in the steward.

profile

The package versions a principal runs, and so the /bin its sessions see. It is a steward record, not a file in the principal’s space. Unix: a Nix profile. Defined in packages.

project

A principal sponsored by several members, with its own budget, volume, package directory and profile, and optionally a label. Membership is capabilities minted into a revocation scope per member. Unix: a group, but with its own budget and no ambient rights. Defined in the steward.

purpose

The one message shape a keyd badge may have its key sign: ssh_host signs only an SSH key exchange, audit only an audit record. No purpose signs a caller’s own bytes. Unix: none; closest to a key usage extension. Defined in keyd.

push

Moving one item from an unlabelled volume into a labelled domain’s volume, triggered by the label’s owner out of band. The mirror of declassification, and the only way input enters a confined labelled domain. Unix: none. Defined in the steward.

quarantine

What happens to DMA pages and devices when a device in the reset set does not confirm its reset: the pages are mapped nowhere and never reused until the machine resets, still charged to their budget, and the device’s object is destroyed and none names it again until reboot. Unix: none. Defined in devices.

reader budget

A short-lived budget the steward creates carrying exactly an item’s labels, with a deadline, to read that item for it: the steward stays unlabelled and calls it. There is no standing reader. Defined in the steward.

receive right

An endpoint handle with badge 0. Only it can receive, and only its holder can mint. Defined in IPC.

revocation scope

A budget with zero limits, made only to be a stamp and later destroyed, so a grant can be revoked without killing any process. Defined in budgets.

root badge

A badge below the minted range that a server’s setter-up gives meaning to (the manifest, through init), rather than one the server minted for a client. It is how system callers get separate shares and how setup-only operations are reserved. Defined in serving.

scope

The IP prefixes and ports an ipd connection may reach. A grant only narrows it, and no scope reaches the box’s own addresses. Unix: none; closest to a per-socket firewall rule. Defined in ipd.

screen buffer

A grid of cells beamlet holds natively for one screen program, written with a few primitives and diffed into the cells that changed; the only way a screen’s text reaches the terminal. Unix: a curses window, but with no escape sequence in it. Defined in beamlet.

screen program

A full-screen program of the session (the pager, the editor, a chooser): an Erlang process that draws into a screen buffer and is sent its keys by the shell’s driver. Unix: a curses program, but in the session’s VM, not a process of its own. Defined in the shell.

seal

The message that ends a server’s setup: before it clients see nothing; after it the contents are fixed for good. bootfsd is sealed once its public entries are added. Defined in bootfsd.

self set

The addresses that are the box itself: its own address, its network and broadcast addresses, loopback, “this host”, multicast, class E and the prefixes named as the host’s. ipd refuses them before any scope is looked at. Defined in ipd.

send

A message that does not wait for a reply. It may transfer pages to the receiver for good. Defined in IPC.

service record

The steward’s record of one installed service: the package’s program, its owner, the grants the owner made for it, a budget carved from the owner’s and a restart policy. The supervisor starts services only from these. Unix: a systemd unit, holding grants rather than a user name. Defined in the supervisor.

session

A person’s or agent’s working environment on the box: an Elixir VM in its own budget, with a namespace and capabilities the steward built for it. Unix: a login session. Defined in sessions and namespaces.

sink

A server whose output leaves a principal or the machine (ipd, gatewayd, sshd). A sink is cleared for no label and refuses every labelled caller, with one exception: sshd, on the channel whose owner authenticated it. Defined in the servers.

sponsor

The principal accountable for an agent: a person, or an agent with a person at the top of the chain. The agent’s budget sits under the sponsor’s, and the sponsor can always end its lease. Defined in agents.

stamp

The budget recorded in a handle: destroying that budget, or any budget above it, closes the handle everywhere. Defined in handles and objects.

startup block

The read-only page a launcher gives a new process: its namespace, named handles, arguments and the location of its image. Unix: argv, envp and the inherited descriptors, in one checked record. Defined in init.

steward

The trusted server that knows principals, authenticates them, builds sessions, grants leases, runs approvals and keeps the audit log. Defined in the steward.

TCB

The trusted computing base: the code whose failure can break the security guarantees. For Redoubt: the firmware interface, the loader and the kernel, plus any server that programs DMA without hardware confinement. Defined in the kernel.

TID

A thread’s number within its process, 1 to 31; the first thread is 1. Defined in processes.

transfer

Pages given away with a send: they leave the sender and become the receiver’s. Defined in IPC.

trust domain

The budgets that share one label set. Within it, delegation is permitted; across it, only the steward moves data, one approved item at a time. Defined in the tenets.

trust list

The signing keys whose code a principal runs. The steward launches code on a principal’s behalf only if a key on its trust list signed it. Unix: an apt keyring, per principal. Defined in packages.

typed message

A message whose word 0 names an operation in a table, encoded by generated code, as opposed to a 9P message. Defined in the wire protocol.

vault session

A session carrying one of its principal’s labels, so it can read that label’s data and cannot send it anywhere unlabelled. Opened with ssh alice+X@box. Defined in sessions and namespaces.

verdict

The line a bench case passes or fails on. It must come from a party the attacker cannot impersonate. Defined in the test bench.

W^X

No RAM page is ever both writable and executable, under any mapping; the kernel’s own mappings keep the same rule. Device memory is a stated gap. Defined in memory.

weight

A budget’s CPU share. The scheduler uses its free weight: its limit less what its children carved. Defined in scheduling.

wire table

A Markdown table in libs/wire/tables/ that defines one typed protocol; the Rust and Elixir codecs are generated from it. Defined in the wire protocol.

writer budget

A short-lived budget the steward creates carrying exactly a target label set, to write one pushed item into that domain, since a write needs equal labels. Defined in the steward.

XLEN

The register width: 32 bits (rv32) or 64 bits (rv64). Every milestone boots rv64 and compiles rv32.

The kernel

The Redoubt kernel is a small RISC-V microkernel in Rust. It keeps five things: memory, threads, IPC, interrupt delivery and the timer. Everything else (drivers, file systems, the network, policy) is an unprivileged server that reaches the kernel only through handles and the 26 system calls. The kernel runs in S-mode under RustSBI firmware, one binary for rv64 (Sv39) and rv32 (Sv32). This page says what the kernel keeps, names its objects, measures the trusted computing base, and maps each source file to the page that documents it.

Purpose

The kernel is the part of Redoubt every other guarantee rests on, so it has to be small enough to read in full (TENETS). A reader who wants to audit it needs three things first: what the kernel is responsible for and what it refuses to hold, the objects it hands out and how they refer to each other, and where the code for each rule lives. The pages below this one each take one mechanism; this page is the map.

What the kernel keeps

Status: built · partly tested: that no driver, file system or policy sits in the kernel is read from the source map, not attacked by a case · tested: bench:no-cruft, bench:legacy-gone

Budgets pay for all five: every object, page, process and share of the CPU is charged to one, and destroying one revokes everything under it (budgets, R10 (destruction)). The budget calls are budget_create, budget_destroy, budget_reap (destroy one child, keep the budget) and budget_usage. Two calls sit outside the five jobs. random returns 64 bits from the kernel’s ChaCha8 generator, keyed from the loader’s Seed argument; the kernel also draws PIDs from it. system_reset powers the machine off or reboots it through the firmware, and only a holder of the Reset device object can call it.

The kernel holds nothing else:

• No drivers. Its own console is the SBI debug console. Every real device (UART, virtio block, virtio net) belongs to a userspace server that holds its device object. The console’s UART is shared: its holder takes the console’s hold around each write, and the kernel’s lines wait, whole, for it (the console’s one writer).
• No names. The kernel knows handles, never paths, file names or server names. A process reaches only what its own handle table holds.
• No program loading. The loader places the kernel and init at boot. After that a launcher builds a process with process_map and process_start, and a loader stub inside the new process reads its ELF image (boot, processes).
• No policy. The kernel enforces R1 (flow) on label sets and the budget limits. Who gets which label, lease or capability is decided by init and the steward.

There is one call table. A number in a0 outside it is InvalidArgument, whatever the other registers hold (ABI). The kernel never calls into user code and never switches straight from one process to another. User mode is entered two ways (resuming a thread, or returning from a call) and left one way (a trap), so every instruction a process runs is counted against the budget the scheduler picked (R12 (scheduling)). The kernel runs on every hart, with interrupts off while it runs, under one FIFO lock that a hart takes at its trap from user mode and gives up at its return or idle. Each kernel global (the memory manager, the process table, the timer, the generator) sits in a KernelCell of its own (kernel/src/cell.rs): a run-time-checked borrow under that lock, so a nested borrow is a panic, not two live references. A checked build asserts that the hart reaching it holds the lock; a release build does not check, and rests on the trap paths taking it.

bench:no-cruft reads the sources and fails on a name from a list of call-interface identifiers Redoubt does not have, on a silenced dead-code warning (allow(dead_code) or allow(unused)) in the kernel, the loader, paging, redoubt-layout or the test programs, on a Cargo feature no cfg(feature) reads, and on a second literal definition of PAGE_SIZE or USER_AREA_END. Every exemption is an entry in the case with its reason, and an exemption that covers nothing fails the case (test bench). bench:legacy-gone makes the calls such an interface would take, from user mode, and checks that each is refused and that nothing it asked for happened: no mapping, no callback run, no switch.

The objects at a glance

A process holds handles: indices into a handle table that only the kernel writes. A handle names an object, a badge (a 64-bit number the minting server chose; 0 for the receive right) and a stamp (the budget whose destruction closes the handle everywhere, R9 (stamps)). Index 0 is never a handle. There are four kinds of object:

Each object lives in a RAM frame of its own. Every lookup compares the id in the frame with the id in the handle, and a mismatch stops the kernel rather than naming a reused frame (I1 (handles name live objects)). Threads, handle-table pages and open calls are not objects: no handle names them. A thread is named by its process and its TID (1 to 255). Details, costs and mint are in objects.

flowchart LR
    H["handle<br/>(object, badge, stamp)"]
    P["process<br/>address space, handle table,<br/>exit slot"]
    T["thread<br/>TID 1 to 255"]
    E["endpoint"]
    D["device object<br/>MMIO, IRQ or Reset"]
    B["budget"]
    P -- "holds, in its table" --> H
    H -- names --> B
    H -- names --> E
    H -- names --> D
    H -- names --> P
    H -- "stamp: closed when destroyed" --> B
    T -- "belongs to" --> P
    T -- "blocked sender:<br/>a queued message" --> E
    P -- "runs in, pays for<br/>threads and memory" --> B
    P -- "object page charged<br/>to the creator's" --> B
    P -- "exit endpoint" --> E
    E -- "owner (R1, charged)" --> B
    D -- "owner (charged)" --> B
    B -- "parent, carved from" --> B

Figure: the kernel’s objects and what each refers to. An arrow points from the one that holds the reference to the one it names.

Containment

Status: built · tested: bench:kernel-containment

One boot, bench:kernel-containment, shows that the kernel’s primitives alone contain hostile code before init, the steward or any server is built on them. Hostile code in a lease is preempted, then ended at its deadline or revoked by hand while its messages and lends are in flight, and its victims stay responsive the whole time. The boot is evidence for the kernel only. Sessions have their own cases (M1 (sessions over SSH, kept apart)), and the steward’s leases, approvals and the network theirs (M3 (agents, approvals and the attack suite)).

What runs. The loader starts one program. It holds root, system, users, the console and the Reset right. It builds the budget tree at the weights init gives (init) and starts copies of itself in the tree, as the latency workload does (responsiveness):

• in system: the workload’s driver stand-in and steward stand-in, and a victim server that takes the hostile agents’ calls and holds them open;
• in users: a bystander session, and a sessions budget the steward stand-in holds. The steward stand-in carves each lease from that budget and starts a hostile agent in it, as the steward will.

Each hostile agent runs in a lease the size of the workload’s leases, with room added for a full handle table and one sub-agent. It does all of these at once:

• some of its threads spin and never enter the kernel, and one enters the kernel in a tight loop;
• some threads call the victim server with lends, which the server takes and holds open, and others are blocked in send to it. All of them go through handles minted into the lease’s revocation scope;
• a sub-agent runs in a budget the agent carves from its lease. That budget has a later deadline of its own, and the sub-agent’s process churns threads and processes;
• the agent fills the rest of its lease with endpoints and its handle table up to MAX_HANDLES, so the destruction walks as much as a lease of its size can make it walk.

The bystander also holds a message queued at the victim server that carries a handle stamped with a live lease. The hostile leases come in pairs, one of each kind. One ends at its deadline while the other lives, so two hostile leases are live at every deadline’s end. The steward stand-in then ends the other with budget_destroy after a timeout, which is its decision; that lease is the only one live at its end. Each pair is replaced when both have ended, until nine of each kind have ended.

Verdicts. None of them comes from a hostile agent:

The program’s lines are trusted (rule F) because it owns the console and holds the reset. Its children hold no device and have no path to the console, so no line on it can come from a hostile agent. Each victim reports through a handle the program badged for it, and the program never counts a hostile agent’s report as a verdict.

The run. The boot runs on rv64 and rv32, at the bench’s hart count, one and two in the gate, in a checked build with the tracing kernel (R23 (no test channels)). Its trace ring is 256 MiB (sched-trace-large, at 576 MiB of RAM), not the usual 64: at the 1 ms slice the run writes about ten records a slice, some four million at one hart and seven million at two, and a trace that drops one fails the gate. It uses the latency workload’s virtual time and one pinned seed. Sweeps of 16 seeds on both widths, at one hart and at two, set which seed the gate runs, and this page records them. The targets are the ones in responsiveness, and the gate adds none. If the gate misses one of them, that is a finding against the kernel, not a reason to set a new target.

The sweep at one hart (with the 192 MiB ring then) ran all 16 seeds on both widths, and every run passed. The table gives each run’s net p99 of the deadline notice, R10’s p99 and a lease’s end (the decision wake’s net p99 plus R10’s), in µs, against targets of 40000, 30000 and 125000:

The deadline notice is the target closest to its limit, at 65% in the worst run, and every seed lands within 1.5 ms of the others. An earlier version of the gate showed a second group about 10 ms higher on some seeds. The steward stand-in then polled for its notices in 200 ms waits, and when one ran out just before a deadline, the stand-in was runnable rather than waiting when the notice came, so another party ran a slice first. It now waits in one receive bounded by the deadline. At one hart seed 13 is the worst on both widths for the deadline notice (26197 µs on rv32, 25794 µs on rv64) and a lease’s end, and on rv32 for R10; rv64’s worst R10 is seed 16, at 22385 µs.

At two harts every target is met on all 16 seeds on both widths; the deadline notice’s p99 is 4 to 7 ms above its one-hart value, and R10’s 1 to 1.5 ms. The bystander’s share of the charges (its one thread is owed a hart, 500 of 1000) fell in two modes by the hart it landed on: the one that waited longer for the lock and took the audits, or the other, 445 or 543 to 546 on rv32. With a wait behind another hart’s audit billed to no one it reads 464 on rv64 and 442 on rv32 on the default seed, so at two harts the share is still reported, not judged (@1; scheduling). In µs, against the same targets, before that change:

The case file pins one seed for both widths and both hart counts: the gate runs seed 4, the worst at two harts or within a millisecond of it on both widths: the deadline notice on rv64 (31641 µs; rv32’s worst is seed 3, 3 µs above), R10 on both (23221 and 23908 µs) and a lease’s end on rv32 (28252 µs; rv64’s is seed 9, 27090 µs). At one hart it is 25939 µs on rv32 and 25258 µs on rv64 for the deadline notice, within 0.6 ms of seed 13.

The gate replaces none of the focused cases. budget-deadline, redoubt-revoke, uaf-lent-page, endpoint-destroy-open-calls and sched-latency each attack one clause alone, and each fails with a narrower message. The gate shows that all of those clauses hold together, under load, against one party that tries them all at once.

The TCB and its size

Status: built · partly tested: the inclusive line counts in the table are snapshots, not pinned by a case · tested: bench:unsafe-budget, bench:docs, bench:size-budget, host:testbench::actual_source_counts_still_enforce_the_budget, host:testbench::every_configured_root_must_contain_rust_source

The trusted computing base (TCB) is the code whose failure can break Redoubt’s guarantees: the firmware interface, the loader and the kernel, with the libraries they link, plus any server that programs DMA without hardware to confine it (devices). Lines are every line of the .rs files under the path, comments and in-file tests included, as the ratchet walks them.

Without the firmware, the TCB Redoubt writes is 28,921 lines. The kernel’s unsafe is split three ways in the ratchet:

Trap entry and context restore are global_asm! in arch/riscv/asm.rs, which the ratchet lists but which holds no unsafe keyword. redoubt-sys’s three are the ecall itself, the unsafe trait Transport whose contract the runtime’s unsafe rests on, and Ecall’s implementation of it. redoubt-layout, redoubt-stride and redoubt-signing say #![forbid(unsafe_code)], so their budgets can only stay at 0.

The unsafe counts on this page are kept true by the docs checker: every count in a `unsafe` (pinned) column must equal the ceilings in tests/unsafe-budget.toml, summed over the budgets under a row’s paths or read by a row’s budget name, so a change to a ceiling fails bench:docs until this page follows it (docs checker).

bench:unsafe-budget does not boot. It counts every use of the word unsafe outside a // comment in each budget’s paths, and fails if a count is over its ceiling, or if any use lacks a justification: a // SAFETY: comment within 6 lines above a block, or a # Safety doc section within 16 lines above an unsafe fn, impl, extern or trait. Every ceiling in the TCB equals its count and allows 0 undocumented uses, so one more unsafe anywhere in it fails the case. A budget whose path holds no Rust source fails too, so a moved directory is not silently uncounted (test bench).

Source map

Status: built · partly tested: the map is checked by reading the source, not by a case

Every file in kernel/src, and each library the kernel links, is documented on one page (or two, where a file serves two mechanisms).

Residual risks

• RustSBI is TCB and outside the ratchet. The firmware runs in M-mode below the kernel. It is vendored at a pinned commit and built with only QEMU virt’s drivers, but its unsafe is not counted, and QEMU loads it outside the signed bundle, so verified boot does not cover it (boot).
• Third-party crates in the TCB are outside the ratchet. The kernel links riscv, sbi-rt, plic and rand_chacha; paging links bitflags; the loader links fdt-rs, elf, tar-no-std, crc, sbi-rt and an Ed25519 verifier. They are pinned by Cargo.lock and are TCB like the rest (TENETS), but no case counts their unsafe.
• The ratchet counts words, not soundness. It checks that a SAFETY: comment is near each unsafe, not that the comment is true, and it counts only the paths its budgets list: a TCB file no budget names is not counted, and the case cannot notice (test bench).
• The table’s inclusive line counts are snapshots. The size budget has separate ceilings for shipped code lines, excluding comments and tests, and fails if a trusted crate grows past its ceiling (the size budget).
• Several harts, one lock. Every hart runs user code, one process’s threads on several harts at once, under one kernel lock (bench:smp-boot, bench:smp-shootdown); completion races between harts are not attacked by a case (IPC). Finer locking is M2 (usable shell)’s later step (several harts).
• The containment gate is one workload. Containment runs hostile leases of one size, against stand-ins for the steward and a driver, at one hart and two and under one pinned seed. It shows that the kernel’s primitives hold together for that workload. It does not bound every workload, and it says nothing about the real steward. The steward reruns the responsiveness measures with its real servers (M3 (agents, approvals and the attack suite)).
• The kernel trusts the loader’s handoff. It reads the argument block through a pointer the loader passed and trusts the memory map in it. It checks the device list itself (no device may overlap RAM or an interrupt controller), and it checks its own mappings are W^X before the first process runs (R19 (kernel W^X)). The loader is TCB for the rest (boot).
• Test builds carry more. The kernel source has features only some bench cases turn on: sched-trace, walk-trace, lock-trace, hold-trace, block-trace, dma-reset-deaf, sum-probe, panic-in-print and smp, and sched-inject-tie-fault for a recorded negative run. A production build leaves them off (R23 (no test channels)); a kernel built with them is not the kernel this page measures.

Why

• Five jobs, because each needs privilege. Page tables, trap entry and the context switch, the stamp on a message’s sender, the one interrupt controller and the one hardware timer can only be done safely by code no process controls. A driver, a file system or a policy can run unprivileged, so it does: a bug there reaches only what its server’s handles reach.
• One call table, no compatibility layer. Two call interfaces are two sets of argument checks to audit and two ways into every object. Redoubt carries one, and bench:no-cruft keeps the tree from growing a second, or dead code, or a feature nothing reads. For the same reason each shared constant has one literal definition.
• No callbacks, no direct switch. A kernel that calls into user code, or hands the CPU from one process straight to another, runs code on a budget the scheduler never picked, and a callback that never returns holds the CPU for ever. With two ways in and one way out, every instruction is charged and every slice ends.
• Count unsafe, not just lines. unsafe is where Rust’s checks stop and a reader’s must start. A ceiling that only goes down, with a written reason beside each use, keeps that part small and said out loud.
• Objects in frames of their own. Each object is one page charged to a budget, so there is no kernel table whose size one budget could exhaust for another, and destroying a budget can free everything it paid for.

Handles and objects

A handle is how a process holds authority: an index into a table the kernel keeps for that process, naming one kernel object together with a badge and a stamp. The kernel has four kinds of object (budgets, endpoints, devices and processes), each one page of RAM charged to one budget. Handles carry no rights bits: whoever holds one may use it in full. A server narrows a grant by minting a handle whose badge means less, and a grant is revoked by destroying the budget its handle is stamped with.

Purpose

Apart from its own memory and threads, the clock and random numbers, a process reaches everything through a handle: a server through an endpoint, resources through a budget, a child through a process handle, hardware through a device. So a process’s handle table is the whole of what it may do beyond itself, and three questions decide whether that is safe. Can a process name something it was not given? It names only indices into its own table, and only the kernel writes the table. Can a grant outlive the decision to revoke it? Every handle is stamped with a budget, and destroying that budget closes every copy. Can holding objects and handles use up memory someone else needs? Every object and every table page is charged to a budget. This page describes those three walls and the tests that attack them.

Interface

The four object kinds

Nothing else is an object: no handle names a thread, a page or an open call. Threads are named by their TID within their process, pages by address, open calls by message id.

Each object lives in one RAM frame of its own. The frame’s first word marks its kind, and its second is the object’s id, drawn from one 64-bit counter that never repeats, so no two objects of any kind ever share an id (I12 (ids never reused)). That frame is the page the cost table charges. No call destroys an endpoint or a device: each dies with the budget it is charged to, and a DMA device also when its reset fails (Residual risks).

Handles

A handle is an index into the calling process’s handle table. The slot at that index holds:

• the object: its kind, its frame and its id;
• the badge, a 64-bit number. For an endpoint, badge 0 is the receive right and any other badge was chosen by whoever minted the handle (mint). Handles to budgets, processes and devices carry badge 0;
• the stamp, the budget whose destruction revokes the handle (R9).

Indices start at 1. Index 0 is never allocated: in a register or a record slot it means “no handle”, for an optional argument left out or a message slot whose handle was revoked. An index that is 0 where a handle is required, wider than 32 bits, or not in the caller’s table is BadHandle; a handle of the wrong kind for the call is WrongObject. A process cannot read its table: it learns nothing of a handle’s object, badge or stamp except by using it.

A handle is four 64-bit words. A slot adds two chain entries of two words each (below), so it is eight words, 64 bytes, on both widths, and a 4 KiB table page holds HANDLES_PER_PAGE (64) handles; a compile-time check in kernel/src/handle.rs confirms that 64 slots fill one page exactly. Index i is slot (i - 1) mod 64 of table page (i - 1) / 64. A table has at most MAX_HANDLES (4096: 64 pages) handles. A message’s copy of a handle is the four words alone.

---
config:
  packet:
    bitsPerRow: 64
---
packet-beta
title one slot: eight 64-bit words, 64 bytes, so 64 slots fill a 4 KiB table page
0-27: "object's frame"
28-55: "stamp's frame"
56-63: "kind"
64-127: "object's id"
128-191: "badge"
192-255: "stamp's budget id"
256-319: "object chain: previous link"
320-383: "object chain: next link"
384-447: "stamp chain: previous link"
448-511: "stamp chain: next link"

The kind is 0 for an empty slot, 1 a budget, 2 an endpoint, 3 a device, 4 a process. A link is 0 for none, the head’s frame with the top bit set, or the holder’s PID and the index. Figure: a handle as the kernel stores it. A compile-time check confirms every frame index fits its 28 bits.

A handle dies when the object it names goes or when the budget that stamped it does. The two chain entries let a destruction find it without reading every table (residual risks). When a handle arrives in a table, the kernel walks up from the holder’s budget, at most MAX_DEPTH steps, and enters the slot:

• in the object chain of the budget its object is charged to, if the holder is outside that budget’s subtree (a budget handle’s object is the budget itself); a handle to a process object is entered in that object’s own chain wherever it is held, since the object can be freed while its creator lives;
• in the stamp chain of its stamp, if the holder is outside the stamp’s subtree.

A handle held inside dies with its holder’s table, which goes whole when the holder ends. Each chain is doubly linked, from a head word in the budget’s or process object’s frame, so adding or closing a handle costs a constant and using one costs nothing more. Beside its two handle chains’ heads a budget’s frame holds two more heads, of its charged chain and its counted chain of process objects; each process object carries a pair of links for each, beside the pair that puts it on its exit endpoint’s lists (what objects cost).

A new handle takes the lowest free index. A table page is a frame of its own, allocated and charged one page to the process’s budget when its first handle arrives, and freed when its last handle goes. Handles are never moved to fill holes, so an index stays valid until it is closed, and a table with holes costs one page per table page in use. A table already holding MAX_HANDLES handles refuses one more with TooLarge, which a caller can tell apart from its budget being unable to pay for the next table page (OutOfMemory). At delivery, a handle that would take the receiver past MAX_HANDLES is a cost it cannot pay, and the sender gets Refused (R4 (delivery)).

flowchart LR
    subgraph T["process P's handle table: index, object, badge, stamp"]
        direction TB
        h1["1: budget B, badge 0, stamp system"]
        h2["2: endpoint E, badge 0, stamp system"]
        h3["3: endpoint E, badge 5, stamp S"]
        h4["4: process Q, badge 0, stamp system"]
        h5["5 to 64: empty"]
    end
    subgraph O["kernel objects"]
        direction TB
        B["budget B"]
        E["endpoint E"]
        Q["process Q"]
    end
    h1 --> B
    h2 --> E
    h3 --> E
    h4 --> Q

Table page 0 holds indices 1 to 64 in one frame, charged to P’s budget; table page 1 (65 to 128) has no frame until a handle needs index 65; table page 63 ends at index 4096 (MAX_HANDLES). Figure: a handle table and the objects it names. Handles 2 and 3 name the same endpoint: 2 is its receive right, 3 a handle minted with badge 5 and stamped with S, a budget below system.

Every lookup checks the id in the handle against the id in the object’s frame, and the stamp’s id against its budget’s. A mismatch would mean a handle outlived its object. The chains of R10 (destruction) rule that out (I2 (revocation is complete)), and the kernel stops rather than use a frame that may hold something else (I1 (handles name live objects)).

Making, copying and closing handles

Each call that makes a handle installs it at the lowest free index of the caller’s table, stamped as R9 says. If the table cannot take it (TooLarge, or OutOfMemory for a new table page), the call is undone and costs nothing.

Handles are copied, never moved:

• a message carries up to MAX_MSG_HANDLES (4) handles, installed in the receiver’s table when it is delivered while the sender keeps its own (IPC);
• process_start copies up to MAX_START_HANDLES (128) of the caller’s handles into the new process’s table, at indices 1 to n in the order given (processes).

A copy is the same object, badge and stamp at a new index in another table. Copies are equal: none is the original, and closing one leaves the others. There is no call that copies a handle within one table.

handle_close(h) removes the handle at index h, and frees its table page if it was the page’s last; BadHandle if the caller holds no handle at h. It never destroys the object: a budget, endpoint or device lives on under its own rules, and a process handle closed early leaves the exit notice pending. The index is free again, and the process’s next new handle may take it. When a process ends, every handle in its table closes. When a process object is freed, every handle to it closes, in every table.

What objects cost

Everything the kernel stores is charged in whole pages to one budget (R6 (charging)):

Pages a process maps, lends or is given are charged as memory and IPC say. The header is the page at PROCESS_AREA (memory layout), one on both widths; a thread’s saved registers are the last bytes of its IPC page, so a thread costs one page on both widths too. The header and each IPC page are counted once, and neither is the process object’s page.

A budget’s own page is its parent’s, so the whole of a budget’s page limit is usable and a revocation scope (a budget with zero limits, made only to be destroyed) is no special case. The process object is charged to its creator, not to the budget the process runs in, because it holds the exit notice, and that notice must outlive the budget it ran in; the page was paid at process_create, so delivering a notice never allocates. Everything the running process needs (header, page tables, thread pages, handle table) is charged where it runs, and comes back when it ends.

So a process object belongs to two budgets, and each heads a chain of them, doubly linked through the objects’ own frames from a head word in the budget’s: the creator’s charged chain, of the objects charged to it, and a budget’s counted chain, of the objects whose PIDs it counts, which while a process lives is the budget it runs in. An object joins both when process_create makes it and leaves both when it is freed. A destruction finds the processes it kills, the objects it frees and the PIDs it moves from the dying budgets’ chains alone (R10).

Every charge comes back exactly, with one exception. Closing a handle, unmapping, replying, receiving an exit notice and destroying a budget each return what they freed; a refused call charges nothing. The exception is a DMA page quarantined because its device did not confirm a reset: it is never freed, so its charge stays, and moves to the parent when its budget is destroyed (devices). A table of n handles filled without closing any costs exactly ceil(n / 128) pages.

mint

mint(source, badge, budget?) -> h makes a new handle to an endpoint, with a badge the caller chooses. The source is one of:

• a receive right the caller holds: the new handle is to that endpoint, and its default stamp is the receive right’s stamp;
• the message id of an open call held by the calling thread: the new handle is to the endpoint the call arrived on, and its default stamp is the stamp of the handle the call came through. A send’s id, another thread’s call and an id the thread never received are InvalidArgument; if the call’s endpoint or its stamp has gone meanwhile, Dead.

The rules:

• The badge is never 0: 0 is the receive right, and mint never makes one. The decoder in redoubt-sys refuses it, and the kernel checks again (I3 (minted badges are non-zero and narrow)).
• Only a receive right mints: a source handle with any other badge is NotPermitted. So only a holder of the receive right hands out badges for an endpoint (I4 (only badge-0 handles receive)).
• With no budget handle, the new handle gets the default stamp. With one, that budget must be the default stamp or below it in the budget tree, or the call is NotPermitted: a budget handle only narrows. A 9P server mints a connection in the scope its client hands it (R41 (narrowing by revocation scope)).
• The new handle is installed like any other: the lowest free index, TooLarge or OutOfMemory if the table cannot take it.

The badge means whatever the server says: a 9P root and its mode, one client’s session, one grant in a typed protocol (the servers). The kernel only guarantees it: every message sent through the handle carries it (R14 (unforgeable sender)). Minting from a call is how a server answers a request with a new capability: the handle it returns is stamped like the handle the request came through, so it dies with the client’s grant. The full order of checks is in the ABI reference.

flowchart TD
    root[root] --> system[system]
    root --> users[users]
    system --> S["S: a revocation scope"]
    RR["receive right on E<br/>badge 0, stamp system"]
    RR -- "mint badge 5" --> H5["E, badge 5<br/>stamp system"]
    RR -- "mint badge 6 into S" --> H6["E, badge 6<br/>stamp S"]
    RR -- "mint badge 7 into root<br/>or into users" --> NP["NotPermitted:<br/>not system or below"]

Figure: narrowing. A receive right stamped with system mints handles stamped with system or a budget below it, never above or beside it. Destroying S revokes the badge-6 handle and every copy of it; the badge-5 handle lasts as long as system.

Because mint only narrows, a server can mint a handle into a user-class budget only from a receive right whose stamp is that budget or an ancestor of it. A server’s own endpoints are stamped with its own budget, so a system-class keeper — the steward, whose sessions and leases are carved from users — cannot mint a session’s or lease’s handles from them: users is beside system, not below it. The receive rights it mints from are therefore ones a process running at or above users created: init, which runs in root, makes its servers’ endpoints stamped root (below which everything sits) and mints the badged handles its manifest names (init); a helper run in users itself stamps its endpoints users and so can mint into anything under users. That helper must run in users itself, not in a child of it (a child’s stamp would be the leases’ sibling, not their ancestor), and it may exit at once, because an endpoint dies only with its owner budget, never with the process that created it.

Authority

What each handle lets its holder do:

A handle of another kind gets WrongObject. A device handle is the only way to hardware (R18 (device authority)).

• A process uses only its own table. An index is looked up in the caller’s table and nowhere else, so no number a process passes names another process’s handle, and a forged index is BadHandle (I1).
• No rights bits. Whoever holds a copy of a handle may do everything in its row. A grant is narrowed by the server minting a badge that means less, or by giving a child budget in place of a budget, never by a flag on the handle.
• Authority grows only three ways: a creating call makes a new object paid from the caller’s own budget; mint makes a new badge on an endpoint whose receive right the caller holds or whose call it took; a copy passes on a handle the sender already holds. None gives the caller authority over anything it did not already hold or pay for.
• A budget handle is the right to end that budget. Any holder may destroy it and everything below it, so a budget handle is given only to a party that may end it. A party that needs a budget only to narrow a mint is given a revocation scope, whose destruction ends no process (budgets).

Security properties

R9 (stamps)

Every handle has a stamp, a budget. Destroying that budget, or any budget above it, closes the handle and every copy of it, in every table; a copy in a message not yet received arrives as 0 (R10 (destruction), I2). Which budget the stamp is:

• endpoint_create, budget_create and process_create stamp the new handle with the caller’s budget, the one its process runs in. A budget handle made by a process in budget A dies with A, even though the budget it names sits under another parent and outlives it.
• A copy keeps its stamp. A handle delivered in a message or a reply, or placed by process_start, is stamped as the sender’s was. No path restamps a handle.
• mint stamps with the source’s default stamp, or with a budget the caller names at or below it (mint). The default stamp of a call is the stamp of the handle the call came through, not the caller’s budget.
• Handles the kernel places at boot, before any process runs, are stamped with root for the budgets and devices init receives (boot).

So a stamp only moves down the budget tree. A handle minted from another dies no later than its source, and a handle minted in answer to a call dies no later than the handle the call came through: a client whose grant is revoked loses what servers minted for it as well.

The stamp is not the object’s owner. An object dies with the budget it is charged to; a handle dies with its stamp; either ends the handle, because R10 closes every handle whose object or stamp is being destroyed.

Failure and restart

• A process ends: every handle in its table closes and its table pages return to its budget. The objects they named are untouched: an endpoint it received on stays for a restarted server (R4b (a server dies)).
• A budget is destroyed: every handle naming it or a budget below it, naming an endpoint, device or process object charged to one of them, or stamped with one of them, closes in every table, and a copy in a message not yet received arrives as 0 (R10).
• A process object is freed, when its notice is received or dropped or its creator’s budget is destroyed: every handle to it closes.
• A creating call cannot install its handle: the object is freed and its charge returned, so a refused create costs nothing.
• A handle whose object has gone is a kernel bug, not an error a call returns. Every lookup compares ids, and on a mismatch the kernel stops rather than use a frame that may hold something else (I1). R10’s sweeps keep it from happening (I2), and no argument to any call reaches it (I14 (no call panics the kernel)); budget-destroy-attack reuses frames and indices after a destruction to look for one.

Residual risks

• No call destroys an endpoint. An endpoint lives, and costs its owner a page, until the owner budget is destroyed; closing every handle to it frees nothing. The owner is always the creating process’s own budget, so a server that makes an endpoint per client pays for each until that budget goes, bounded by the budget’s page limit. Servers make one per service instead (Why).
• A device object is never remade. None is created after boot; one destroyed with its owner, or for failing a DMA reset, is gone until reboot (devices).
• Revocation is by budget only. A grant is revoked by destroying the budget it is stamped with, and with it everything else stamped there. A server that means to cut off one client alone must have minted that client’s handle into a revocation scope of its own. Otherwise it can only stop honouring the badge: the handle still reaches the endpoint, and the refusal is the server’s, not the kernel’s.
• A budget handle cannot be narrowed. Every holder may destroy the budget and everything below it: a handle to system is the right to end every system server, and a handle to root the right to end every process.
• A stale handle stops the machine. The kernel’s answer to a broken I1 is to stop. A bug in R10’s chain walk would stop the kernel, and every process with it; it would not let a process use a freed object.
• Slot searches and one sweep scan. Destroying a budget closes the handles in its chains and frees the dying tables whole; it walks the dying subtree, its owner lists and its process chains, not the object frames or the live tables (budgets). Destroying a quarantined device still closes its handles in one pass over every table of every process (up to MAX_PROCESS_COUNT (511) processes of 64 table pages), bounded by compile-time constants. Installing a handle searches for the lowest free slot of one table.

Why

• No rights bits. A read-only or non-transferable handle would not hold: its holder can proxy for anyone it talks to. So the kernel checks one thing, that the caller’s table holds the handle, and meaning lives where it is enforced: in the badge, which the server chose and checks (a 9P root, read-only), and in the stamp, which bounds how long the grant lasts.
• Budgets are the only revocation. There is no per-handle revoker and no derivation tree to walk. Every handle already names a budget in its stamp, and destroying a budget is already the one way resources come back, so revocation reuses it. A revocation scope, a budget with zero limits, makes any grant revocable on its own for one page. Budget ids are never reused, so a stale stamp never matches a later budget.
• Stamps only narrow. A server answering a call mints under the call’s stamp by default, so what it hands a client dies with the client’s grant, and the server never holds the client’s budget.
• An endpoint dies only with its owner. A server serves every client on one endpoint and tells them apart by badge (the servers), so it makes one endpoint per service, not per client, and no server needs to free one on its own. A call that did would add a destruction path to the kernel for a cost that already falls only on the owner’s own budget, bounded by its page limit.
• Stamp and owner are separate. Who pays for an object and who may revoke a handle to it are different questions. A process in budget A may create a budget under B for someone else; B’s child lives as long as B, while A’s own handle to it dies with A.
• Every object is a page of its own. There is no kernel table of fixed size that one budget could fill for everyone: creating an object fails only on the caller’s own budget (R7 (carving)). Handle tables work the same way, a page at a time.
• Lowest free index, never compacted. An index stays valid until it is closed, so a program can keep a number. A table with holes costs a page per page in use, which is what its memory costs, and the model charges the same.
• TooLarge at MAX_HANDLES, so a caller can tell a full table from a budget out of pages; the limit also bounds every scan of a table.
• 0 means none, so optional arguments and revoked message slots need no second encoding.
• The process object is its creator’s, because its exit notice must outlive the budget the process ran in; the page was paid at creation, so a notice never allocates.

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.

Memory

A process gets memory only from the kernel, in whole 4 KiB pages, paid for by its budget. Five calls change what a process has mapped: map_anon, map_fixed, unmap, set_flags and process_map. The kernel zeroes every page before a process first sees it, never maps a RAM page writable and executable, and chooses every address but the ones map_fixed and process_map name. Lends and transfers move pages between processes by changing page-table entries, never by copying.

Purpose

Memory is what every process consumes, and a page is the easiest thing to leak between two processes: a frame freed by one and handed to the next still holds what the first wrote. So the memory calls have four jobs. Hand out pages that hold nothing of anyone else’s. Keep every RAM page W^X, so data a process writes cannot run as code. Keep a page’s owner and payer straight as it moves by lend, transfer or process_map. And keep the cost of each call bounded by what the caller has, because the kernel runs a call to its end with interrupts off.

Interface

The mapping calls

A range is page-aligned and non-empty, and for every call but map_anon it lies below USER_AREA_END (the end of user space: 0x8000_0000, 2 GiB, on rv32; 0x40_0000_0000, 256 GiB, on rv64). Flags are READ, WRITE and EXECUTE: at least one, never WRITE with EXECUTE, never WRITE without READ. “The caller’s own page” is a live user mapping that is neither side of a loan and is credited to the caller in the kernel’s frame ownership table (or is a dma_alloc page of its own, or device registers it mapped). Only the RAM among them can be made executable (R11). A reservation not yet touched is not a mapping.

Each call checks the whole range before it changes any page, so an error leaves every mapping as it was and charges nothing. process_map counts the untouched pages of its source among what the call must pay for, and backs them only once nothing can refuse it. The errors are InvalidArgument and OutOfMemory, and for process_map also BadHandle, WrongObject and NotPermitted (the child has started). The order of the checks, the same in the kernel and the model, is in the ABI reference.

Backing and zeroing

map_anon and map_fixed back every page when they map it. Each takes a free frame, charges it to the caller’s budget (R6 (charging)), and only then writes the entry that maps it. Every free frame is already zero: a frame given up is zeroed before it is free again (below), and a frame free since boot, which may hold whatever the loader or the firmware left there, is zeroed through the physmap the first time it is taken. So a page is zero the first time its process can see it, whoever held the frame before, and backing a page writes nothing to it. The page tables a mapping needs are allocated and charged as it goes, to the budget of the process they map into. A free frame is a set bit in a bitmap the kernel keeps, with a summary bit for every word of it, level above level, to a fixed depth set by the most RAM the kernel can map. Taking the lowest free frame reads one word a level, and giving one back sets its bit and at most one word a level, so neither searches RAM, however much of it is in use (bench:scan-bounds). A checked build proves after each destruction that the bitmap is exactly the free frames and every summary is exact.

The one exception is the stack of a program the loader starts: it is reserved, its entries holding permissions but no frame. A page of it is backed with a zeroed, charged frame on first touch: a load or store fault, or a call that lends, transfers or process_maps it. A process started by process_start has no reservations: its parent gave it every page it has.

Running out is the caller’s error: map_anon of more than the budget or RAM can supply is OutOfMemory, and every page and page table it had taken goes back.

The zeroes cannot be discarded from user mode. Until they are evicted they may live only in a data cache, and a cbo.inval of the page would drop them and expose the frame’s old contents in DRAM. So the kernel writes senvcfg 0 on every hart at entry, whatever the reset left, and every cache-block operation traps in user mode; the boot stops unless it reads the 0 back. The firmware turns a supervisor cbo.inval into a flush, so no mode below M can discard a line. The kernel requires privileged architecture 1.12, where senvcfg first appears: on an older hart the write traps and the boot stops.

A test kernel’s trace ring (sched-trace, never in a release build; R23 (no test channels)) takes its frames at boot, the highest free ones, before the budget tree counts what the kernel keeps, and holds each as its page number in 32 bits, so the 256 MiB ring’s table of 65,536 frames fits the kernel’s 1 MiB RAM region. Every frame the kernel takes lies in the physmap, which ends at 128 GiB on rv64 and below 4 GiB on rv32: page numbers to 2^25, where 32 bits reach 16 TiB of physical address. A compile-time assertion in kernel/src/sched.rs holds the physmap’s last page number within 32 bits.

Frames in flight

A frame its owner gives up, by unmap, a process’s end, a page table emptied, an abandoned lend or a kernel object freed, is not free at once. Under the kernel lock it goes in flight: the ownership table names it as IN_FLIGHT’s, a reserved owner no process has, so every call that checks who owns a frame refuses it, and its bit in the bitmap stays clear, so no allocation takes it. Its budget is uncharged then, as before. It is zeroed later, outside the lock by the hart that freed it when that hart idles, or under the lock by an allocation that finds the bitmap empty, and the lock’s next holder, on any hart, gives it back to the bitmap (R81). So zeroing, the one piece of a frame’s work long enough to matter, leaves the calls that free and the calls that allocate whenever a hart has idle time to do it, and a call never pays for frames it did not free or take.

A frame waits for its zeroing on one of two lists the freeing hart keeps:

1. Staged, while another hart may still hold a translation to it: the call cleared its entry in a process’s space and has yet to shoot that process down. The list holds the frame’s number, never anything in the frame, since a store through a stale translation could still change it. The call’s shootdown (residual risks) moves the process’s staged frames on; a call that frees more than the 64 a hart stages shoots the process down early, once for every 64.
2. Pending, once no hart can store to it: an ended process’s frames (its harts left its space before its frames were freed), a kernel object’s (never mapped), and the staged ones after their shootdown. The list is linked through one word of each frame, the word a destruction already links the object frames it frees through, so that chain joins the list whole.

Pending frames are zeroed in one of two places, and never in a third:

• Idle, when every hart is idle. A hart with nothing to run, when every started hart is idle too, takes one frame off its pending list while it still holds the lock, gives the lock up, zeroes it and pushes it onto its done list, the link still in that word. With more left it does not halt, but goes back through kmain’s interrupt-enabled top, where an interrupt that came meanwhile is taken and anything woken runs first, and then takes the next. So an idle hart answers an interrupt within one frame’s zeroing, about 30 µs under icount. One hart drains at a time: each frame costs its drainer a release and a take of the lock, and two drainers would find it held at nearly every take, each take a halt and each release the other’s interrupt. At rest after a login on launch’s four harts that was about 33,000 interrupts in two seconds, where alone a drainer finds the lock free. A hart that idles while another drains halts; the drainer, its list empty, wakes the next hart with frames pending once it gives the lock up, and so does a hart that idles last with none of its own, for a hart that halted with frames while another worked. A drainer woken to work drains no more until every hart is idle again, and gives the drain up at its next idle pass if one is not. While any hart is busy, an idle hart halts instead, as before, and a hart with nothing pending halts as it always did. So the system at rest, once drained, takes the interrupts it took before R81 (the machine at rest).
• On demand. An allocation that finds the bitmap empty with frames in flight gives back the done frames first, then takes one frame off any hart’s pending list and zeroes it under the lock, as every allocation once did: one frame for each allocation, main’s cost. Only when every frame in flight is one an idle hart is zeroing does it wait, still holding the lock, and then for one frame at most: that hart needs no lock to finish it, and its push wakes the waiter. So a budget can always pay for the frames it can buy, and they always exist, because the frames in flight are RAM no budget is charged for.
• Never at an exit to user mode. The thread a hart returns to did not free those frames, and the caller of a destruction waits for the walk of R10 (destruction), not for the zeroing of the lease it freed: a lease’s 4,300 frames, zeroed there, put 140 ms into the steward’s deadline notice in the containment gate.

Why only when every hart is idle: under icount the harts share one virtual clock, so a hart that zeroes while another works slows that one’s time as surely as if the work were its own; a refused search in map-anon-search-bound took 406 µs instead of 116 at two harts while the other hart zeroed. On a real machine that zeroing would run beside the work for free; that is forgone for now (residual risks).

A pending list is read and written only under the lock, and the frame an idle hart zeroes only by that hart, so a frame in flight is in exactly one place: staged, pending, being zeroed, done or being given back. The kernel’s checked build counts them, list by list, against the ownership table at each destruction’s audit, so a list lost or linked twice stops the boot. Every acquisition of the lock gives back up to 64 done frames from every hart’s list, clearing each link, so a frame enters the bitmap all zero and the step adds a bounded piece to each kernel section. Pending frames are bounded only by RAM.

Every build, the release one too, keeps a count of the frames in flight and says on the console when a large drain begins and ends: mem: 1024 frames in flight when the count first reaches 1,024 since it was last 0, and mem: frames in flight 0, at most N when the frame that brings it back to 0 is given back, N the most it held meanwhile. Both are ordinary kernel lines, under the console’s hold like the rest (the console’s one writer), and the common give-back pays one comparison with 0. The bench waits on them before it measures a system at rest, so that window never holds the zeroing of the boot’s and the login’s frames (the machine at rest). Why 1,024 frames (4 MiB): on launch’s machine the boot and the first login leave about 35,000 in flight, the first line coming during the boot and the second only once every hart first idles after the login, and the shell’s step after the bench’s window frees about 4,600, while a system at rest frees a page or two every few seconds, which never reaches it, so at rest the console stays quiet; and a drain under 1,024 frames takes under 10 ms to zero, too short to matter to the window. A pair of lines needs 1,024 frames retired and then a drain back to 0, so the console gets at most two lines for every 4 MiB freed and drained. What they tell a reader of the console is that some process freed 4 MiB or more and when the zeroing ended: a timing channel, out of scope (TENETS). The last frames come back at the lock’s next acquisition, at rest the next timer interrupt, so the second line can follow the drainer’s last frame by up to about a second.

The zeroing an idle hart does is the work of whoever freed the frames, so it is billed to them: the budget paying for the kernel time when the frame was retired (the caller, a destroyer, or a deadline’s payer (R10 (destruction))), when the hart takes the lock back, for the frames it zeroed, the newest first as the list gives them; the hart keeps at most four such payers, and what it has not zeroed stays theirs until it does. A frame zeroed on demand is the allocation’s own kernel time, as on every allocation before: it comes off the freeing hart’s payers unbilled, the newest first by count, since a frame does not record its payer, so the split among those payers is by counts, not by frame.

Page tables

Status: built · tested: bench:page-table-reclaim, mutation:R6EmptyTableKept

A page table is made when a mapping first needs it, charged to the budget of the process it maps into, and freed, with its charge, by the call that leaves it mapping nothing: every entry empty, with no page, no reservation and neither side of a loan. So unmap frees the tables its range empties, and so do a failed map_anon’s rollback, process_map in its source, and a transfer in its sender. A lend’s tables in the server go at the reply that returns it; an abandoned lend’s go from the caller when the call is abandoned, and from the server at the reply that frees the lend. A call frees tables once it has finished, never between making a table and filling it. It reads at most ENTRIES entries for each table the range reaches, so the cost follows the pages it unmapped (R22). The root table goes only with its process.

Where map_anon puts pages

The kernel chooses the address, and nothing may depend on it. map_anon takes the first free run of pages in its placement area, 256 MiB from DEFAULT_BASE (0x6000_0000 to 0x7000_0000), searching from the start of the run it placed last to the last start that fits, then from the area’s start. Every start up to the last one that fits is tried, so a run that fits only at the area’s end is found, and so is the whole of an empty area; every run placed lies inside the area. A page is free only if its entry is empty: a reservation or either side of a loan is taken. A request that finds no run, or is larger than the area, is OutOfMemory. The search looks at each page of the area at most once (R22). map_device and dma_alloc place their mappings the same way (devices). A receiver’s lends and transfers land in a second area, 4 MiB from DEFAULT_MESSAGE_BASE (0x4000_0000), found the same way. The rest of the user layout is on memory layout.

The model places runs in the same two areas, searched the same way, so the two agree on addresses as well as outcomes.

map_fixed

map_fixed(addr, len, flags) maps zeroed pages at exactly addr in the caller’s own address space, charged as map_anon’s are. It is the one call that puts new pages at an address the caller names, so that the loader stub can place a program’s segments at their link addresses from inside the process it is loading.

Unlike POSIX MAP_FIXED it never replaces a mapping. A range that touches any occupied entry of the caller’s (a mapping, a reservation, either side of a loan) is InvalidArgument, and nothing is mapped. The checks run in this order, all before anything is allocated:

1. the range: aligned, non-empty, no overflow, below USER_AREA_END (page 0 is user space);
2. the flags;
3. the pages alone against the budget, by arithmetic;
4. the overlap, over the whole range;
5. the pages and every page table the range still lacks, counted across table boundaries.

Only then does the mapping loop run, and it cannot fail. So a map_fixed maps everything it was asked or nothing, and a refused one charges nothing.

Instruction fetch after mapping

Status: built · partly tested: no case can see a missing fence.i, because QEMU keeps instruction fetch coherent with stores; smp-fence shows from the trace that the other hart fenced · tested: bench:smp-fence

A hart may fetch stale instructions from a page just written unless it fences. After any call that installs an executable mapping (map_anon, map_fixed, set_flags or process_map with EXECUTE), the kernel runs fence.i, so the hart’s later fetches see every store it made before. It runs one more at boot, before the first process, for the images the loader wrote.

W^X makes one fence per call enough: a page is written while it is writable and not executable, and becomes executable only through one of these calls. On several harts the call also shoots the process down on every other hart running it, and that hart runs fence.i before it acknowledges; a hart also runs fence.i before it runs a process. A thread that moves between harts needs no fence of its own: a RAM frame has at most one user entry, so a process’s code changes only through these calls.

Lending at the page-table level

A lend or a transfer is page-table edits:

• When the message is sent, each page is checked first: backed (a reserved page is backed at this point), the sender’s own RAM, and for a lend writable. Then each is taken out of the sender: its entry keeps the frame, loses VALID and gains the lent bit S (a software bit of the entry; memory layout). That entry is the loan’s only record.
• When a receiver takes it, the frames are mapped read-write in the receiver’s message area. A lend’s entries there carry S too, marking them as the borrower’s side.
• At the reply the kernel checks that the borrower’s entry and the lender’s entry name the same frame, clears the borrower’s, and makes the lender’s valid again. A message refused or timed out while still queued was never mapped in a receiver: the lender’s entries are simply made valid again.
• A transfer’s sender entry is cleared when the receiver takes it, and the frame’s owner and payer change together (R4 (delivery)). A lend whose call is abandoned goes the same way to the server (R3 (lends and abandoned calls)).

Only these steps of the kernel’s own (the return, a transfer’s delivery, an abandonment) touch an entry with S. unmap, set_flags, map_fixed and map_anon’s search treat both sides of a loan as occupied, so the lender cannot unmap, remap or re-flag a lent page, and the borrower cannot unmap or re-flag its side. A borrowed page stays credited to its lender, so the borrower cannot lend it on, transfer it or process_map it. The kernel never reads or writes a call’s record in a borrowed page. When caller and server are the same process, both sides of the loan sit in one address space, and the return still checks both markers and the frame before changing either.

A page’s life

A RAM frame is taken from the free-frame bitmap and given back to it, so backing a page, a page table or an object searches nothing, however much of RAM is in use; a dma_alloc run comes from the DMA pool instead, a fixed 1024 pages (devices).

stateDiagram-v2
    state "DMA-held" as DMA
    state "In flight" as Flight
    [*] --> Free: free at boot<br/>(zeroed when first taken)
    Free --> Mapped: map_anon, map_fixed,<br/>first touch of a reservation
    Mapped --> Flight: unmap, a reply to an<br/>abandoned call, or the process ends
    Flight --> Free: zeroed (its hart idle, or an<br/>allocation), then given back
    Mapped --> Mapped: process_map<br/>(moves to the child)
    Mapped --> Lent: call with a lend<br/>(unmapped from the caller)
    Lent --> Mapped: reply, or the call fails<br/>(back to the caller)
    Lent --> Mapped: call abandoned<br/>(the server's own)
    Mapped --> Transferred: send with a transfer<br/>(unmapped from the sender)
    Transferred --> Mapped: taken (the receiver's), or<br/>the send fails (the sender's)
    state "DMA pool" as Pool
    [*] --> Pool: taken at boot
    Pool --> DMA: dma_alloc (zeroed first)
    DMA --> Pool: its process ended and every<br/>device that could hold it was reset

Figure: the states of a RAM frame. A frame is mapped by at most one process at a time, and is zero whenever it leaves Free or the DMA pool: zeroed in flight, on its way back, or at its first allocation if it has been free since boot. A frame in flight is no one’s and not free (R81). A pool frame is never Free, and a Free frame is never DMA-held.

Authority

• A process maps only into its own address space. map_anon, map_fixed, unmap and set_flags act on the caller’s own pages; none names another process.
• process_map needs a process handle to a child that has not started. A started process is closed to its parent: nothing can be slipped into a process that is already running.
• Pages come from the budget. Every frame and page table is charged to a budget, so a process can map no more than its budget allows (budgets).
• No call names a physical frame. There is no call that maps RAM by physical address, so holding memory never gives a way to reach anyone else’s.
• The memory calls create no authority: they change pages the caller already has, or move them to a child it already holds.

Security properties

R11 (memory)

• No RAM page is ever mapped writable and executable (W^X): not by one entry, and not by two, since a RAM frame has at most one user entry at a time (the kernel’s physmap aside). W+X is refused when any call is decoded (WRITE with EXECUTE, or an unknown bit, is InvalidArgument), again by map_fixed and process_map before they charge, and again by the page-table layer, which refuses to build such an entry, so no check rests on another. set_flags may add EXECUTE only to a page it makes not writable in the same call.
• W^X holds per frame, not only per mapping. Only RAM that a process owns is ever executable. Device registers and DMA frames are never mapped executable: the device, or another mapping of the same registers (in this process or a co-holder’s, since a mapping outlives its handle), can write them underneath. map_device and dma_alloc map read-write and never executable, set_flags refuses EXECUTE on either, and process_map refuses device and DMA pages.
• Writable implies readable. The privileged architecture reserves the write-only entry, so map_anon, map_fixed, set_flags and process_map refuse WRITE without READ.
• Flags are checked before anything is charged or moved for the new mapping, so a step that cannot fail never meets bad flags. process_map checks them before it backs any page of its source.
• Every page is zero before a process first sees it: anonymous and fixed pages, backed reservations, page tables, and dma_alloc pages. Every free frame is zero, by R81, and a frame free since boot is zeroed when first taken, so backing a page writes nothing to it; dma_alloc pages are zeroed as they leave the pool. Pages moved by lend, transfer or process_map carry their contents, because moving them is the point.
• The zeroes stay. senvcfg is 0 on every hart and the firmware turns supervisor cbo.inval into a flush, so no process can discard the zeroes the kernel wrote to its page and read what the frame held before (above).
• No physical addresses. No call takes one, and none maps RAM by one: map_device maps a device object’s registers, and the boot refuses any device object that overlaps RAM. The one physical address a process learns is that of its own dma_alloc pages, which its device needs (devices).
• DMA pages are held until reset. A dma_alloc page stays with the process that allocated it until that process ends: unmap drops only its mapping, and it is never lent, transferred or process_mapped. It returns to the pool only after every DMA device that could hold its address has confirmed a reset, and a quarantined device never counts as reset (devices, I16 (DMA pages reset before reuse)).
• A lent page is unmapped from its lender until the call ends (above).
• map_fixed never replaces a mapping, so it can neither discard a page nor alias one.

Together these are I9 (pages W^X, zeroed, lends unmapped) of the invariants.

R81 (frames in flight)

A freed RAM frame is in flight until it is zero: it belongs to no process and is not free.

• No one can name it. Its owner in the ownership table is IN_FLIGHT, which no process is, so every call that frees, lends, transfers or process_maps a frame refuses it, as it refuses a frame of another process’s; and no call names a physical frame (authority).
• No allocation takes it. Its bit in the free-frame bitmap is clear until it is given back, and every frame a mapping, a page table or an object gets comes from the bitmap.
• One hart writes it at a time, and only once no other can. Its number is staged until the shootdown of the process whose entry for it was cleared has been acknowledged by every hart asked; only then is it linked through a word of its own, and later zeroed, by the hart that freed it while that hart idles, or under the lock by an allocation that took it off that hart’s list. Pending lists change only under the lock, and an idle hart zeroes only the frame it took off its own, so no two harts hold one frame. A frame of an ended process, whose harts left its space first, or of a kernel object, never mapped, is linked at once.
• It is given back only zero, and only under the lock, by the lock’s next holder, which clears the link it held.

So every free frame is zero and allocation writes nothing. The kernel’s checked build samples every frame it takes from the bitmap and counts the frames in flight against the ownership table in its destruction audit (I1 (handles name live objects)); smp-inflight-race’s kernel checks each frame it gives back word by word, and its trace shows the order above for every frame (the frames in flight). In the model, a free puts the frame in flight with what it held, and time passing zeroes and frees it; a frame is held, in flight or free, never two, and a free frame is zero (the model).

R19 (kernel W^X)

Status: built · partly tested: no case plants a writable kernel code page to show that the check stops the boot · tested: bench:kernel-wx

The kernel’s own mappings are W^X. At boot, before any process runs, the kernel walks its own area of the address space and, for every executable page there, checks three things: the page is not writable, its frame’s alias in the physmap is not writable, and that alias is not executable. The check reads only the aliases of executable kernel frames; it does not walk the rest of the physmap, whose entries the loader builds never executable. If one fails, the kernel panics instead of running. It then prints W^X verified: N executable kernel pages, none writable under any alias, the line the case checks. Every mapping the kernel makes later goes through the same entry constructor that refuses W+X; its one later window, for DMA device registers, is read-write and never executable.

R22 (range cost)

Status: built · tested: bench:map-fixed-attack, bench:map-anon-search-bound, host:redoubt-model::huge_len_is_refused_promptly

A call that takes a range costs what the page tables hold and what the budget can pay for, never what the length asks. A process could otherwise ask for a huge range for free, and the kernel, running the call to its end with interrupts off, would stall every other process.

• unmap, set_flags and process_map check the range page by page and stop at the first page that is not the caller’s, so their cost follows what is mapped there.
• map_fixed first refuses a range the budget cannot pay for by arithmetic alone, before any walk. It then checks overlap by walking the page-table tree and skipping every absent subtree whole: at most the root entries the range spans, plus ENTRIES (512 on Sv39, 1024 on Sv32) for each table present in it, and only then counts page tables. A map_fixed of the whole of user space, which no budget in the case can pay for, is refused well inside the case’s 10 ms bound, over mappings or not.
• A lend or transfer checks at most the pages mapped in its range, and a lend is at most MAX_LEND_PAGES (16).
• map_anon’s search, which also places map_device, dma_alloc and a received message, never tests a start twice: when a page is taken, the next start tried is the page after it, and a missing page table skips its whole span. So it looks at each page of its fixed area at most once, 65536 for map_anon’s and 1024 for the message area, whatever the request asks. With every page table of the area present, the worst case, a refusal takes about 9.6 ms in a checked build under virtual time; the case bounds it at 12 ms, and a timer wake during it at 15 ms.

Failure and restart

• Out of memory is the caller’s error. A mapping call that cannot be paid for returns OutOfMemory; a process that exhausts RAM gets OutOfMemory and every other process keeps running. A refused map_fixed charges nothing, a refused process_map charges neither the child nor the caller, and a refused map_anon gives back every page and page table it took.
• A permission fault ends the process. A store to a page that is not writable, or a fetch from one that is not executable, is never mistaken for a page to back. The process faults, and its exit notice carries the RISC-V cause (12 for an instruction page fault, 15 for a store page fault; processes). The console gets one line, PROGRAM HALT: CPU Exception on PID n: <cause> of <address> at <pc>, printed holding the kernel lock; the thread’s registers and the address space’s map, a line a mapped page, are printed only for a fault in the kernel and in a debug-print build. Printed for every fault, they held the lock for as long as the process was large: 837 ms on rv64 for a process of 4096 pages, against 7.5 ms for its teardown now (bench:fault-report-bound, under icount).
• A process ends: every frame it owns returns to the pool and its charge to its budget. A page it had lent is its server’s until the server replies (R3), and is never reused while the server has it mapped. Its dma_alloc pages wait for the device reset (R11).
• No argument to any memory call makes the kernel panic (I14 (no call panics the kernel)). Lending untouched or half-mapped ranges, unmapping a lent page, and exhausting RAM are each attacked by a case that passes only on a clean power-off.

Residual risks

• map_fixed can fill map_anon’s area. A process that maps the whole area with map_fixed makes its own later map_anon calls fail with OutOfMemory. It harms only that process. The same for the runtime’s thread-stack area (memory layout): a map_fixed of the program’s own there takes a slot, or a guard page, from its own later spawn, which is then refused.
• Several harts. fence.i and the TLB flush act on the hart that runs the call. A process’s translations carry its ASID, and a hart that ran it may keep them; it flushes that ASID before it next runs the process if any of its mappings were removed meanwhile or its PID was given out again. Every call that clears or narrows one of a process’s entries, frees one of its tables or makes one executable first shoots the process down on each other hart running it now, which flushes its ASID, runs fence.i and acknowledges before the call returns; a destruction’s shootdown also makes the hart leave the process’s space before any of its frames is freed. The asking hart waits for the acknowledgements halted, and each hart sends it an interrupt as it acknowledges, as a hart waits for the kernel lock (R78 (fair kernel entry)): spinning, under QEMU’s icount it spent the turns the other hart needed to acknowledge, and the p99 of a destruction’s kernel time (R10 (destruction)) in sched-latency at two harts was 51.9 ms on rv64 against 3.0 ms halted. The asking hart holds the kernel lock while it waits: measured under icount the waits total 0.9 ms over the whole containment gate at two harts, so they stay under it, where the asker is the lock’s one holder. So no stale translation reaches a page unmapped, lent or returned, or a frame’s next owner. A missed shootdown cannot be seen on QEMU, which empties a hart’s TLB at every satp write: the checked build stops when a process loses an entry while another hart runs it and is not shot down there (bench:smp-shootdown, the case’s recorded negative), and smp-fence checks from the trace that the fence was taken.
• The physmap maps every user frame writable for the kernel, code included. Only the kernel can use that alias (memory layout).
• A freed frame may still be mapped on another hart. A free writes nothing into the frame until the shootdown that clears its last translation is acknowledged: the frame waits staged by number, and is linked through a word of its own, then zeroed, only after (R81). So a stale mapping could reach only a frame no one has written since, never the kernel’s link nor its next owner’s data. Every path that frees a mapped frame unmaps it and flushes the TLB first, or frees an ended process’s frames or a refused process_create’s, whose cached translations carry that process’s ASID, which nothing runs under again until the PID is given out, and that flushes it first (satp); on one hart that leaves no stale mapping. On several, the call shoots the process down on any other hart running it before the frame can be given out again, and a destruction before the free (above, bench:smp-evict, bench:smp-shootdown).
• Freed frames are not zeroed beside the work. An idle hart zeroes frames in flight only when every hart is idle (frames in flight), because the bench runs harts under icount, whose one virtual clock bills a working hart for another’s zeroing. On a real machine an idle hart could zero while others work, at no cost to them; while any hart is busy, frames are zeroed on demand instead, one per allocation under the lock, as before R81. To revisit when the bench can judge an idle hart’s work without that shared clock, as sched-lock-contention-4-mttcg judges the four-hart tail without icount. So R81 saves nothing on a busy machine: in the containment gate, at two harts, no hart is idle while another works and 576 MiB never runs short, so allocations zero never-used frames at their first allocation, as before, and frames in flight reach about 79,500 (about 310 MiB), nearly all held to the end of the run, the longest given back 113 s after it was freed. A process that keeps one hart busy keeps every allocation at that cost, never worse than before R81. Meanwhile a freed frame’s old contents stay in RAM, though no call names the frame and no process maps it.

Why

• Back at map time, not on first touch. A process told it has memory, which then faults for want of it, has been told a lie. map_anon charges and backs every page before it returns, so a process’s memory is its own the moment it has the address. Only the loader-started stacks are reserved, because their programs have no parent to map them.
• Zero on reclaim, when the harts are idle. A freed frame is zeroed outside the kernel lock by the hart that freed it when every hart idles, or under the lock by an allocation that needs it, and the bitmap holds only zero frames, so no path that hands a frame to a process can forget to zero it. An allocation writes nothing when idle time has zeroed ahead of it; under load, with no idle time, it zeroes its own frame under the lock as before R81 (a frame never used since boot, or one in flight), so it is never worse than before. No hart zeroes on its way back to user mode: that taxes whatever runs next for frames someone else freed, and a lease’s 4,300 frames, zeroed there, put 140 ms into the steward’s deadline notice in the containment gate. Measured at two harts under icount before R81, zeroing was the one piece of a frame’s work long enough to matter: 220 µs a page while it checked every word, about a fifth of that after, and 15 s of the containment gate went to zeroing in 68,218 endpoint creations. The other way, zeroing at allocation outside the lock, splits every mapping call in two around a second wait for the lock, and the second must find its process alive and its range still free; zeroing on reclaim needs neither, since a freed frame is already no one’s. Frames free since boot are zeroed at their first allocation, under the lock, rather than all at boot, which would cost seconds of boot under icount for the RAM the cases give.
• The kernel chooses addresses, so no program depends on a layout and no call lands on another mapping. map_fixed exists because a program’s segments must sit at their link addresses and the loader stub, running inside the new process, is the only code that parses its ELF. The other ways were worse: mapping the segments from the parent would make the launcher parse ELF images, and relocatable programs would differ from every other binary’s fixed-address link. map_fixed never replaces, so it cannot discard or alias a page.
• The lender’s entry is the loan’s record. There is no side table to fall out of step. The S bit makes the entry one that only the kernel’s own lend steps may overwrite, and the return checks both sides against each other first.
• Flags checked more than once, and before charging. Decoding and the page-table layer each refuse W+X, and map_fixed and process_map check again, so a slip in one leaves the others. Checking before anything is charged means the steps after it cannot fail, so a bad combination is a clean InvalidArgument, never a half-done call or a kernel panic.
• Cost follows occupancy. The kernel does not preempt itself, so every loop in a call must be bounded by something the caller paid for: pages it has mapped, or pages its budget can buy.
• One fence per executable mapping. A frame reused from another process may still sit in a hart’s instruction cache. That is a correctness hazard, not a privilege one, since the code runs in the new owner’s context, and the fence each executable mapping gets on this hart clears it.

Budgets

A budget is the kernel object that holds resources. It has a page limit, a process limit and a CPU weight, a class, a label set, an account and an optional deadline. Every process runs in one budget, and every kernel object is charged to one. Budgets form a tree: a child’s limits are carved out of its parent’s, so the children never add up to more than the parent. Destroying a budget destroys everything below it, kills the processes in it and closes every handle stamped with it, wherever the copies went. A budget whose deadline passes is destroyed the same way.

Purpose

One object does five jobs that Unix spreads over cgroups, revocation lists, security labels, accounts and the scheduler:

• accounting: every kernel object costs pages from a budget, and running out is an error for the caller, never for anyone else;
• CPU: its free weight is its share of the one stride queue (scheduling);
• revocation: destroying it revokes every handle stamped with it or a descendant (objects);
• information flow: its label set decides whom it may talk to (R1 (flow), IPC);
• identity for servers: its account travels with every message it sends.

The steward builds a budget per principal, per label set, per session and per lease, and ends any of them by destroying it. A lease is a budget with a deadline, so the kernel ends it on time even if the steward is busy or gone.

Interface

The budget object

The free weight is the weight limit less the carved weight. It is the budget’s stride weight (R12 (scheduling), scheduling), so a budget with free weight 0 holds no process: process_create into one gets InvalidArgument. A budget also carries its place in the stride queue, which scheduling describes.

A budget with zero limits is a revocation scope: nothing runs in it, and it exists to be a stamp and later destroyed, so one grant can be revoked without killing any process (objects). It costs its parent one page, like any budget.

Each budget occupies one page of its own, allocated when it is created: the page its parent pays for. So there is no kernel table of budgets for one budget to exhaust at another’s expense. The page starts with a fixed magic word; a frame read as a budget that does not hold one means a stale reference survived destruction, and the kernel stops rather than trust it (I1 (handles name live objects)). A handle names a budget by its page and its id, so a handle to a destroyed budget never reaches a later one in the same page.

A budget lives until it or an ancestor is destroyed or its deadline passes. Closing the last handle to it does not destroy it: its carve stays out of its parent (see Residual risks).

The calls

The spec has no class and no scheduling flag: a child’s class is its parent’s, and what runs first is a matter of weight alone. budget_create’s own checks run in this order: the parent handle (BadHandle, WrongObject); depth (TooLarge if the child would be at MAX_DEPTH); the labels (LabelDenied, then ClassDenied); pages, counting the child’s own page (OutOfMemory); processes (OutOfProcesses); weight (InvalidArgument: no error names weight). The new handle is stamped with the caller’s budget (R9 (stamps)). If the caller’s handle table cannot take it (TooLarge at MAX_HANDLES, or OutOfMemory for a new table page), the child is undone and the parent is as it was. budget_destroy and budget_reap fail only on their handle (BadHandle, WrongObject). Record checks come first for every call; the full rows are in the ABI reference.

The kernel itself (PID 1) has no budget and makes no calls. A call from it would get InvalidArgument from a call that passes a record (the record check comes first, and no user page is the kernel’s), NotPermitted from most others, BadHandle from handle_close, budget_destroy and budget_reap, and an answer from time_now and random; none of them panics, so a bug there cannot become one.

Root, system and users

At boot the kernel creates three budgets, all with account 0, no labels and no deadline:

root pays for the two budgets’ own pages and carves the rest of its pages and processes into them, but what it keeps for init: one process, INIT_WEIGHT (1,000) of its weight, because a budget that holds a process needs free weight, and init’s pages (below): everything the loader gave init, its first thread and INIT_PAGES (1,024). By R6 (charging) root’s own page is charged to root, so its limit is the free frames less that page. The boot checks that root’s limit, its own page and the kernel’s frames fit in RAM, and stops if they do not.

init, the one program the loader starts, runs in root, charged there for everything the loader gave it (image, stack, page tables, header page, the bundle’s frames) and for its first thread. It gets handles to root, system and users in slots 1 to 3, stamped with root, then a handle to every device object (boot). The machine’s device objects are charged to system. A boot whose init and INIT_PAGES do not fit does not boot: the kernel stops (fail closed).

flowchart TD
    R["root<br/>class system, 510 processes<br/>weight 1,000,000, keeps 1,000 free"]
    S["system<br/>class system<br/>a quarter of the pages, 15 processes<br/>weight 250,000"]
    U["users<br/>class user<br/>the rest, 47 processes<br/>weight 749,000"]
    I[init]
    SV["servers and drivers<br/>(manifest weights)"]
    P["principals, label sets,<br/>sessions and leases"]
    R --> S
    R --> U
    I -- runs in --> R
    SV -- carved from --> S
    P -. carved from .-> U

Figure: the budget tree at boot. Solid: built. Dashed: planned, once the steward carves the principals’ budgets.

The tree from the boot manifest

The loader starts only init, which runs in root on the weight and the one process root keeps free. What init launches counts in the budgets it launches into.

A server’s heap cap (heap_pages, init) is its runtime’s own ceiling inside its budget: past it the runtime refuses an allocation before the kernel is asked, and the cap reserves nothing until it is used. The budget stays the hard bound on everything else the server holds: its image, its stacks, its buffers and lends, its page tables and its kernel objects.

• The kernel keeps its fixed split, the table above. The boot manifest does not size system: the kernel reads no manifest and the loader parses no JSON, so the split is set in one place, the kernel. init adds up what the manifest’s servers ask for and refuses the boot if it does not fit in system, before it starts anything (init).

• INIT_PAGES is init’s working set, with room to spare. Everything init uses is charged to root:

  • its first thread’s stack: 32 pages reserved by the loader, with one page initially backed;
  • its heap, one fixed arena mapped once, for the manifest and the startup blocks it builds;
  • a handle table of up to 64 pages;
  • a page for each server endpoint it owns;
  • a thread for each server, watching its exit endpoint: the thread’s stack and IPC page;
  • a process object for each process it starts (at most system’s process limit);
  • one batch of the program it is starting, at most 64 pages of its image and 64 of its stack at a time, copied through its pages and moved to the child (the loader stub).

  Each child’s first-thread stack is charged to that server’s own budget, at the manifest’s stack_pages size (the boot manifest).

  With the steward, sshd and the userland disk’s blkd, verity and erofsd, the image manifest’s bound is 564 pages on both widths (init-boot prints it; 14 of them the 16-page lend init pushes the public entries through), and the fixed 1,024-page limit is nearly twice it. The image’s servers need 17,448 of system‘s pages, each budget and its own page (the steward’s 1,051 among them: 1,024, the three pages of its cleanup thread and the twenty-four of its launch thread and the loop’s wider stack, the steward). The shell’s VMs are not among them: the steward carves each session from its principal’s sub-budget under users, from the top budgets the manifest names, 47,624 pages for Alice, 32,768 for Bob and 24,576 for agent (the steward, the image). A session is 11,392 pages, its VM’s share and its console relay’s. The VM’s is 11,264 pages: a heap cap of twice the largest peak of beamlet’s runtime heap across the memory cases plus what the VM holds outside its heap, 44 pages (its two schedulers’ stacks and thread pages, its locks’ endpoints and its process’s page), rounded up to 128 (beamlet), from a largest peak of 5,556 pages on rv64 (at one hart, with the shell’s machine mode beside the agent principal; 5,542 with the machine mode alone, 5,523 before it) and 5,362 on rv32, which the cap, 11,220 pages, holds twice with 108 to spare. It was 11,136 from a peak of 5,492, 11,008 with one scheduler, 19 pages outside the heap, and 11,904 while the shell loaded every command’s module at its start, when the peak was 5,904. The scan’s cap rule bounds it from below: an rv64 peak above 5,610 pages puts the cap under twice the peak, and the share then moves up a step of 128. The relay’s is 128 pages: its image (about 21 pages on rv64), its four stacks (5, 4, 4 and 4 pages), a heap cap of twice its 22-page peak (consrelay-footprint), and what the kernel charges for a process, rounded up to 128 (consrelay). The steward gives the VM the session’s pages less the relay’s, as its startup block’s budget_pages and its heap cap, so the relay’s room is never the VM’s. The console session has no relay and its VM the same share. Each sub-budget still holds two sessions, 22,786 pages with their budgets’ own pages: Alice’s top budget splits into two of about 23,800 pages, one for her unlabelled sessions (the console’s and one SSH context) and one for her vault’s, and Bob’s one sub-budget of about 32,760 holds two, as before, but not three. A session holds ten processes: its VM, its relay, its pipe server piped and up to seven stages (native programs). piped and the stages draw for now on the VM’s share, inside the headroom twice its peak leaves; they are to get their own measured share the way the relay has. The bench and mkimage’s instructions give the image 1 GiB (the image). The bound is a fixed count, not a share of RAM, because init’s needs do not grow with the machine, nor with the size of a program it starts, and a share of a large machine would sit idle in root. The manifest cannot change it, because the kernel reads no manifest. init works in a fixed arena, and before it creates anything it bounds what the manifest will cost it in root: the endpoints it makes, a process object, a startup block and a thread watching its exit endpoint (the thread’s IPC page and stack) for each server, the handles it keeps and mints, and the arena. It reads root’s free pages with budget_usage and refuses the boot if the bound is larger; a charge that fails later is a bug in the bound, and refuses the boot too, so no boot runs half started. The number changes only in the kernel, with a stated reason. A tester in init’s place (test bench) works within the same allowance. A kernel case whose first program needs more works in a budget it carves from system.

• The weights stay. ROOT_WEIGHT is 1,000,000 and INIT_WEIGHT is 1,000. init’s free weight in root is a driver’s, and the rest is split between system (250,000) and users (749,000). Only the budgets that hold processes compete, so what matters is how their weights compare: 1,000 for init, the steward and the drivers, an ordinary weight for other servers, and 100 for a session. Each server runs in a budget of its own, so no program takes a shared free weight by yielding in a busy loop.

init carves each server’s budget from system with the pages, processes and weight its manifest entry names. Only init and the steward ever hold a handle to a system-class budget, and a manifest that grants a server a budget handle is refused (init). The steward holds users and carves each principal’s budget from it, then a fixed sub-budget per label set (steward).

Class is trust, not order

A budget’s class is its parent’s, fixed at creation; budget_create takes no class argument (I8 (class and account inherited)). root and system are class system; users and everything below it are class user. Class decides three things and nothing else:

• a message to or from a system-class budget, and an exit notice into one, is not label-checked by the kernel (R1);
• a system-class caller of budget_usage is not label-checked (the caller’s class decides, not the target’s);
• only a system-class caller may create a child with more labels than its parent (ClassDenied). The caller’s class decides, not the parent’s.

Scheduling never reads class. Every budget is in one stride queue, and what matters is weight: init, the steward and the drivers get large weights instead of running first (scheduling).

Because class is inherited, a handle to a system-class budget is the authority to create more of them, with any labels and any account the rules allow, and to run processes in them. The kernel does not look at the holder’s class for that. What protects system budgets is that their handles are never handed to anything but init and the steward (see Residual risks).

Labels on budgets

Status: built · tested: bench:budget, bench:process-attack, mutation:LabelsAddedByParentClass

A budget’s labels are fixed when it is created. The kernel sorts the spec’s labels and drops repeats, then checks them:

• they must include all of the parent’s, or the call gets LabelDenied: labels only grow downward (I6 (labels only grow downward)), so no child can shed a label its parent carries;
• if they add any, the caller’s own budget must be class system, or the call gets ClassDenied. A user-class process can only make children with its parent’s exact label set.

A spec whose label count is above MAX_LABELS does not decode (TooLarge). What a label means, and who owns it, is the servers’ business (labels); the kernel sees a number, and carries the sender budget’s label set on every message.

Deadlines

A deadline is the kernel’s half of a lease. budget_create takes it as an absolute time in microseconds since boot (the clock time_now reads); FOREVER means none. The kernel sets no maximum: a lease’s longest term, MAX_LEASE (24 hours), is the steward’s rule, and the steward refuses a longer request rather than clamp it (steward). The kernel knows deadlines, not leases.

When a deadline passes, the kernel destroys the budget exactly as budget_destroy would (R10), with nobody asking. Budgets with a deadline sit on one list linked through their pages, and the hart timer is always armed for the earliest (timer). Every kernel entry (a call, a fault, an interrupt) first answers every deadline that has passed, before anything reads the entering process, so a deadline beats any operation that enters after it. A process that never enters the kernel is stopped by the timer interrupt. There is no state, call or interrupt path in which the kernel puts a deadline off. So a deadline always destroys its budget, at the first kernel entry at or after it.

• A deadline already past at creation destroys the budget at the next kernel entry; the handle is dead by the time it is used.
• At an equal instant, blocking-call timeouts are answered first (I13 (every blocking call returns by its timeout)), then deadlines in id order. So a caller whose server’s budget dies at its own timeout gets Timeout with its lend consumed, not Dead with it returned.
• The processes it kills get exit notices with cause killed, blaming nobody (processes). A process still being launched is one of them: a deadline that passes between its process_create and its process_start kills it with no thread ever run, and the launcher’s next process_map or process_start answers NotPermitted. A lease shorter than its launch never runs (bench:deadline-in-launch).
• The destruction’s whole cost is billed to the budget’s parent, after its carve returns, or to the nearest ancestor with free weight above 0 (R10). A deadline is a preemption point.
• A child may have its own, earlier deadline. A later one never fires, because the child dies with its parent. So a sub-budget (a sub-agent’s lease inside an agent’s) never outlives its parent.

budget_usage

budget_usage(h, usage_rec) writes six slots (USAGE_SLOTS): the page limit and usage, the process limit and usage, and the weight limit and carved weight. The free weight is the limit less the carved weight. The record is checked writable before anything is read.

A usage read is a flow from the budget read to the reader’s budget. So a user-class caller reads only budgets whose labels its own budget’s labels contain, and gets LabelDenied otherwise; a system-class caller reads any budget it holds a handle to (R1). The check uses the caller’s budget, not the handle’s stamp.

budget_children

Status: planned · M6 (persist, install, share)

budget_children(h) -> [h] returns a handle to each child of the budget h names, so a restarted steward can find, and destroy, the budgets it created before it stopped. With it, a budget whose last handle was closed is reachable again from any holder of its parent. Nothing else about budgets changes.

Open: direct children only, or the whole subtree; how many handles one call returns, and how a caller pages through a budget with more children than one record holds, within MAX_HANDLES (4096); what the returned handles are stamped with (the caller’s budget, as budget_create stamps, or the stamp of h, so that revoking h revokes them too); whether a holder of h may then create processes and children in a child another holder carved, which is more than h alone gives (with h alone it can only destroy that child, with the rest of h’s subtree); whether handing back a labelled child’s handle to a user-class caller is a flow R1 must check.

Authority

• A budget handle is the right to spend the budget and to end it. Its holder can carve children from it, create processes in it (process_create), read its usage, narrow a mint to it when it is at or below the source’s stamp (objects), and destroy it with everything below it. Handles carry no rights bits, so there is no read-only budget handle.
• Handles reach down, never up. No call turns a handle to a budget into a handle to its parent or a sibling. A holder of a child cannot reach its parent’s limits, beyond the carve it has.
• A new handle is stamped with the caller’s budget (R9): destroying the budget that created a child’s handle revokes that handle, while the child itself survives if it is not below the destroyed budget.
• Class gives a caller two powers: a system-class caller may add labels, and may read the usage of any budget it holds. It also exempts messages to and from the budget from the kernel’s label check (R1). A system-class budget handle held by a user-class process gives that process everything a system-class budget can hold.
• The account is inherited once set (R8): a process cannot give a child a different principal to bill to.
• Who holds which budget handle is policy. init hands servers only revocation scopes, never a budget that holds processes, because a budget handle is a destroy right: a compromised server holding its callers’ budgets could end every session.

Security properties

R6 (charging)

Every kernel object is charged in pages to one budget, and a charge over the budget’s limit fails with OutOfMemory before anything changes. Who pays:

• a budget’s own page: its parent, always (BUDGET_PAGES, 1), and root’s own page to root: root’s limit is the RAM frames the kernel did not keep for itself or for the DMA pool, less root’s own page, so the sum of all charges never exceeds the free frames. A held DMA run is charged to its caller’s budget as well, though its frames are the pool’s, so while runs are held up to DMA_POOL_PAGES free frames cannot be charged for: conservative, never short (devices). A revocation scope is no special case;
• a process object, which holds the exit notice: the creator’s budget, the budget of process_create’s caller (PROCESS_PAGES, 1), until the notice is received or dropped;
• a thread’s IPC page (THREAD_PAGES, 1), its saved registers, its process’s page tables (each until it maps nothing, memory) and mapped pages: the budget the process runs in;
• a handle-table page: the budget of the process whose table it is;
• an endpoint: the budget of the process that created it, its owner;
• an open call’s page: the receiving process’s budget (R4a (open calls));
• a lent page and the page tables that map it: the caller and the receiving process’s budget while the call is open (R3 (lends and abandoned calls)).

A process limit counts PIDs, and every held PID counts once: against the budget the process runs in, for as long as the PID is held, which for a created process is until its object is freed and for a program the loader started is while it lives. It counts there whoever launched the process. If that budget is destroyed while the PID is still held, the count moves to the destroyed budget’s parent (R10). A process_create over the limit fails with OutOfProcesses before a PID is drawn (processes). root holds every PID but the kernel’s, so the limits run out no later than the PIDs do: with every PID in use, every budget refuses with OutOfProcesses (process-fill).

The page counts per object are in objects. A parent’s usage counts its children’s limits and their own pages, never their live usage, so one child filling up changes nothing its siblings or its parent can see.

Page tables are counted before a mapping is made, and the count names each missing table by the span of address space it covers. A missing table at the same index under two different parents (two gigabytes, say) counts twice. Because the count is exact, a mapping that passes the budget check never runs out of pages halfway; the charge and the allocations agree, so a request one table short is refused with nothing charged (R22 (range cost)). Every page a budget uses is on its ledger, and usage stays within limits after every call (I5 (usage within limits)).

R7 (carving)

A child’s page, process and weight limits come out of its parent’s free limits, and the child’s own page comes out of the parent’s pages too. The children never add up to more than the parent; nothing is overcommitted. So an allocation succeeds or fails on the paying budget alone, and a failure says nothing about any other budget. The largest values, and sums that would wrap, are refused like any other excess.

Carving weight moves CPU share to the child; it never copies it. The parent’s stride weight is its free weight. A carve that would leave a budget that holds a process with free weight 0 is refused (InvalidArgument), as is process_create into a budget with free weight 0. The carve returns to the parent, whole, when the child is destroyed (R10).

R8 (accounts)

Status: built · tested: bench:process-attack, mutation:R8AccountFromArgument

A new budget’s account is its parent’s, unless the parent’s is 0; then it is whatever the creator put in the spec. So once a budget bills to a principal, everything below it does too, whatever its creator asks (I8). The boot budgets have account 0, and the steward sets one on each principal’s top budget. The kernel attaches the sender budget’s account to every message it carries, and a server bills or throttles by it (IPC). An account grants nothing by itself.

R10 (destruction)

Destroying budget B, by budget_destroy or by a deadline, destroys B and everything below it, in this order:

1. Mark. B’s weight goes back to its parent first, so that the destruction’s own work is billed at the parent’s restored weight, not the sliver it kept while B held the rest (the deadline path departs from this; see below) (scheduling). Then B and every descendant are marked dying.

2. Kill. Every process running in a dying budget is killed, the caller last if it is one of them. Each gets an exit notice with cause killed, blaming nobody, unless its process object is itself charged to a dying budget.

3. Free process objects. Every process object charged to a dying budget is freed, its process killed first if it still runs elsewhere, with no notice. A notice never outlives the budget that pays for it.

   A process that step 2 or 3 ends is doomed from the mark on: it runs in a dying budget, or its process object is charged to one, because its creator’s budget is dying.

4. Reach messages in flight. Every endpoint a dying budget owns is destroyed: calls and sends blocked on it and receives waiting on it fail with Dead, calls a server took through it are abandoned (R3), and exit notices owed to it are dropped. Every device object charged to a dying budget is destroyed. From the mark on, no message stamped with a dying budget is delivered: a message still queued that was sent through a handle stamped with a dying budget fails its sender with Dead. A call sent through one that a server already took fails its caller with Dead at once, not when the server replies, and is abandoned.

5. Lift. Each dying budget’s work since it entered the queue moves to its parent, bottom-up (scheduling).

6. Sweep. Every handle that names a dying budget, or an endpoint, device or process object that died with one, or that is stamped with a dying budget, is closed in every process’s table. A handle stamped with one inside a message not yet received arrives as 0 in its slot (IPC).

7. Return. B’s page, its page and process limits go back to its parent. The parent’s usage is exactly what it was before B was created (I10 (create-destroy leaves the parent unchanged)), except for what step 8 moves onto it.

8. Move what outlives the carve. DMA pages held in quarantine and charged to a dying budget are charged to B’s parent instead (I16 (DMA pages reset before reuse), devices), and so is every PID still held by a process that ran in a dying budget: one whose object step 3 did not free, because its creator is outside B and has not taken the notice (R6). Both move after the carve came back, and both were inside it, so the parent never goes over its limit.

9. Free. The dying budgets’ pages are freed and they leave the deadline list.

Nothing is delivered while a budget is dying. Every surviving endpoint that lost a receiver or gained a notice during the destruction is pumped once, at its end, when no doomed process and no dying object is left to take anything.

What that end delivers is notices, never a message stamped with a dying budget. Outside a destruction every delivery is made at once, so at the mark nothing a waiting receiver could take is queued. A kill gives the survivors only notices, callers woken with Dead and the dying processes’ freed open-call slots, never a receiver newly able to take a message, and step 4 fails every message stamped with a dying budget. The one thing a delivery inside the destruction could do is hand a doomed receiver a notice owed to a survivor, which putting each endpoint on a list and pumping the list at the end prevents.

A budget is emptied one child at a time by budget_reap, each child destroyed as above (B is the child: its processes killed, the calls its servers held failing their callers with Dead, what was sent through handles stamped with it failed) and the budget kept with its limits, class, labels, account and deadline. The call returns how many children remain, so one call is one destruction, and the caller loops until the count is 0. The child reaped is the first on the budget’s child list, the one created last; the call takes no child handle, so the caller cannot choose, and the order is not a promise. Its authority is the handle, as for budget_destroy: a handle to a child reaches only below that child, never its parent. Once the last child is gone the budget’s usage is what it was before any child was carved (I10, per child). Its class is untouched: it is not made again, which budget_create, taking no class, could not do for users.

root has no parent, so destroying it (init holds its handle) destroys the whole tree: every process ends, and what step 8 would move goes with the tree. The kernel keeps running with nothing to run.

Revocation is complete (I2 (revocation is complete)): no handle, queued message or taken call keeps authority that came through a destroyed budget. Budgets outside B are untouched, including budgets B’s processes created elsewhere and handles to them stamped outside B. A device whose reset fails at the end of a process that used it for DMA is destroyed the same way, at that end: every handle naming it closes, in every table and every unreceived message (devices, R11 (memory)).

A budget whose deadline has passed is destroyed before any operation that enters the kernel at or after that instant: expiry runs first at every kernel entry, before anything reads the entering process. At an equal instant, timeouts expire before deadlines, so a caller whose call a server took, and whose timeout falls with the server budget’s deadline, gets Timeout with its lend consumed, not Dead with it returned (timer).

Every destruction’s whole cost is billed to someone. For budget_destroy and budget_reap that is the caller, as the call’s own kernel time. For a deadline it is B’s parent, after its carve returns, or the nearest ancestor with free weight above 0 if the parent has none; root always has. No part of a destruction is billed to nobody. On a deadline the kernel names the payer once step 1 has returned B’s carve, and after step 9 bills it for everything from the expiry walk that found the deadline on, whatever B’s own free weight (bench:deadline-flood-billed). The frames a destruction frees are zeroed outside the kernel lock by the hart that freed them while every hart idles (frames in flight); that time is billed to the same payer (scheduling). Zeroing any hart still has to bill to a budget the destruction ends is lifted to its payer with the rest of that budget’s debt, between marking the subtree dying and freeing it, so no bill names a budget that is gone. The one exception is root’s destruction, which has no payer and leaves nothing to run: its zeroing is billed to nobody.

stateDiagram-v2
    [*] --> Live: budget_create, or boot
    Live --> Live: handle_close<br/>(the budget stays)
    Live --> Dying: budget_destroy on it<br/>or on an ancestor;<br/>budget_reap on an ancestor
    Live --> Dying: its deadline, or an<br/>ancestor's, passes
    Dying --> Destroyed: kill, free process objects,<br/>fail messages, lift, sweep,<br/>return carve, free
    Destroyed --> [*]

Figure: a budget’s life. It is dying only inside one destruction, which runs in the kernel without preemption.

Failure and restart

• A process in a budget ends: its threads, pages, page tables and handle table go back to the budget at once. Its process object stays charged to its creator’s budget until its exit notice is received (processes), and by R6 its PID counts against the budget it ran in as long.
• A budget’s creator ends: the budget lives on. Budgets outlive the processes that made them; only destruction, of it or an ancestor, or a deadline ends one.
• A budget is destroyed while its own process is in the call: the process is killed last, and the call never returns to it.
• A budget’s deadline passes while a process in it runs: the timer interrupts it, and the kernel destroys the budget before the process runs again.
• The steward restarts: it holds the budgets it created only if it kept their handles; budget_children lets it find them.
• The ledger disagrees with itself (usage below zero, a frame named as a budget that holds none): the kernel stops rather than continue on a broken ledger (I5, I1). No sequence of calls reaches that (I14 (no call panics the kernel)).

Residual risks

• Destruction costs time nobody can interrupt. Destroying a budget runs with interrupts off and is not preemptible; every interrupt, wake and timeout on the machine waits for it, and it dominates lease termination, R39 (leases end). The frames it frees are not zeroed on the way back to user mode: zeroing runs on an idle hart while every hart is idle, one frame a pass (about 30 µs, interrupts off), and on demand, one frame under the lock when an allocation finds the bitmap empty (frames in flight), so the destroyer’s caller and whatever runs next wait only for the walk. The cost must follow the objects the dying subtree holds, not every object page in the system and not every live table. Destruction gives three indexes, handle chains, the dying endpoints’ and stamps’ own lists, and a walk of each dying process’s own frames:

  1. The budget tree is linked downward. Each budget keeps a first_child and a next_sibling beside its parent, so mark_dying, lift_dying and the final free walk the subtree directly instead of scanning 0..=high_frame for budgets below top. The top unlinks from its parent’s list at mark time, with its carve; a refused budget_create unlinks its child on the rollback. The checked build’s check_all_dying proves that after root’s destruction no budget outlives it; the child links themselves are read by the destruction’s walk, not re-scanned by an audit.

  2. Objects are linked to their owner. Each budget heads one chain of the endpoints and devices charged to it (a link word at the same place in both kinds’ frames, read alone), so a destruction ends exactly the dying subtree’s endpoints and devices instead of re-scanning every object frame for one whose owner is dying. Its first walk of the chains destroys the devices, which leave them, each moved to its chain’s head first so that leaving does not walk the endpoints ahead of it; the endpoints stay until the handle chains are closed, and a second walk frees each in a link read and a free. Process objects are not scanned either: each budget heads a chain of the process objects charged to it and one of those whose PIDs it counts (objects). Step 2 kills the live processes on the dying budgets’ counted chains, step 3 frees what is on their charged chains, and step 8 moves what is left on their counted chains onto the parent’s, recounting each; none reads a process object outside the subtree. Only root’s destruction walks every live PID, since then every process dies, init with them, which the loader started with no process object and which runs in root alone.

  3. Handles held outside a budget are chained to it. A handle dies when the object it names is destroyed or when the budget that stamped it is. A handle whose holder runs inside that budget’s subtree dies with its holder’s table, so it needs nothing more. A handle held outside is entered, when it arrives in a table (made, copied, minted or received), in the chain of the budget it depends on: one doubly linked chain for the budget its object is charged to (a budget handle’s object is the budget itself), and one for its stamp. Each budget heads both chains. A process object is the exception: it can be freed while the budget it is charged to lives (its creator’s), once its exit notice is taken or dropped, so a handle held inside the creator’s subtree would not die with its holder. Every handle to a process object, held anywhere, is therefore in a chain headed by the process object itself, instead of in its budget’s object chain. Freeing a process object, inside a destruction or not, walks that chain, never a sweep. The budgets’ object chains carry budget, endpoint and device handles. A device object is freed outside a destruction only after quarantine, which keeps its full sweep. The inside-or-outside test walks up from the holder’s budget, at most MAX_DEPTH steps, and holds for the handle’s life because no budget moves. The cost is a constant on each call that adds or closes a handle, and nothing on a call that only uses one.

     A destruction walks the chains of the dying budgets and of the process objects it frees, and closes exactly the handles that depend on them. The dying processes’ tables were freed whole when they ended: each table page counts its chain entries, a page with none goes without being read, and on the others each slot’s two entry words are read and any entry unhooked from its chain. No live table is swept. The checked build’s check_handle_chains, run once after the walk, checks every live handle’s entries against its holder’s place, and the test-only features handle-chain-fault, which leaves out every stamp entry, and process-chain-fault, which leaves out every process object entry, are what it catches (bench:handle-chain-fault, bench:process-chain-fault); bench:handle-chain-attack holds the dependent handles several levels up, in the dying top’s parent and in its sibling, and handles to a process object the destruction frees while its creator lives: in the creator, inside its budget, and outside it under the live stamp.

     The chain entries make a slot eight words, 64 bytes, so a table page holds 64 handles and a full table (MAX_HANDLES) is 64 pages. A message’s copy of a handle keeps the four-word form, since the chains index tables, not messages.

  4. The endpoints’ teardown reads their own lists. destroy_endpoint once ran three all-thread scans per endpoint, and later budgets_dying two walks of every thread for the whole subtree. Now each endpoint keeps its receivers, its queued senders by R2 (fair waiting) group, the calls owing a notice on it and the calls taken through it whose callers wait; and each budget keeps two chains of what was sent through a handle stamped with it, the queued messages and the taken calls whose callers wait. budgets_dying walks the dying subtree’s owner chains and empties each dying endpoint’s lists: its receivers and senders fail with Dead, the notices owed on it are dropped, and the callers waiting for a reply through it fail with Dead, their calls abandoned, and then every notice owed on it is dropped, those abandonments’ included. Then it empties every dying budget’s chain of queued messages, and then each one’s chain of taken calls. Each fails in list order. No pump runs inside a destruction: each endpoint that may have something to deliver is put once on a to-pump list, linked through the endpoints’ own frames; when nothing more can be listed, one walk of that list takes the subtree’s own endpoints off it (a read per listed endpoint, never a read per endpoint the subtree owns), and the destruction’s last act pumps each survivor on it once. The cost follows the subtree’s own parked messages and calls, never the threads that exist or its endpoint count. process::endpoint_dying drops the exit notices owed on a dying endpoint from its own exits and reporters. Freeing an endpoint’s frame touches only the frame, once its handles are closed (item 2), not the dying budget that owns it: the budget’s whole object list is going with it, and its endpoints’ pages come back in one write.

  5. A process’s frames are found from the process. Ending a process releases the frames it owns by walking its own page tables: the tables themselves, the user half’s pages and the process area’s saved registers, each freed if the ownership table still credits it to the process. Its handle-table, IPC and open-call pages are kernel objects, released with its handles and threads. Nothing walks the ownership array over all of RAM: a term linear in RAM frames is what R12 (scheduling) forbids. A frame it lent stays with the borrower, as R3 says, and a page it borrowed is its lender’s. The checked build’s check_frame_owners scans RAM for a frame still credited to an ended process, at a process’s end and once after a destruction’s walk, never inside it.

  The invariant the five keep is R10 itself: after a destruction no handle, queued message or taken call keeps authority that came through a dying budget (I2), and no handle names a freed frame (I1); the ledger returns exactly (I10). The checked build’s scans over 0..=high_frame (check_process_index, check_irq_index) prove the PID and IRQ indexes name exactly the live objects, check_frame_owners and check_handle_chains the frames and the chains, and they run once off the destruction walk, never scaling it; check_all_dying proves no budget outlives root. The child and owner links are not re-scanned: a missed link shows as an object the destruction fails to end, which the destruction cases exercise. One production full scan remains, destroy_quarantined_devices (message.rs), which a process teardown runs to find the quarantined device objects and stops once it has the machine’s DMA slots. R10’s and the deadline notice’s targets are back at 30 and 40 ms (scheduling); bench:sched-latency asserts both on both widths (seed 3: R10’s p99 is 5,461 µs on rv64 and 5,722 µs on rv32), and bench:budget-destroy-growth shows the destruction does not grow while another budget owns thousands of endpoints and its running process holds a full table of handles to them (a median of 1,211 µs against 1,123 µs alone on rv64, 1,385 against 1,290 µs on rv32). What those cases do not expose is a lease that itself holds many endpoints: bench:endpoint-destroy-full destroys a budget whose running process holds a full table of endpoints it owns (4,095 on both widths, past the containment gate’s full fill of 4,091), and bounds R10’s kernel time from the trace’s records at 30 ms on both widths (10,976 µs on rv64 and 10,985 µs on rv32), the same target the containment gate’s own full-fill run repeats with both leases live.

  Before items 3 and 5 were built, one sweep read every live slot of every table, and ending a process scanned the ownership array over all of RAM. The containment gate’s lease fills its handle table (containment): 4,091 endpoints. At that fill, the destruction ran several times over the 30 ms target, and more while the other lease’s full table was live. The difference was the sweep, about 36 µs for each live handle in the other table. The rest was the lease’s own objects: about 8 µs to close each of its handles and 10 µs to release each of its endpoints, 18 µs an endpoint in all. There were also fixed walks of about 17 ms: the RAM scan once per process, and a walk of every thread for the abandoned-call notices. Under 30 ms leaves a few microseconds per object in the checked build. The chains therefore come with those costs cut: a table freed whole instead of slot by slot, an endpoint released in a few words, and the notice walk joined to a thread walk the destruction already makes. The budget was 25 ms at the full fill on rv32, the slower width. Built, the gate’s full fill measures an R10 p50 of 22.9 ms and a p99 of 23.5 ms on rv32, and 22.1 and 22.9 ms on rv64, over its 20 destructions with both leases live at each deadline’s end (its pinned seed 13; the sweep is on containment). An ending process pumps each endpoint once, after its threads; pumping after each thread instead, the same kernel measures 24.5 and 21.2 ms on rv32. A traced build brackets each process’s end with T and t records, and the bench reports the time inside each destruction beside R10’s. On rv32, with the other lease live (the threads’ teardown measured with those records, the other lines by the bisect that set the budget):

  • the chain walk, 0.2 ms (budgeted under 1 ms);
  • the dying tables, 0.3 ms (2 ms);
  • the processes’ frames, 2.0 ms (1.5 ms; most of it is reading the Sv32 page tables of two processes; 2.5 ms on rv64);
  • the endpoints, 8.8 ms, 2.15 µs each: a 5.0 ms walk that destroys the devices and a 3.8 ms walk that frees the endpoints (8 ms);
  • the threads’ teardown, 3.1 ms (8 ms; 6.7 ms pumping after each thread). Every thread ends first, and then each endpoint their waits served is pumped once, so the cost follows the served endpoints, not the parked calls: the four parked lend calls are one pump of the server’s endpoint, which reads that endpoint’s own lists, not four;
  • the message reach, 1.3 ms (2 ms) when it was two walks of every thread; it now reads the dying endpoints’ lists and the dying budgets’ two stamp chains;
  • the rest, 2.9 ms (3 ms).

  Those are the gate’s fill. At full occupancy, every PID in use and each holder’s budget holding MAX_THREADS threads (129,796 live threads across 510 processes), one holder’s destruction stays within R10’s 30 ms (bench:worst-walk, net of the checked build’s audits, at the 1 ms slice): the run’s two destructions, one near empty and one at full occupancy, take 16.35 and 16.35 ms on rv64 and 17.35 and 17.38 ms on rv32. Their threads’ teardown is 13.1 and 13.8 ms of each, and the rest, about 3.3 and 3.6 ms at most, follows the dying subtree’s own chains (item 2).

• A system-class budget handle is a lot of authority. The kernel lets any holder create system-class children with added labels and any account the parent allows, and run processes in them. The wall is policy: only init and the steward hold one (init). Until init builds the tree, init (or the tester in its place) holds root, system and users, and is trusted.

• A budget handle is a destroy right. Whoever holds a copy can end the budget and everything in it. A server given a budget that holds processes could end them; servers are given only revocation scopes (init).

• A lost budget is carved until its parent is reaped. Closing the last handle to a budget leaves it alive, its limits still carved from its parent, with no handle to it until budget_children exists. A holder of the parent can take it back only with the rest: budget_reap destroys the parent’s children one at a time, the lost one among them, with no way to pick it out. The loss is the closer’s own tree’s, never another budget’s.

• Quarantined DMA pages stay charged. A DMA run whose device did not confirm its reset is held until reboot. When its budget is destroyed, the charge moves to the parent, which keeps paying for those pages until it too is destroyed or the machine reboots (devices).

• Usage reads and OutOfMemory are signals. A budget_usage read and a failed carve tell the reader about the budget it names, and only a budget it holds a handle to. Covert and timing channels are out of scope (TENETS).

Why

• One object, five jobs. Accounting, CPU share, revocation, labels and billing identity all follow the same tree, so there is one thing to create, one to destroy, and nothing to keep in step.
• Everything costs pages, threads, handles, endpoints and budgets included, so one number bounds every kind of exhaustion. Processes are counted apart only because PIDs are address-space tags, which are scarce on rv32; so the count follows the PID, once per PID held, in the budget the process runs in. The steward and init launch everyone’s processes, and counting them in the launcher would pool every principal’s PIDs in one budget.
• Carved, never overcommitted. An allocation that fails on the caller’s own budget reveals nothing about anyone else’s. A parent counts its children’s limits, not their usage, for the same reason.
• A budget’s own page is its parent’s. A child cannot use up the page it lives in, and a revocation scope, with zero limits, needs no special rule.
• A lend is charged to both sides. A server’s budget covers its open lends up front (256 open 9P calls of 16 pages each is 16 MiB), a server that cannot pay does not take the call (R4 (delivery)), and no budget is ever over its limit.
• Class is inherited, with no class argument. A class check on budget_create alone would guard one of three doors (process_create and budget_destroy are the others). Inheriting it leaves one door to guard: never hand a system-class budget to anything but init and the steward.
• Class is trust, not order. One stride queue by weight means nothing jumps the queue by being trusted; init, the steward and the drivers are served first by being given more weight.
• The kernel keeps deadlines, the steward keeps leases. A deadline is a time, which the kernel can enforce without a policy; how long a lease may be is policy, and lives with the policy.
• Bounded depth, because revocation and “is this below that” walk the ancestors.
• A budget is its own page, so creating budgets never fills a kernel table that other budgets need.

Scheduling

The kernel runs threads from one stride queue over every budget with a runnable thread. Each budget has a pass; the lowest pass runs next, for a slice of at most 1 ms, and running raises the pass in inverse proportion to the budget’s free weight. There is no priority: init, the steward and the drivers are scheduled by weight like everyone else. A waking budget joins at no less than the queue’s current minimum, a wake never preempts, and every run is charged, however short it is and however it ends.

Purpose

CPU is a resource like pages, and a hostile budget must not get more of it than its share, nor delay anyone else beyond its weight. The scheduler has two jobs: hold every budget to its weight whatever pattern of running, sleeping, exiting and budget churn it tries, and keep the steward and the drivers responsive enough that a person can end a session under load. It does both with one mechanism and no exceptions, so the rule that contains a hostile agent is the same rule that serves the steward.

Interface

One flat stride queue

Every budget with a runnable thread is in one queue, whatever its class. There is no priority, no second queue and no flag that jumps it. The kernel runs the queued budget with the lowest pass, and running raises its pass by its runtime times STRIDE (2^20) divided by its weight. So over any stretch in which budgets stay runnable, each gets CPU in proportion to its weight. On several harts each hart picks the lowest-pass budget that has a runnable thread no hart is running, so a budget runs on as many harts as it has runnable threads. Its stride state stays one per budget: each hart charges its own runner, under the kernel lock, to the budget’s one pass. A reconcile keeps a budget queued while any hart runs it.

The weight the queue uses is the budget’s free weight: its weight limit less what its children carved (R7 (carving)). Carving moves share to the child and never duplicates it. Weights are 32-bit and matter only relative to each other. At boot the kernel gives root 1,000,000; system gets a quarter (250,000) and users the rest less 1,000 (INIT_WEIGHT), which root keeps so that a process in it has free weight (budgets). Below that, the budget that carves a child chooses the child’s weight.

Class (system or user) decides trust, never order (budgets). A system-class server doing a user’s work waits its turn like the user.

Within a budget, threads take turns. Each pick runs the budget’s next runnable thread that no hart is running, after the one it last picked, in (pid, tid) order, wrapping. sched-round-robin holds one budget’s four threads, two processes of two, to that order on one hart: each thread notes when the CPU comes back to it after a gap of over half a slice, and over twelve rounds the four run the cycle their first runs set, in (pid, tid) order from the cursor, each once a round, wrapping, with their counts within a tenth of each other (over 100 ms, rv64: 25, 24, 24 and 24 slices, counts 589,056, 570,624, 564,480 and 568,832; rv32: 24, 24, 23 and 23 slices, counts 199,936, 201,984, 198,912 and 193,280). The code is kernel/src/sched.rs, which keeps each budget’s scheduling state in the budget’s own frame, and libs/stride, which holds the arithmetic, the ranks and the order of steps. libs/stride is #![forbid(unsafe_code)] and has no dependencies.

Preemption points

The running thread keeps the CPU until one of these:

• its slice ends: SLICE_US (1,000 µs) from its return to user mode after the pick;
• it blocks, exits, faults or is killed;
• a budget deadline fires.

Nothing else takes the CPU. A timeout expiring or an interrupt firing only makes a thread runnable; it runs when the queue next picks it. The hart timer is always armed for the earliest of the slice end, the next timeout and the next budget deadline (timer).

On several harts a timeout is answered at whichever kernel entry first comes after it is due, on any hart: a timer interrupt, another budget’s call, or kmain‘s own. That entry deschedules no runner whose slice has not ended for its own reason (its slice’s end, a block, an exit, a fault or a deadline): the woken thread first runs at a pick, an idle hart’s or one after a runner left for such a reason. sched-wake-no-preempt proves it at one hart nap by nap, each against the slice that follows it; sched-wake-no-preempt-harts judges it at two, each wake at the entry that made it, its naps’ ends stepped through the slices’ phases, and needs at least twenty of its hundred and twenty wakes answered where they could have preempted, mid-slice or at another budget’s call (57 to 101 at a call on rv64 and 65 to 74 on rv32, five runs a width alone and three with the timer’s placement, whose one hart armed for a sleeper’s timeout moves where a wake is answered run to run; the floor is a third of the least). Whether a slice ended at a timer interrupt the oracle decides itself, from the decision’s inputs the trace records (its end and now), so a slice that ends during the entry’s own expiry counts as ended, as the kernel ends it. Under icount a wake comes mid-slice on rv64 (1 to 61 across runs; 26 to 35 before the placement) but at most four times on rv32 (0 to 4), whose armed hart takes its interrupt only at its next turn, after the other hart’s call has answered the timeout; so sched-wake-no-preempt-harts-mttcg, the same program where the harts run at once, needs five mid-slice. How many come is the host’s race: 49 to 55 on rv64 and 48 to 57 on rv32 with the two harts on eight host cores (three runs a width), 41 to 74 alone on the quiet core set with the placement, 69 to 75 beside other cases, as few as 5 beside a whole bench’s load, and as few as 3 with the two vCPU threads and QEMU’s I/O thread sharing two cores, so the case runs on the quiet core set, and a read at the floor is re-run alone before it is believed. A kernel built with wake-preempts, whose timeout wake preempts the entering thread as a deadline does, fails both on both widths, in recorded negative runs (on rv32 under icount: a wake took hart 0 from budget 37).

A device interrupt only wakes too. sched-irq-wake runs a driver stand-in on the goldfish RTC’s alarm beside an equal-weight spinner, so every alarm interrupts the spinner mid-slice, and the oracle requires each device interrupt that claimed its source and woke the driver to return to the spinner, which runs to its slice’s end before the driver is picked (irq_wake_no_preempt): 60 of 60 alarms on both widths, on one hart. It also refuses a device interrupt that began no destruction and returned otherwise than to user mode. No kernel feature makes a device wake preempt, so the check’s negative is its floor: asked for 61 proofs of 60 alarms it fails, naming the 60 (a recorded run).

A budget deadline preempts whatever runs, because the destruction lifts passes and removes budgets, so the queue must be picked again. A thread that entered the kernel just as the deadline fired takes its trap again when it next runs. sched-deadline-preempt makes empty budgets due 1.3 ms ahead, one at a time, beside a spinner, so the deadlines fall at every phase of the two runners’ slices, and the oracle requires every timer interrupt that destroyed another budget by its deadline to leave for kmain with its runner requeued and the hart’s next event a pick, never to return to the runner (deadline_preempts): 94 preemptions on rv64 and 80 on rv32 over 2.5 s, every one mid-slice (the checked build’s audits after each destruction take most of the window: 78 audits, 356 ms, in the first 300 ms tried). The deadlines a runner’s own call finds due preempt it too, outside the trace’s interrupt brackets, and are not counted. Asked for 200 the check fails, naming the 94 (a recorded run).

The kernel itself is never preempted. It runs with interrupts off (sstatus.SIE clear) and takes the timer and device interrupts only from user mode or while idle, so a system call or a destruction runs to its end. Picking is done by kmain, the kernel’s own loop (PID 1). It runs its pick through a private S-mode ecall into the kernel’s trap handler, which saves kmain’s context as it saves a thread’s.

So a slice’s end picks again. When nothing is due for kmain’s expiry to answer first and no other thread of the running budget waits for a hart, the trap picks where it is (sched::repick): the stride takes the steps of the round trip through kmain, in its order (Harts::repick), the budget charged and requeued behind its equals, the entry reconciled, the queue picked. If the pick is the same budget its thread runs on, a new slice from its return, with no switch to kmain and back; if it is another budget’s thread, the trap switches into it there (sched::switch_here), with the steps of kmain‘s switch: the thread it ran made ready, the pick’s address space and thread activated, instruction fetch fenced, one return, which deschedules the budget switched from and starts the pick’s slice. Only a slice’s end that finds something due, or whose budget has another thread waiting for a hart, goes through kmain, as every one did before. The differential takes slice ends through it at 1, 2 and 4 harts and requires each to leave the queue as the round trip leaves it, its thread counted as the process table counts it there, and to pick what the model picks. The trace records the requeue and the pick, and the hart’s new runner at the return when it switched (H), no change of it when the thread ran on; the oracle counts the thread as waiting only at a slice’s end that picked its own budget again (the scheduler oracle). sched-timer-entry bounds what a slice’s end costs the kernel: two spinners and nothing else, so every timer interrupt from user mode ends a slice, and the oracle bounds their lock sections, trap to return, net of the checked build’s audits at one hart: the p99 at 2,000 ticks, the steady entry, which measures 951 on rv64 and 1,452 on rv32 (five runs a width alone, p50 949 and 1,424; 930 and 1,415 before the timer’s placement read the harts’ runners at each re-arm, 15 and 26 ticks, and 945 and 1,441 before its one-hart rule for an item whose payer runs nowhere asked every hart’s arming, 6 more: the hart timer), and the longest at 5,000, the cold first preemptions of a phase, 3,552 and 4,452 (at two harts, where icount’s one clock counts the other hart’s instructions too, they are recorded: p99 5,447 and 7,378). In a release build the slice’s end of a thread that only computes, alone on its hart, is about 4,200 kernel instructions on rv64 and 6,700 on rv32 (QEMU’s exec log), about 3.4 and 5.4 % of a hart at the 1 ms slice; through kmain it was 9,000 and 13,000. One that switches to another budget’s thread, two such threads sharing a hart, is about 7,050 and 10,600 (the same log, sched-timer-entry’s program), 5.6 and 8.5 % of a hart; through kmain it was 8,500 and 12,200.

The current minimum and ties

A budget wakes when it goes from no runnable thread to one. Its pass becomes max(own pass, floor). The floor is the current minimum: the lowest pass among queued budgets, the running ones included, each once, at the pass it was last charged. The floor only rises, and it holds while the queue is empty. So a budget that slept while others ran, or through an idle gap, comes back at the floor and not with credit it banked while away. The floor is raised only when it can have moved (a budget at it was charged or left, or wakes filled an empty queue), from ranks the queue keeps beside its slots, each written where the queue changes a queued budget’s pass or tie; the pick compares the same ranks. Neither reads a budget’s frame, which stays the record: a checked kernel audits the ranks against the frames with the marks’ audit. So a slice end’s scheduler work is under 3 µs per queued budget (2.4 µs measured in a checked build, “Charging”), the frame reads it makes being its hart’s running budget’s own.

On several harts the floor leaves out a capped budget, one whose weight’s share of the harts is more than it has runnable threads. Running every thread it has, its pass lags, and counting it would hold the floor below the budgets that share the other harts, so a waker would enter far behind them and take their harts until it caught up. The cap is found as the shares are: in descending weight per runnable thread, a budget is capped if w x H > k x W (H the harts, k its runnable threads, waiting or on a hart, W the queued budgets’ free weight), and the next is tested with the capped one’s harts and weight taken out. Only a budget capped already, or one every thread of which runs on a hart, is tested: a budget with a thread waiting for a hart is not taking the harts its weight would give it, so it stays in the floor and its weight in W. A budget a switch takes off its hart with its own thread requeued (its slice ended or it was preempted) counts that thread as running: its own requeue is no wait, but a sibling still waiting after a block is. A queued budget whose last thread just ended, which the entry’s reconcile takes out, counts for neither, unless no queued budget has a thread: then the floor rises to the lowest pass, as at one hart. At one hart no budget is ever capped. When every queued budget is capped, fewer runnable threads than harts, the floor rises to the highest of their passes instead of holding: uncontested time banks for no one, so a budget waking then cannot take the others’ harts later for time no budget wanted. A budget that stops being capped is lifted by what the floor rose while it was capped: it cannot bank what it had no thread to run. Its lift target starts at min(own pass, floor) when it is capped and follows the floor from there, so a lag it had then it keeps, and the target needs no hold while a thread of it waits: the capped budgets’ threads total at most H - 1, so they all run at once and a capped thread never waits long enough to be owed, and one lagging below the floor outranks every budget that is not capped. Without these limits a carve could cap an equal-weight victim while its thread waited behind the carver’s two on both harts, and the carve’s return lifted it to the carver’s pass, erasing what it had waited: 82 times in sched-budget-churn-shell‘s window at two harts on rv64, 7.4 ms of its hart time each, and the victim kept 398 of 1000 (568 with them). The model’s carve waiter scenario is that pattern (R12UncapForfeitsWait); heavy capped has a capped budget whose own slice ends fall inside the others’ and gain it nothing; contracts hold that a budget with no thread raises the floor to no pass of its own (R12EmptyHoldsFloor) and that a heavy budget is capped by the raise its own slice end makes (R12RequeueWaitsForCap), but not by a block while its sibling waits (R12BlockLeavesAsRequeued). With more than one hart online the queue keeps each budget’s free weight, its threads no hart runs (as the kernel’s settle counts them), its harts and the pass a lift would take it to beside its slot, counted afresh as a hart comes online and kept by no scan at one hart, so every floor raise finds the cap set in one scan, keeping the top H - 1 by w / k, linear in the queue, with no frame read but a lifted budget’s. A checked kernel audits the set, with the marks’ audit, against water-filling done its own way over every queued budget.

A pick takes the lowest rank, (pass, tie, id). At an equal pass:

1. a waker ranks ahead of a budget that was requeued;
2. of two wakers, the later kernel entry’s ranks first;
3. within one entry, the lower budget id first (ids are the kernel’s, I12 (ids never reused));
4. requeued budgets run in the order they were requeued.

The tie key encodes this. Each wake takes front - 1, and one entry’s wakes are processed in descending id, so the lowest id ends frontmost. Each requeue of a still-runnable budget takes back + 1. Both counters reset when the queue empties. Wakes are reconciled once per kernel entry: as the kernel leaves, budgets that lost their last runnable thread leave the queue and budgets that gained one wake. The reconcile visits only the budgets whose runnable state changed in the entry, with the same wakes and leaves, the wakes in the same order: each budget counts its ready threads, and a change of a process’s ready threads marks the process, whose count then moves to its budget. Leaves have no order a pick can see. Ranking later wakers first starves nobody: a waker that has run is charged, its pass rises above the floor, and it no longer ties.

bench:sched-ties runs a kernel built with the scheduling trace (R23). The bench’s own oracle (tools/testbench/src/sched_oracle.rs) rebuilds the order from the trace’s events with its own reading of the four clauses and checks every pick, keeps its own floor, and requires every pass never to fall but at a weight change, which it recomputes (the lead follows the weight). In the guest, two groups of three each wake in one entry, by one destruction each, and each group runs lowest id first. The oracle alone judges which group runs first: a slice end between the waker’s two destructions may run the earlier group before the later one wakes.

flowchart TD
    K["kernel entry: a call, an interrupt,<br/>a timeout, a slice end, a deadline"] --> D{"does the running<br/>thread leave the CPU?"}
    D -- "no: a wake never preempts" --> REC
    D -- "yes: it blocked, exited, faulted,<br/>its slice ended or a deadline fired" --> F["charge: t = rem + ticks x STRIDE<br/>pass += t / w, rem = t mod w<br/>(at least 1 tick)"]
    F --> S{"still has a<br/>runnable thread?"}
    S -- yes --> RQ["requeue behind its equals<br/>(tie = back + 1)"]
    S -- no --> LV[leave the queue]
    RQ --> REC
    LV --> REC
    REC["reconcile: each budget that gained a<br/>runnable thread wakes, highest id first,<br/>pass = max(own, floor), tie = front - 1"] --> FL["floor = max(floor, lowest queued pass)"]
    FL --> R{"a pick due: the thread left,<br/>or its slice ended?"}
    R -- no --> RUN[the hart's running thread resumes]
    R -- yes --> P["the queue picks the lowest (pass, tie, id)<br/>and runs that budget's next thread<br/>after its cursor, for up to 1 ms<br/>(at a slice's end the trap picks where it is;<br/>otherwise kmain does)"]

Figure: the pass and wake rule at one kernel entry. w is the budget’s free weight.

Charging

Runtime is counted in timebase ticks at the trap boundary. There are two ways into user mode (resuming a thread, returning from a call) and one way out (the trap handler). On every trap from user mode the kernel adds the user time since that hart’s last return to the pending runtime of the budget whose thread it ran. So no path runs user code unaccounted, whatever ends the run.

Pending runtime is folded into the pass at a deschedule, before a weight change, at a destruction, and when work is billed to a budget that is not running:

t = rem + ticks x STRIDE;   pass += t / w;   rem = t mod w      (w: the free weight)

• The remainder is exact, so a run split into pieces costs what one run would, at any weight. Without it a weight above STRIDE would round a one-tick run to nothing.
• A deschedule charges at least MIN_CHARGE (1 tick), so a run too short for the clock to see is not free.
• One fold counts at most RUNTIME_CAP (2^40 ticks), so the product fits 64 bits on rv32 and rv64 alike. The pass is a 128-bit number that is only added to and compared, so it never wraps.
• A weight change (a carve, or a carve returned) folds first, so runtime is charged at the weight it ran at, and then rescales what the budget owes to the new weight (the lead follows the weight).

Kernel time is billed as well:

• a system call’s time is its caller’s;
• an expired timeout is billed to its thread’s budget, and a deadline’s destruction as below, each with its share of the walk that found it. The timer is armed for a timeout only when its thread blocks; a wait that ends before its timeout leaves it early, and the walk that finds the wait gone is billed to that thread’s budget. The rest of an entry that found either, the timer’s own handling included, is billed to the budget it found last: the budget it interrupted pays for none of it. Each bill closes its interval at the tick that opens the next, so a bill’s own handling is in the interval after it and no part of a timeout’s expiry is nobody’s (residual risks). A timer interrupt that found neither is the budget’s its hart runs when it ends that budget’s slice, and nobody’s otherwise;
• an interrupt’s handling is billed to the owner of its device object (R5 (interrupts)), the budget it is charged to: system, which the boot charges every device to, whoever holds the handle (sched-irq-wake’s oracle requires every device interrupt that claimed its source to charge the budget the program marks, system, and lets it charge only that and, for its return, the budget it interrupted: 60 alarms charged system 286,980 ticks on rv64 and 208,903 on rv32 in the checked build, 4,783 and 3,482 each, and the interrupted spinner 19,476 and 31,488 for their returns); one with no device object, to nobody; a device interrupt that claims nothing, its source claimed first by another hart, is billed as a timer interrupt that ends no slice: the rest of it after its expiry is the budget its expiry billed last, or nobody’s, never the budget it interrupted; so is one a deadline took at its entry: the expiry every entry answers first destroyed a budget, and the entering thread gave up the hart before the controller was asked (preemption points), leaving the source pending for the next entry. The trace records it with no claim, the destruction inside it and a preempting return, and the oracle accepts a missing claim only so marked (the real steward’s two-hart traces, where a deadline passes while the other hart holds the lock, carry one or two a run; one hart’s none);
• kmain’s pick and switch into a budget are paid by the budget picked, whatever ended the run before: a block or an exit is paid by its actor, a timer entry’s handling by the budget it served, and the pick that follows by the budget it picks (a pick that cannot run leaves the next pick owing it; a pick of nothing is nobody’s);
• idle time is nobody’s.

A slice end that switches budgets costs about 0.056 ms of kernel time on rv64 and 0.085 ms on rv32 in the release build under QEMU (about 7,050 and 10,600 instructions, two spinners sharing a hart), billed to the budget picked after it: the trap, one SBI timer call, the deschedule, the reconcile, the pick and the switch, made where the trap is (preemption points), with under 3 µs of it per queued budget (the checked, traced build measures 2.4 µs per queued budget per slice end from three to seventeen queued, net of its audits, over a fixed 175 µs). At a 1 ms slice the nine spinners of bench:sched-large-weight-release do 0.91 (rv64) and 0.87 (rv32) of the useful work the 10 ms build does; the case requires 0.85, the fixed part being the rest. A count of user work still falls short of the window: in the checked build, bench:sched-share‘s three spinners count 975 (rv64) and 964 (rv32) of 1000 of what the loop’s rate alone would fill, the rest being what a slice end that switches budgets costs over a lone spinner’s, the checked build’s audits among it (the marks’ audit after about every slice end, the queue’s ranks audited with it), so the case judges each spinner’s share of what the three counted (600 of 1000 for the weight-300 spinner on both widths, against its 600; 585 and 578 of the window), not of the window. It reports the sum beside, with no verdict; bench:sched-share-release requires the release build’s sum to reach 960.

The top of a destruction returns its carve to its parent before any of the destruction’s work is billed. So the parent, often the caller of budget_destroy, pays for the destruction at the weight it has once the child is gone, not at the sliver it kept while the child held the rest. In bench:sched-destroy-billing a parent that kept 10 of 1000 destroys the child holding 990 and is back on the CPU within twice the destruction’s cost and four slices; billed at 10, it would wait for seconds.

Every destruction’s whole cost is billed to someone. For budget_destroy and budget_reap that is the caller, as the call’s own kernel time. For a deadline it is the top’s parent, after its carve returns, or the nearest ancestor with free weight above 0 if the parent has none; root always has. No part of a destruction is billed to nobody (R10 (destruction)). On a deadline the kernel names the payer once the carve is back, and bills it after the subtree is gone for everything from the walk that found the deadline. In bench:deadline-flood-billed a creator floods its own budget with empty weight-0 budgets on short deadlines: its count falls as the flood grows from 16 to 64 a round, and an equal-weight victim keeps its half. With the bill planted out, the victim fell to 137 of 1000.

The frames a call or a destruction frees are zeroed outside the kernel lock by the hart that freed them while every hart is idle (memory), and that time is part of the work: when the hart takes the lock back it is billed to the budgets that were paying when the frames were freed (the caller, the destroyer, a deadline’s payer), split by frames. No thread’s slice pays for it, since no hart zeroes on its way to user mode; a frame an allocation zeroes because it found no free one is that allocation’s own kernel time. A payer destroyed before the bill does not take its share to nobody: its destruction lifts the share to its own payer with the rest of the dying budget’s debt (R10), root’s alone excepted.

The trace checks every timer interrupt from user mode (bench:sched-timer-flood): after its expiry it charges only the budget it found last, an expired item’s or a wait’s that ended before its timeout, and with neither, only the budget it interrupted, when it ends that budget’s slice. Against 30 sleepers a microsecond apart, the same with 64 staggered budget deadlines, and two waits answered at once 15 ms before their timeouts, the victim gets 473, 473 and 477 of 1000 net on rv64 and 468, 469 and 481 on rv32, and no timer interrupt is nobody’s. The last case requires interrupts that found the attacker’s waits ended early inside the victim’s window, so the check cannot pass for want of them: 73 on rv64 and 19 to 20 on rv32. Its attacker holds no other timed wait that times out within the window: one due at every expiry walk of its process would reset the timer’s hint each slice, and a hint 15 ms ahead would never come. A sleep of a microsecond has passed before its call would block, so it arms nothing; when every call armed the timer, each such sleep made an interrupt that found nothing. With the rest of each timer interrupt billed to the budget it interrupted (timer-tail-billed, the recorded negative run), the check fails on both widths: the victim pays for the attacker’s waits that ended early.

A server that works for a caller spends its own budget’s CPU: no time is donated (Residual risks). CPU charging is separate from page charging (R6 (charging)). The model charges runtime, and three kinds of kernel work billed to a payer: a deadline’s destruction (R12DeadlineWorkUnbilled), a timer’s expiry of the timeouts it ends (R12TimerWorkUnbilled), and the pick and switch into a budget (R12SwitchBilledToPrevious). Billing other kernel work is the kernel’s alone, and the boot cases are its only check.

Against threads that each run nine tenths of a slice and exit, beside a main thread polling on a 1 ms timeout (sched-exit-churn‘s first share), the victim got 439 of 1000 net on rv64 and 432 on rv32 while it paid the pick and switch at each of its own slice ends, about 90 µs at the 1 ms slice, a tenth of what it was charged, and while each expiry of the attacker’s poll left about 50 µs, its bills’ own handling, to nobody. Billed as above it gets 492 and 487.

Inheritance

A child budget enters at e = max(floor, parent's pass), and keeps e as its entry. A running parent is charged first. So a child never starts behind the parent it came from, and making a child buys no turn.

When a budget is destroyed (R10 (destruction): descendants first, bottom-up), its own work since entry moves to its parent:

W = (pass - max(e, floor))+ x w_child + rem_child
parent's pass = max(parent's pass, floor) + W / w_parent      (the remainder carried)

w_parent is the parent’s free weight after the child’s carve has returned. A parent below the floor starts from the floor, without its remainder: it cannot bank what it did not run. Only work after entry counts, so creating and destroying a budget that never ran moves nothing. The child’s debt adds to the parent’s own lead instead of hiding under it, so a parent that spins and churns children pays for both.

bench:sched-budget-churn runs a churner that creates a weight-1 child, lets it run a slice and destroys it, over and over (blocked, spinning, by a deadline, and through fresh intermediates), against an equal-weight victim who keeps half; the oracle recomputes every lift from the trace. Its last variant, a shell that keeps giving a child half its weight and taking it back with no run between, leaves the victim at least half, and the recomputed lifts show that creating and destroying moved nothing. Its victim’s share has no ceiling: the shell pays at its halved weight for what it runs while carved, its own calls included (running while carved down), so how far above half the victim gets follows the kernel’s speed.

Running while carved down

A budget that runs while most of its weight is carved away accrues its lead at the small weight it kept, and owes that runtime at whatever weight it has later (the lead follows the weight). A destroyed child’s work is lifted at the child’s weight at its destruction, whatever the child kept while it ran. That only over-charges the budget that carved; it never under-charges, so no share is gained by carving. In bench:sched-carve-inflation a spinning budget that carves spinning children, one deep and four deep, gets at most half against an equal victim.

A budget that holds a process keeps free weight above 0. A carve that would take its last free weight gets InvalidArgument, and so does process_create into a budget whose weight is all carved (R7).

The lead follows the weight

What a budget owes is runtime, and a weight change keeps it exactly. Every weight change, a carve and a carve returned alike, folds at the old weight and then converts the budget’s lead and remainder to the new weight, the same way a lift converts a child’s work:

W = (pass - floor)+ x w_old + rem
pass = floor + W / w_new;   rem = W mod w_new

So a carve raises the lead by the ratio of the weights and its return lowers it by the same ratio, and a carve returned with no run between leaves the budget where it was. If the carve raised the floor (the budget had the lowest pass), the return converts from the higher floor and the budget ends a little higher: over-charged, never ahead. Both directions are needed: rescaling only on a return would let a budget carve just before a burst and return just after, and its lead would shrink at the return without having grown at the carve. A budget at or below the floor owes only its remainder, and waking would lift it to the floor anyway. At a destruction the carve returns first, so the parent’s lead is converted before the child’s work is lifted onto it at the parent’s restored weight (inheritance). A budget at weight 0 holds no process, and what it owes is stated at weight 1 meanwhile, so it is carried exactly through 0: carving everything away and then getting back only part of it is the same as the one carve from the old weight to the new.

libs/stride’s rescale is the conversion; the model makes the same one, and the bench’s oracle recomputes every weight change a traced kernel records, the one place it lets a pass fall. A host test checks that a carve and its return leave pass and remainder unchanged. In bench:sched-carve-return a budget of weight 1000 carves 999 away at the start of a slice, runs on the 1 it kept until nine tenths of the slice into it, and takes the weight back: from then on it gets 496 to 499 of 1000 against an equal victim. With the remainder alone rescaled, as before, it got 0.

Responsiveness

No wake latency follows from weight. Unless a hart is idle, a wake waits out a running thread’s slice, a waking budget keeps a pass above the floor if it has one, and several budgets can tie at the floor. So wakeup is prompt but not bounded, and responsiveness is a measured target under a named workload, not a bound derived from the queue.

The workload (tests/programs/src/bin/sched-latency.rs): a driver stand-in (weight 1000, from system) that waits for the goldfish RTC’s alarm interrupt; a steward stand-in (1000, from system) that sleeps on timeouts, destroys leases by hand after a timeout (its decision) and waits for other leases’ deadlines; and N spinning sessions of weight 100 from users, for N = 1, 4 and 16. At N = 16 a spinning server of weight 1000 joins them. Each run takes 200 wakes and 50 destructions of each kind, on QEMU, on rv64 and rv32.

Targets are guest instructions. The case runs under -icount shift=3,sleep=off with the RTC on the same clock (-rtc clock=vm; tests/sched-latency.toml): every guest instruction advances virtual time by 2^3 ns, and idle time skips to the next timer deadline. So 1 ms is 125,000 instructions, and each target below is that many instructions; the milliseconds are for reading. Host load does not change a result.

Targets exclude the checked build’s audits. The case is a checked build, since the trace needs one (R23). A checked build runs full audit scans after each destruction and at each process-object free, and a release build compiles none of them. It also checks the reconcile’s marks. Each reconcile asserts that every budget it visited is queued exactly when it has a ready thread. At most once a slice, and whenever the hart is about to idle, a full walk of every live process must find the runnable budgets the marks hold. So a mark missed in one entry is found within a slice of the next reconcile that visits a budget, or at the next idle. A miss that a later change undoes before then is not seen, and costs a budget a turn late or lost, never a wrong thread run. Each target counts the kernel a release build runs, a share as well as a window, so an audit neither fills a window nor moves the schedule. The audit time inside each window, a share’s included, is subtracted, from the trace’s audit records, and reported beside it (checked builds). The scheduler does not see an audit either: its time is charged to no budget, and its hart’s running slice’s end and the start of the kernel time being billed both move forward by its length, so the thread that ran it is picked and preempted as in a release build (sched::audit). With two full handle tables live, the audits are about 24 ms after a destruction and 8 ms at a free.

Measured at seed 3 with the 1 ms slice in the checked, traced build, p99 in µs, net / gross (audit time inside the windows): the audits hold the deadline notice, which waits out the audit after its own destruction, and little else. They are the sixth sweep’s seed 3, the seed the gate pins; the earlier sweeps’ figures stay as measured.

The run’s 49,535 audits total 12.7 s (rv64), and its 50,037 total 15.3 s (rv32), of the hart; R10 itself has none inside it, which the oracle asserts. Beside each destruction’s R10 time the oracle reports its threads’ time: the processes’ threads ending inside it, their pumps included (the trace’s T and t records), at seed 3 a p99 of 54 µs on rv64 and 60 µs on rv32. In the containment gate, with two full leases live at a deadline’s end (seed 13, at one hart), the deadline notice’s p99 is 25,794 µs net and 95,579 µs gross on rv64, with 1,158,114 µs of audit inside its windows, and 26,197 µs net and 97,703 µs gross on rv32; the sweep is on containment. With the audit after a destruction left unstamped (audit-unstamped, the recorded negative run), it is 84,710 µs net on rv64: the target misses, since the oracle subtracts only what the trace shows it. With each audit’s time billed to the budget that ran it and counted against its slice (audit-billed, the second recorded negative run), it is 44,761 and 45,577 µs net: the target misses. The steward stand-in spends its slice on the audit at the first killed notice, is requeued, and the victim and a hostile budget run a slice each before it takes the second.

A share is judged from the same trace: what the kernel charged the budget in the window, against what it charged every budget, never a count, since under icount a count is the machine’s instructions (checked builds). An audit is charged to no budget, so every share is net of the audits, and on several harts net of the lock waits too. In a checked build only, a hart’s wait for the kernel lock behind another hart’s audit is billed to no one either, and the waiter’s slice’s end moves by it (the trace’s y). That changes the schedule as well as the bill: an excused waiter keeps its slice, stays on its hart and meets the next audit. At two harts deadline-flood-billed-traced’s victim, whose creator’s destructions each run a 20 ms audit, moved from 875 to 413 of 1000 on rv64 with it, from one mode of its share to the other; with the lift target (“The current minimum and ties”) it kept 482 to 877, by where the destructions landed; with a destruction armed on the creator’s hart it keeps 919 to 924 or 507 to 530 under icount, by which hart’s entry first reaches a deadline that passed during the destruction before it, and 762 to 802 where the harts run at once (residual risks, timer). Each is owed its water-filling share, which at one hart is its weight’s; the victims of churn, floods and gaming are owed at least theirs. Measured at 1 ms in the checked build, of 1000, rv64 / rv32:

sched-large-weight‘s users and sched-server-busy judge a ratio of counts between budgets alike, which the machine’s rate leaves as it is: the least user gets 992 and 988 per 1000 of the users’ mean, against a floor of 900, and the server’s work for A is 351 and 363 per 1000 of the users’ mean (one hart, rv64 then rv32).

The gate runs one pinned seed. The guest’s boot RNG seed decides the PIDs the kernel draws, which shift instruction counts and so the phase of every later event; with it pinned, a run repeats exactly, and the case prints the seed so that a failure replays. One seed hides the spread, so a sweep of about 16 seeds measures it. A target that the stride rank decides (how many spinners’ slices a waking budget with a lead lands behind) is the sweep’s worst case plus a stated margin. The sweep’s seeds and worst case are recorded here with the target they set.

In instructions: 15 ms is 1,875,000, 25 ms is 3,125,000, 30 ms is 3,750,000, 40 ms is 5,000,000, 50 ms is 6,250,000, 95 ms is 11,875,000, 125 ms is 15,625,000, and one 1 ms slice is 125,000.

At 2 harts the targets above are gated; at 4 they are recorded (gate_harts). Under icount with several harts the clock counts every running hart’s instructions: the harts take turns on one host thread, so a millisecond is still 125,000 instructions, now of the whole machine, and a hart that halts gives its turns to the others. Measured at the pinned seed 3 in the checked, traced build, p99 in µs, net / gross:

Every target is met at two harts on both widths, and over a 16-seed sweep there too: the worst net p99s over the sweep’s N = 1, 4 and 16 are, rv64 then rv32, 11.5 and 13.0 ms for the driver wake, 18.2 and 26.5 ms for the steward timer wake, 6.8 and 13.7 ms for its decision wake and 5.4 and 12.0 ms for the deadline notice, and a lease’s end at most 9.8 and 16.6 ms; the worst p50 is 7.2 ms (rv32’s timer wake at N = 16). At four, every p99 is met, and one p50 is not: rv32’s driver wake at N = 16, 17.2 ms against 15 ms; rv64’s is 12.6 ms. At four harts a wake can wait for the kernel lock behind three sections (residual risks). sched-lock-contention holds the lock’s order under R12’s costliest call at two and four harts, and gates the driver’s wake there, both targets at two harts and the p50 at four (R78).

A slice end adds its own kernel time (charging). In the release build that is about 7,050 instructions on rv64 and 10,600 on rv32 when it switches budgets (4,200 and 6,700 when the same thread runs on), so a 1 ms slice takes about 1.06 ms and 1.09 ms on the hart with two runnable budgets, each further queued budget adding under 3 µs. The checked, traced build takes longer, its slice end growing by 2.4 µs per queued budget net of its audits: the median gap between slice ends, the marks’ audit included, is about 1.22 ms under three, 1.30 ms under nine and 1.39 ms under seventeen (rv64). A round of N budgets’ slices is N such periods, not N ms.

The decision wake is measured by the stand-in itself (time_now against its own deadline), and the post-check reads its sample windows, net of audits, while R10’s time comes from the kernel’s trace: that half of the lease-end sum is the program’s own report, not the kernel’s.

With the real steward. steward-latency measures the same quantities from the steward itself: alice’s session holds N live leases, the probe’s own lease or the kernel’s deadline lease among them beside N - 1 spinning agents (Redoubt.Agents.Echo spin, each a beamlet VM of 5,248 pages on a lease), N = 1, 2, 3, 4 and 16, D = 16 of each kind per round and 8 at N = 16; a round’s deadline leases run one at a time beside the spinners, each a sample of its own lease grouped at N, the deadline lease twice that round’s worst launch over both widths at one and two harts, rounded up to a second, so the deadline falls on a running VM and never inside the launch (a deadline runs from the time the steward sets as the launch’s batch starts, and a lease shorter than its launch dies before its VM runs, budgets): N = 1 8 s, N = 2 10 s, N = 3 11 s, N = 4 and N = 16 14 s (2 × 3.84 / 4.47 / 5.09 / 6.62 / 6.64 s; N = 2 rounds to 10 not 9 because the probe tells its own lease by 9 s, so no measured lease may be 9 s). Each deadline lease is followed by a sleep of the lease plus a second — the margin over the kernel’s R10 destruction (≤ 30 ms) that frees alice’s pages — both the guest’s clock under icount, so the next lease is requested only after the previous is gone, which also holds the N = 16 carve, where alice’s share leaves room for one measured lease beside the fifteen spinners. One at a time, not a burst: deadline_notice is a single lease’s notice latency (the sponsor told — the steward’s lease_ended send to its session returned — less the deadline; target 40 ms; the send adds 10 to 14 ms to the dequeue it was once sampled at, measured as the first notice of each burst below with the shell idle; the table’s deadline notice row is re-measured at the send, 14 to 32 ms where the dequeue read 8 to 16). A burst of D deadlines firing together hands the steward D Exited events at once, and the sponsor is told of the last of them about D times the core’s decision of one exit after the first, every notice of the burst sent before any exit’s bookkeeping: measured by steward-deadline-burst (six leases on one shared deadline, both widths) and steward-deadline-burst-16 (sixteen, rv64), each lease’s notice the send’s return less that lease’s own deadline; the first 0.43 to 0.96 s gross (32 to 149 ms net of the checked build’s audits) after it — the kernel destroying the six or sixteen VM budgets at its one entry at the deadline before any exit notice goes out, each within R10, and the loop then taking the reports together — then each send returning 13 to 77 ms after the previous, the decision of the next exit; the worst of six 0.91 to 1.12 s gross after its deadline (0.13 to 0.16 s net), the worst of sixteen 1.42 to 1.47 s (0.33 to 0.43 s net), one run per column at the seed, every notice’s line printed by the session; the cases assert twice the worst rounded up, 3 s at both sizes, and every line; the exits’ bookkeeping follows the sends, 17 to 297 ms of effects and then 0.17 to 0.78 s of console lines at the loop’s next turn. With the bookkeeping between the sends they returned 40 to 145 ms apart, the loop’s work for one exit (18 ms of its own time in a 41 ms gap on a traced boot, the checked kernel’s audits the rest), the worst of six 1.13 to 1.43 s and of sixteen 1.8 to 2.5 s. The sends themselves once set the pace: beamlet’s serve thread forwarded each to the session’s VM by a send that waited for the VM to take it, a VM busy in Erlang took one per scheduler turn, and the sends returned 40 to 300 ms apart, the last of six 1.5 to 1.8 s and of sixteen 2.1 to 2.8 s after the deadline, one of six or of sixteen lost at the steward’s bound on rv64 at one hart; under that gate the steward’s ordering (its notices ahead of the exits’ bookkeeping, 16 ms of the 1.4 s then, kept now) and the shell’s listener (receiving and queueing, printing in another process) were each built, measured and found to move nothing, and a block trace placed the wait in that forward, which the thread’s queue removes (the steward, beamlet). What the sponsor sees is the shell’s print of each notice, 250 to 370 ms a line through the relay. The deadline inside a launch: these rounds have the steward idle at each deadline, and a launch in flight once held the serve loop inside a synchronous start_agent (2-6 s), so a deadline that fired during one waited behind it. steward-launch-overlap stages that overlap (a lease’s deadline one second inside another lease’s launch, five times a boot, both widths; judged only when the trace shows the deadline inside the launch’s arrival-to-answer window, else a failing verdict): with the launch on the loop the notice came 0.36 to 0.58 s net after the deadline (0.76 to 1.5 s gross, the launch’s remainder: rv64 at one hart, two harts, rv32 at one); with the steward’s launch thread running the launch while the loop serves, the sponsor is told 16 to 36 ms net after it (p99 20 / 36 / 19 ms on the same three boots, target 40 ms met), the loop’s worst wait on the thread’s install lock 33 µs, 5.2 ms and 50 µs (the steward). What still holds the loop inside a lease’s batch is its mints at the shared servers, within SERVER_US (4 s; 1.66 s worst measured): a deadline inside a mint waits for it, a residual on the steward’s page. The case measures the per-notice quantity, one lease at a time. The trace ring (256 MiB, 8,388,608 records) is per boot, and a single boot of all five rounds overran it at two harts, a boot of N = 1 to 4 too (the rounds record about 1.0 / 2.2 / 2.4 / 3.1 / 1.5 M at N = 1 / 2 / 3 / 4 / 16, and on rv32 N = 1 to 3 alone fill 6.0 M at two harts), so the rounds run as three boots judged on their own rings: steward-latency runs N = 1, 2 and 3, steward-latency-n4 the round at N = 4 and steward-latency-n16 the round at N = 16, on rv64 alone (below). The probe ends each boot’s window on the latency-done marker the case writes after its last round, so one build serves a three-round boot and a one-round boot alike. The steward’s test-only probe arms its timer at the last point before the receive that waits on it, prints its wake, its decision wake and its budget_destroy call to return, and the kernel’s deadline notice, as the stand-in prints them; the post-check judges them net of audits with the targets above, unchanged, and R10 from the trace. The load shapes differ: the stand-in’s spinners were plain budgets of weight 100 under users, the steward’s are lease VMs under alice’s share, each a sizes.agent budget; the measured quantities are per lease end, whatever carries the load. The steward runs at the workload’s weight, 1,000 under system, the image’s own, so the targets are measured at the weight the image runs the steward at. A lease’s end is measured to its destruction and the notice to the sponsor: the servers’ records are freed after, off the measured path. N = 4 is measured at one hart since every shared server’s budget became its manifest entry’s (serving), and the round at N = 16 runs since the per-account caps’ lease term is derived from the manifest as the context cap is (the steward): the case’s alice is sized for it by the carve, 213,542 pages, 104 processes and weight 2,200 over two label sets, so her unlabelled share of 106,770 pages, 52 processes and weight 1,100 holds two sessions, the console’s and the SSH session that drives the rounds (2 × 11,393 pages), and sixteen leases of 5,248 pages, 2 processes and weight 50, their own pages beside (2 × 11,393 + 16 × 5,249 = 106,770), and her home’s quota, 18 MiB, sixteen project carves of 1 MiB; the servers’ caps follow (erofsd:system 2 × 5 + 18 connections, the home and /boot 5 + 18, and 21 parked calls at the home: what the share carves at once and a spare, littlefsd). N = 3 was not reached while a cleanup step a busy server did not take was dropped, leaking a State there until the eighth was refused; the step is parked and retried at the server’s next answer now (steward), and the round runs on both widths at one and two harts; the parked after 4 attempts line, which appeared one to four times a run for a lease’s disconnect at erofsd:system under the two spinners while the loop made the attempts, appears in neither width’s run now that the steward’s own thread makes them. Measured at seed 3, one run each, net µs p50/p99 at N = 1 / 2 / 3 / 4 / 16; each lease destroyed is a VM budget of 5,248 pages, and the gross figures beside the deadline notice and the destroy call carry 300-500 ms of the checked build’s audits after such a destruction (subtracted, as every target is net):

Each boot’s trace fit its ring with nothing dropped: 4,841,622 / 2,876,371 / 1,022,850 records of 8,388,608 for the boots at N = 1 to 3 / 4 / 16 on rv64 at one hart, 5,525,840 / 3,711,105 / 1,363,142 at two; 5,005,142 / 2,963,667 on rv32 at one hart, 5,979,365 / 3,932,389 at two. The real steward meets every target on rv64 at one and two harts, N = 1 to 16, and on rv32 at one hart, N = 1 to 4, each column one run at seed 3 with the cleanup steps on the steward’s own thread (steward): the timer wake’s p99 at N = 3 and 4 is 2.6 and 5.2 ms on rv64, 1.2 and 1.5 ms on rv32, and the reply-to-receive p99 in those rounds 11.5 and 11.0 ms, 10.6 and 12.4 ms, with no 100 ms retry in any sample. At N = 16 on rv64 at one hart the timer wake meets its targets, 0.6 ms at p50 and 1.4 at p99 (54.5 and 57.3 ms when the round first ran, from the tree before the thread, where the wake waited behind whole slices of the fifteen spinner VMs: the cleanup steps’ turn, not the spinners’, was the slice it waited for), and at two harts the N = 16 round’s thirty-one launches are all served, with no parked after line in either run: the refusal of a 29th launch at erofsd:system behind eight parked disconnects, seen once at two harts before the thread, does not recur. Before the thread, the loop ran the cleanup steps at its top within its 100 ms send bound, and one sample of sixteen in the N = 3 and 4 rounds (78 and 93 ms on rv64, 69 and 93 on rv32; the next largest under 4 and 24 ms) held one attempt at a disconnect the busy erofsd:system did not take, so the p99 (50 ms) was missed by construction; the same retry showed in those rounds’ reply-to-receive p99 (124 and 65 ms, 135 and 64) and at N = 4 in the decision wake’s (89 and 66 ms, within its 95), where the lease the probe ends waited behind that turn, and at two harts on rv64 as the N = 3 timer wake’s one miss (148 ms, 112 in the reply-to-receive row).

A lease’s launch is a measured call, and its bound follows the measurement. The steward’s served start_agent line gives the launch from the call’s arrival to its answer: the batch that carves the lease, mints its connections and reads its program from the verified system volume, run beside the sponsor’s other leases spinning. The worst of each round’s launches, one run at the seed:

The launch was the one steward call past the client library’s 5 s bound for a short call, and that 5 s was the VM’s own ceiling on a call’s timeout, MAX_CALL_MS, a guess (beamlet): on rv32 the round at N = 4 at one hart and N = 3 at two died on the match of {:error, :timeout}, and the measure then available, the gap between consecutive AgentStarted audit lines less the session’s sleep, overstated the launch under load by the shell VM’s own share and its sleep’s lag (6.8 s against 3.1 s served, beside fifteen on rv64 at one hart). The bound is derived once, over both widths at one and two harts, from every round the runs reached: twice the worst launch served beside the spinners the case runs, 6.64 s on rv32 at two harts, the N = 16 round’s fifteenth spinner launched beside fourteen (a launch between the table’s columns; 5.851 s at one hart beside three, when the 5 s bound ended that round), 2 × 6.64 s = 13.28 s, rounded up to 14 s, the client’s launch_timeout/0 and the VM’s MAX_CALL_MS one number (the steward); the rounds reached with it show launches up to 6.64 s, within it. The launch is compute: beside spinners of its own weight the launching VM’s share of the harts is theirs divided, 3.0 s beside three on rv64 at one hart against 1.7 s alone, and a block trace (block-trace) of the wedge before the bound showed the steward’s every call out returned within 1.43 s, its only long waits receives on its own endpoint, and the read path’s servers (erofsd:system, verity:system, blkd:system) running whenever a reader asked; verityd’s data cache and read-ahead (verityd) cut its blkd reads by two thirds without moving the launch. With the bound the rv32 rounds run: at one hart N = 1 to 4 meet every target, and at two harts N = 1 to 4 complete for the first time, their rows not judged, since that boot ends in the round after them before the reset dumps the trace the oracle judges from (below); they are judged when a run reaches the reset. The one-hart rv32 column’s rows at N = 1 to 4 are this run’s; the launch’s own spread beside three spinners on rv32 at one hart is 2.76 to 5.85 s over the thirteen launches of the round the bound was derived from, with no step of the steward’s differing between them.

Two rv32 rows are findings, not targets met. With the deadline lease derived from the launch every round completes on rv64 at one and two harts and on rv32 at one hart up to N = 4, each boot’s reset dumping a trace the oracle judges whole (dropped 0); before it, the round’s five-second leases, sized as twice a two-hart launch when that launch was 2.5 s, died inside their own launch on rv32 (5.2 s beside fifteen spinners at one hart, 5.7 to 6.3 s at two), at one hart with no deadline-notice sample and at two harts with a Launch the kernel refused NotPermitted, the deadline passed before the process was made. The round at N = 16 still does not complete on rv32 when it was measured: beside fifteen spinners one spinner VM exited 1 before the round’s first deadline notice, after which the samples grouped at N = 15 around the dead VM (the deadline notice’s p99 over the eight that lived about 45 ms, on a round that had lost a VM). The cause was found and closed on the read path: not the drain rate but admission, the file servers’ fid cap of 32 fair-shared with every connection’s root fid in the share, so that at sixteen connections of one account (two sessions’ and fourteen leases’) no VM of the account could load a module, and the spinner launched last died inside its start module’s read (erofsd); the root is a fixed cost outside the share now and the caps are derived from the connections, and sixteen agents of one account launch and load all their modules on both widths at one and two harts and every one exits 0 (bench:lease-code-load, on the host’s clock: under the virtual clock the guest, idle for an instant with no nearer timer, reached the oldest live lease’s deadline, the test bench). steward-latency-n16 still runs on rv64 alone: its rv32 round was not re-measured with the cap, and the column says so until it is. At two harts on rv32 the N = 1 to 3 boot reaches the reset and is judged for the first time, and the N = 2 round misses the timer wake’s p50, 31.8 ms against 15 (its p99 35.2 ms, met), the same within 30 µs over five boots (31,855, 31,835, 31,825, 31,832 and 31,831 µs), every other target of the boot met with dropped 0 and the kernel lock waited for in 249 of 1000 ticks; N = 1 is 5.6 ms and N = 3 4.2 ms, so the miss is the one-spinner round’s: a kernel lock-contention finding at two harts (a wake can wait for the kernel lock there, R78 and residual risks), to be taken up on its own — why the round with one spinner, then a fix or a stated residual. The table carries the rv32 two-hart rows with their numbers, and rv32 is gated at one hart until it lands, rv64 at both. The a device interrupt returned without its claim rejection of the rv32 two-hart trace, one run in two at this seed before, met neither rv32 two-hart boot here. Before the steward’s console lines were queued and written through one kept fid at the loop’s turn (steward), the steward reached its wait with the console round trips of the reply it had just given on its pass (each line an attach, open, write and close at consoled), the timer wake’s p50 missed on every width and hart count (23 to 61 ms), and at two harts the decision wake’s p50 and the deadline notice’s p99 missed too; the reply-to-receive gap was 34-56 ms at one hart and 94-162 at two. Now a call’s records go before its reply, one write each, and the gap (the last row, recorded, no target) is the loop’s own work and the reply’s hand-over to the caller, with no console call in it. The two-hart figures are gated as the stand-in’s are, and the rv32 two-hart row’s miss of the timer wake’s p50 at N = 2, every sample near 40 ms with the one spinner’s VM live before the round at N = 3 ran, is the finding above, judged now. The same finding at one hart on rv32, one cell: the decision wake at N = 1 is a bare 30 ms receive timeout that sleeps 53 to 62 ms with exactly one lease VM running (the round’s own, just launched and spinning) and wakes 1 to 3 ms late beside a second, the steward doing nothing in the window; it measured 24,235 / 28,493 µs with the launch on the steward’s loop, 0.8 ms under the 25 ms p50, and 30,376 / 33,376 with the launch on the steward’s launch thread (the steward), whose report lands the loop’s receive about 10 ms earlier against the VM’s first run; the same tree with the launch put back on the loop measured 23,300 / 31,843, so the thread moved the phase of a pathological wake, not the wake (the 20 ms timer wake at N = 1 is 2.2 to 3 ms late with the thread, 0.8 without, within its 15 ms). The cell is recorded, not judged (record= on the case, the target unmoved; the table above carries both numbers), the one-runnable-VM timeout wake being the scheduler finding above: a sleeper’s timeout that does not end the running VM’s slice, the timer apparently armed for the slice’s end rather than the nearest timeout, visible only when nothing else switches. Landing the phase under by putting process_start back on the loop would be designing to pass an anomalous wake, and is not done. The cases stay out of the whole run, by name, until the two-hart rows pass on both widths. The destructions judged are those before the probe’s LATENCY-END (99 in the N = 1 to 3 boot, 165 over the three); the sixteen after it in each boot (the marker-file exits reaping the leases) are recorded and not judged.

The sweep (2026-09-27, seeds 1 to 16, on rv64 and rv32, TESTBENCH_QEMU_SEED; the gate runs seed 3, this sweep’s worst, and no gate sets the variable). The steward decision wake, p50 / p99 in µs at N = 1, 4 and 16, and a lease’s end (the worst decision-wake p99 plus R10’s p99 from the trace):

The worst case is rv64 at N = 16: decision-wake p50 17,904 µs (every seed within 4 µs of it) and p99 103,984 µs (seed 3); R10’s p99 is 26,379 µs (rv64) and 27,407 µs (rv32) on every seed. The targets were 15 ms (p50) and 50 ms (p99) before the sweep, which rv64 missed on every seed; the sweep sets them at the worst case plus a margin of a tenth, rounded up to 5 ms: p50 17.9 x 1.1 = 19.7, so 20 ms; p99 104 x 1.1 = 114.4, so 115 ms. Every other measure met its fixed target on every seed; their worst p99s were driver wake 33.3 ms, steward timer wake 34.2 ms and deadline notice 23.7 ms (all rv32), and the server’s share never fell below 380 of 1000.

The second sweep (2026-09-29, the same seeds and widths) followed a change that found process objects by index instead of scanning frames. The change made most destructions cheaper, which moved the workload’s timeline: the last lease destructions at N = 16 now overlap the live sessions. There, taking a lease’s exit notice inside R10 frees its process object, and that object’s handle sweep walks every live process’s handle pages. The N = 16 deadline notice and R10’s kernel time, p99 in µs, and a lease’s end:

The worst are the deadline notice at 48,851 µs (rv32, seed 15) and R10 at 35,421 µs (rv32, seed 6). Their targets became the worst case plus a tenth, rounded up to 1 ms: 48.9 x 1.1 = 53.7, so 54 ms, and 35.4 x 1.1 = 39.0, so 39 ms. The lease end’s bound moved with R10’s, to 154 ms; its worst is 105.8 ms. The difference from 30 ms was the handle-sweep term of budget destruction’s cost. A destruction now follows the dying subtree and folds that sweep into one pass, so the term is gone and the targets are back at 30 and 40 ms above (budgets). Every other measure met its target on every seed. The gate stays on seed 3.

The third sweep (2026-09-29, the same seeds and widths) followed a change that frees a page table once it maps nothing. It found the first sweep’s rv64 median was one phase, not a property of rv64: the N = 16 decision wake’s p50 is about 7 ms on most seeds and about 18 ms on some, on either width (rv64 on seeds 6, 7, 11, 12 and 16, rv32 on seeds 5 and 9). The decision wake, p50 / p99 in µs, and a lease’s end:

The worst are p50 18,529 µs (rv32, seed 9) and p99 82,463 µs (rv64, seed 13). By the same rule, a tenth over the worst rounded up to 5 ms: p50 18.5 x 1.1 = 20.4, so 25 ms; p99 82.5 x 1.1 = 90.7, so 95 ms. The lease end’s bound follows, to 95 + 39 = 134 ms; its worst is 116.6 ms. Every other measure met its target on every seed. The gate stays on seed 3, which is no longer the worst seed; the targets come from the sweep, not from the seed the gate runs.

The fourth sweep (2026-09-30, the same seeds and widths) followed a destruction that walks what it destroys instead of every object frame (budgets), which cheapens R10 and moves the phase of every later event. R10 and the deadline notice return to the 30 ms and 40 ms they had before the second sweep. The decision wake’s worst p50 is 18,541 µs (rv32, seed 11) and its worst p99 82,497 µs (rv64, seed 6); a tenth over the worst rounded up to 5 ms sets the p50 at 25 ms and the p99 at 95 ms. A lease’s end follows to 95 + 30 = 125 ms. Every other measure met its target on every seed; the gate stays on seed 3. The decision wake, p50 / p99 in µs at N = 1, 4 and 16, and a lease’s end (the worst decision-wake p99 plus R10’s p99 from the trace):

The fifth sweep (2026-09-30, the same seeds and widths) followed a destruction that closes only the handles chained to what it destroys and frees the dying tables whole (budgets). R10’s p99 is 5,462 µs on rv64 and 5,723 µs on rv32 at most, on every seed, and the deadline notice’s worst p99 is 27,089 µs (rv64, seed 7). The decision wake’s worst p50 is 7,606 µs (rv32, seed 5) and its worst p99 50,993 µs (rv64, seed 15); a lease’s worst end is 56,454 µs. The targets stay where the fourth sweep set them. The steward now sets each by-deadline lease’s deadline 300 ms ahead, not 150: a budget’s deadline is fixed at its creation, before the spawn, and at N = 16 the spawn takes about 150 ms, so on one seed every lease ended before its process started and the notice took no sample. The lead is the fixture’s; the notice is measured from the deadline, and its target stays 40 ms. The decision wake, p50 / p99 in µs at N = 1, 4 and 16, and a lease’s end:

The worst are p50 18,541 µs (rv32, seed 11) and p99 82,497 µs (rv64, seed 6); R10’s p99 is 22,812 µs (rv64, seed 6) and the deadline notice’s is 37,450 µs (rv32, seed 15), both inside 30 and 40 ms. The lease end’s worst is 104,318 µs, inside 125 ms.

The sixth sweep (2026-10-05, seeds 1 to 20, on rv64 and rv32) followed the 1 ms slice. Every seed passes on both widths. The N = 16 decision wake, p50 / p99 in µs, and a lease’s end (the worst decision-wake p99 plus R10’s p99); at N = 1 and N = 4 the decision wake stays under 1 ms and under 3 ms on every seed:

The worst are p50 11,688 µs (rv32, seed 11) and p99 18,591 µs (rv32, seed 16). R10’s p99 is at most 4,223 µs (rv32), the deadline notice’s at most 12,738 µs (rv32, seed 18), the driver wake’s 23,924 µs (rv64, seed 2) and the timer wake’s 26,937 µs (rv32, seed 12). The lease end’s worst is 22,812 µs. The targets stay where the fourth sweep set them; every measure is well inside them.

The cluster workload (tests/programs/src/bin/sched-cluster.rs) measures the same driver and timer wakes where retained stride debt bites: sixteen weight-100 spinners released by one common timeout, a busy weight-1000 server, and 200 attempts each from the two weight-1000 stand-ins, at fixed 80 ms slots and programmed offsets of 100, 300, 600 and 850 µs. Its whole window is on the kernel clock (time_now, µs): one reading T gives start H = T + 200 ms, release R = H + 50 ms and end F = R + 16 s, sent to every child and printed from the same values. H only anchors R: nothing waits for it, so the server counts from its go to F and the spinners from R to F, each span as printed. The spinners, the server and a stand-in’s spin to a slot run in fixed chunks and read time_now between them; that work is billed alike in a candidate and its control. Each attempt reads B before arming, fixes L = B + delay before it arms, and reads P after the wake (the driver also reads E and the RTC’s service time s between them); its envelope is [L, U) with U = P + 1, which holds all of P’s floored microsecond. The clocks run at one rate and a timeout never ends before its deadline (time, timeouts), so the physical span from the deadline to the service lies inside the envelope, and the envelope’s length, net of the audit time the trace certifies inside it (checked builds), is an upper bound on the wake’s non-audit latency. The bench requires R <= L <= P and U <= F for every attempt, and judges the same p50 <= 15 ms and p99 <= 50 ms on all 200 envelopes of each stand-in. Before that, the trace must show at least 25 wakes per stand-in in each category, five at each offset: zero lead, a zero-intent attempt whose wake’s pass is at the floor the oracle replays, and positive lead, a positive-intent attempt whose wake’s pass is above it. A wake that is neither joins no category but still counts in the percentiles, and how many spinners ranked before each wake is reported beside the categories. A met target proves the bound; a missed one alone does not prove the latency is over it. So the known-bad control (the 10 ms slice) must miss an envelope target and have a driver lower witness, the RTC’s service lateness less the union of every audit’s outer bin [u, v + 1) inside the envelope, above the matching target, on each width. A control that misses only on the envelope demonstrates nothing, and so does one whose positive-lead wakes are not behind the cluster: it needs at least 25 per stand-in with eight or more spinners ranked before them, which under a 1 ms slice a weight-1000 waker never has, since it is picked within one of its own slices of the lowest spinner. A control can also fail to take its samples: a stand-in that comes back after a zero-intent attempt’s target has passed cannot arm it, and the construction stops there. That counts as the demonstrated miss only when the oracle classifies it from the console and the trace: the attempt is zero-intent and not the first, the stand-in’s earlier attempts joined the trace as blocked waits, and B less the target, less the certified audit time between them, is over the p99 target. Any other construction failure, a smaller miss, or a run without its trace is no control. The control is sched-cluster-old-control: the same program and gates with the oracle’s cluster_old_control, run by name only, on the kernel built with its test-only slice-10ms, which keeps the old 10 ms slice. It expects the trace rather than the program’s pass, so a failure the guest reports still reaches the oracle. The RTC lateness is reported beside each envelope, not as its length.

Measured at seed 3 in the checked, traced build, envelope net p50 / p99 in µs, the targets 15,000 / 50,000:

The certified audit credit inside the envelopes was 288 ms and 320 ms on rv64, 384 ms and 376 ms on rv32; the driver’s lower witness p99 was 10,902 and 17,195 µs. At most ten spinners ranked before a positive-lead wake. The control fails as required on both widths, by the classified miss: on rv64 both stand-ins could not take attempt 1, B exceeding its target by 104,188 and 109,853 µs (102,676 and 106,472 µs net of audits); on rv32 the timer could not take attempt 1, by 71,624 µs (69,515 net), and the driver missed attempt 2 by a net 29,843 µs, under the target.

The case fails on any missed. bench:sched-latency-tcg runs the same workload in host time and only reports, with the oracle still checking every pick.

On hardware (the softcores) the same workload is measured in cycles, from rdcycle or mtime at the stated clock rate. That is a characterisation of the board, not a gate.

Authority

Status: built · tested: bench:sched-carve-inflation, bench:legacy-gone, host:redoubt-model::scheduler_contracts_hold

• Weight is the only lever. No call sets a pass, a rank, a priority or a slice, and there is no yield: a thread gives up the CPU by blocking, for instance in a receive with a timeout.
• Weight is carved. A budget’s weight comes out of its parent’s free weight at budget_create, by whoever holds a handle to the parent (R7), and goes back when the child is destroyed. A budget’s free weight rises only when a child it carved is destroyed.
• Ties are the kernel’s. The budget ids that break ties are assigned by the kernel and never reused; no caller chooses one.
• kmain’s switch is not a call. Its tag lies outside the call table; a user-mode ecall with it gets InvalidArgument like any unknown number (ABI).
• Passes are not readable. No call returns another budget’s pass or rank. The scheduling trace would, which is why the production kernel has none (R23).

Security properties

R12 (scheduling)