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.