diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 05dc535..8989bba 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -12,6 +12,51 @@ recorded is indistinguishable from law that was never agreed. ### Added +- `docs/rfcs/0005-address-spaces-and-physical-memory.md` — **proposed**, the memory half of Phase 1 and + the first of three interlocking kernel RFCs drafted together with RFC-0006 and RFC-0007. Physical + memory comes from firmware tables into one bounded `MemoryMap` (the image moves to 0x4020_0000 because + QEMU places no DTB for an ELF at the base of RAM), and a colour-capable bitmap hands out frames. O-7's + "who pays" is answered with typed fixed-capacity slot arrays reused by generation and a + capability-named `Pool` charged for every post-boot frame and slot, `map`'s tables included. The Pool + is declared the single accounting domain for counted units, with CPU time left to RFC-0006's `Core`: a + stated split from research/0002. `Region` and `AddressSpace` join RFC-0003's objects, and `EXECUTE` + joins its rights as bit 5 by a proposed dated amendment. W^X (O-13) holds in four layers, including per + Region across every address space, backed by `SCTLR_EL1.WXN`, whose full value the RFC states. O-5 + becomes a structural rule: the kernel never dereferences a user virtual address. The SMP shootdown and + ASID-rollover protocol is designed now rather than bolted on later. Donation (`reissue`) is + deliberately not proposed but handed to RFC-0003a as input, because gating it on `REVOKE` would + pre-empt that RFC's (a)/(b) choice. Twenty increments, fourteen marked for the Phase-1 demo, each with + the interims it carries named and costed. +- `docs/rfcs/0006-threads-and-scheduling.md` — **proposed**, revised the same day against a three-lens + review (constitution, technical correctness and implementability). Threads, scheduling contexts and + interrupts for Phase 1. The spine is unchanged. The kernel is event-driven, with one stack per core and + preemption points, and time is a capability: a `SchedContext` configured only through a per-core + `SchedControl` (seL4 MCS). Priorities are 256 fixed levels behind a priority ceiling that any + capability to a thread confers. The timer is tickless on both Tier-1 targets. FP/SIMD is enabled per + thread and saved lazily. A device line reaches its driver as a notification and stays masked until + `ack`. The review turned several quiet choices into verdicts. Endpoint queues are now priority-ordered, + because the FIFO citation was wrong. Budgets are declared caps, not minima, departing from + research/0002 on purpose. Userspace timers are named: deadline objects on the release queue. A caller's + death can no longer take time away from a server mid-request. The departures from accepted papers are + now listed as amendments A1–A4: donation only to passive receivers, a short caller waits instead of + being refused, seL4's timeout faults corrected, and the big lock rejecting RFC-0003 §14.2's premise. + The review also fixed the state machine (a tenth state, `Unfunded`), the FP ownership races, the SCTLR + bits RFC-0005 had inverted, and the parked-core start-up (checked against QEMU). The increments now + interlock with RFC-0005 and RFC-0007. The demo's interims are named with their numbers. +- `docs/rfcs/0007-system-calls-and-process-bootstrap.md` — **proposed**, the third of the Phase-1 kernel + RFCs drafted alongside RFC-0005 and RFC-0006, and the one that makes RFC-0003 §9 live. Every + kernel-object operation is a `call` on its capability (seL4's uniform invocation), with twelve syscalls + in all. A method's extra handle words ride in message registers, *presented* rather than moved, so + `map` never costs the mapper its Region. The IPC register budget RFC-0004 §9.4 left open is settled at + four physical and 64 virtual registers, with an optional 1 KiB buffer fetched once at rendezvous. The + handle word is fixed at a 20-bit index and a 44-bit slot generation. A Process object is born with an + empty table and filled only by explicit `GRANT` before its first thread runs, which discharges O-27 and + states honestly what that window does not close: a spawner that keeps the child's AddressSpace keeps + control. There is one root task with every boot capability listed in BootInfo, and no kernel branch on + "is root". The kernel never parses ELF. The console is a capability that never waits. The `user/abi` + binding gets a third designated `unsafe` tree, limited to trap instructions and entry stubs. It + proposes dated amendments to RFC-0003 (the handle word) and RFC-0004 (reusable reply objects), and + names every demo interim with its cost. - `docs/research/0002-virtualisation-and-containment-prior-art.md` — the second prior-art review, on the maintainer's initiative: what the virtualisation and containerisation fields learned under production fire, mined for Setonix. Six research sweeps (hypervisors/microVMs, container diff --git a/docs/rfcs/0005-address-spaces-and-physical-memory.md b/docs/rfcs/0005-address-spaces-and-physical-memory.md new file mode 100644 index 0000000..2a9c1e0 --- /dev/null +++ b/docs/rfcs/0005-address-spaces-and-physical-memory.md @@ -0,0 +1,461 @@ + + +# RFC-0005 — Address spaces and physical memory + +| Field | Value | +|-------|-------| +| Status | **Proposed** — 2026-09-27, awaiting the maintainer's verdict | +| Author | Drafted by Claude Code as sparring partner; verdict the maintainer's | +| Date | 2026-09-27 | +| Affects | Constitution §3 (kernel doctrine) and §11.1's "minimal assembly" (§17.7); RFC-0003 (a dated amendment adding one right; three new objects; `capability/src/rights.rs` and `object.rs`'s doc comment); RFC-0004 §9.1; the boot stub, `aarch64.ld` and the exception reporter; `kernel/src/mm/**`; a new host-tested `memory/` crate; threat model §10 and O-7's text (proposals via `docs/CHANGELOG.md`) | +| Depends on | RFC-0003 (capability table), RFC-0004 (IPC); interlocks with RFC-0006 (threads and scheduling) and RFC-0007 (system calls and process bootstrap), proposed the same day | +| Discharges | O-7 for kernel allocation (reclaim across a transfer stays open), O-8, O-13 (the mapping half); O-5 for every path by which the kernel touches user memory; O-3's destruction case extended to memory; answers RFC-0003 §14.3 and RFC-0004 §9.1 (share) | + +> **Proposed verdicts.** **[demo]** marks what the demo stands on; the rest is forward design. +> +> 1. **[demo] Discovery:** firmware tables into one bounded `MemoryMap`; the image moves to 0x4020_0000, where QEMU leaves room for the DTB (§4). +> 2. **[demo] Frames:** a colour-capable bitmap; fresh frames and table frames zeroed, boot data handed over read-only (§4, §7). +> 3. **[demo] Who pays (O-7):** typed slot arrays reused by generation; every post-boot unit charged to a Pool named by capability, `map`'s too (§5). +> 4. **[demo] One accounting domain:** the Pool, for every counted unit; time stays with RFC-0006's `Core`, a stated split from research/0002 (§5). +> 5. **[demo] Layout:** the same higher-half layout on both; the image read-only in the physmap; per-core stacks guarded, kept by the kernel (§6). +> 6. **[demo] Objects:** `Region` (eager and zeroed, or boot-minted read-only) and `AddressSpace` join RFC-0003's objects beside `Pool` (§7). +> 7. **[demo] Operations:** `map` / `unmap` / `protect` are capability-checked, bounded and atomic; the kernel never picks an address (§8). +> 8. **[demo] Rights:** `EXECUTE` joins RFC-0003's set as bit 5 — on Regions and Pools only, refused at mint elsewhere — by dated amendment (§8). +> 9. **[demo] W^X (O-13):** unrepresentable, enforced per Region across all address spaces, backed by `SCTLR_EL1.WXN` (§9). +> 10. **Sharing (RFC-0004 §9.1):** *share* is derive-and-transfer; destruction walks mappings; *donation* goes to RFC-0003a as input (§10). +> 11. **[demo] User memory (O-5):** the kernel never dereferences a user virtual address; a carried one is a number, validated as one (§11). +> 12. **TLB:** kernel-private, recycled tags; this RFC owns SMP shootdown and rollover, RFC-0006 provides the IPI; single-core half [demo] (§12). +> 13. **[demo] Early boot:** the stub enables the MMU with a stated `SCTLR_EL1`; Rust runs only high and installs the final W^X map (§13). + +## 1. The question + +**Where does memory come from, who pays for it, and how does a process reach exactly the memory it holds +capabilities for — never writable and executable at once, and without the kernel trusting an address a +process gave it?** Mechanism only: how much memory, which program may execute code, and where a heap goes +are userspace's. + +## 2. Which pillar + +**Pillar 2 and the doctrine that capabilities are the only authority, where authority becomes hardware.** A +`READ` capability that becomes a writable page is O-2 violated by the silicon. Pillar 1 lands here too: the +threat model files integrity *in memory* under A1, and W^X is how signed code stays what was signed. + +## 3. What the hardware gives — one shape, two encodings + +Both Tier-1 MMUs, as configured here, are one machine: **four levels of 512 eight-byte entries, 4 KiB pages, +and 47-bit user and kernel halves whose top level uses 256 entries each** — AArch64's 4 KiB granule with +`TCR_EL1.T0SZ = T1SZ = 17`, x86_64's four-level paging without LA57. The leaves differ: + +| Property | AArch64 (VMSAv8-64, 4 KiB granule) | x86_64 (IA-32e, 4-level) | +|---|---|---| +| User / kernel split | two roots: `TTBR0_EL1` (low), `TTBR1_EL1` (high) | one root, `CR3`; PML4 entries 0–255 user, 256–511 kernel | +| Writable | `AP[2]` (bit 7) clear | bit 1 (R/W) set | +| User-accessible | `AP[1]` (bit 6) set | bit 2 (U/S) set | +| No-execute | `PXN` (bit 53) and `UXN` (bit 54), separately | `XD` (bit 63), only with `IA32_EFER.NXE` | +| Global | `nG` (bit 11) clear | `G` (bit 8) set, with `CR4.PGE` | +| Accessed | `AF` (bit 10), set by software on this CPU | bit 5 (A), set by hardware | +| Address-space tag | 16-bit ASID in `TTBR0_EL1[63:48]` | 12-bit PCID in `CR3[11:0]` | + +*(Checked against Linux's `arch/arm64/include/asm/pgtable-hwdef.h` — Arm's site was unreachable — and SDM +Vol. 3A §4.5. QEMU's `cortex-a72` has 44-bit physical addresses, 16-bit ASIDs, no hardware access flag and +no PAN: `target/arm/tcg/cpu64.c`, `ID_AA64MMFR0_EL1 = 0x1124`, `MMFR1` 0.)* Hence **one table engine**, +generic over a `Descriptor` encoder and a frame-access trait, host-tested in `memory/`; only turning a frame +number into `&mut [u64; 512]` through a kernel window (§6, §13) is `unsafe`, in `kernel/src/mm/`. + +## 4. Physical memory: discovery and the frame allocator + +**Discovery.** QEMU fixes RAM at 0x4000_0000 on `virt`; every other address "may vary" and comes from the +DTB, "at the start of RAM" with no register naming it (`docs/system/arm/virt.rst`) — and `hw/arm/boot.c` +puts it only *below* the image (`dtb_limit`). Checked on QEMU 8.2.2 on 2026-09-27: an ELF at 0x4000_0000 +finds **no DTB in RAM**; at 0x4020_0000 it finds one at 0x4000_0000. **So the image loads at 0x4020_0000**, +capping the DTB at 2 MiB; increment 1 re-checks QEMU 11.0.3. A minimal FDT reader (Borrow Ledger boot-path +row; Devicetree Specification v0.4) reads the cell sizes, `/memory`, `/memreserve/` and `/reserved-memory`, +bounds-checks every offset and fails closed; threat model §10 gains a proposed assumption, *firmware tables +describe memory truthfully*. x86_64's UEFI stub (no RFC yet) hands over `GetMemoryMap` after +`ExitBootServices`. **Both produce one `MemoryMap`**: same-kind neighbours coalesced, then at most **256** +sorted, disjoint `(PhysRange, Kind)` entries (raw UEFI maps run to 100–200) — `Usable`, `KernelImage`, +`DeviceTree`, `Reserved`, and `Mmio` from Phase 1's hard-coded addresses — failing closed beyond that; image, +boot stack, DTB and boot tables tagged first. Nothing above `arch` names FDT or UEFI. + +**The frame allocator is a bitmap** (16 KiB per 512 MiB, in the first free frames) allocating from a *colour +set* — `pfn mod C`, `C = 1` until time protection *(Ge et al., EuroSys '19, via research/0002 Part 6)* — or +runs of `n` at an alignment; a double free fails closed. A run search is bounded by RAM, not the caller; a +per-alignment cursor if measurement asks. **Fresh frames are zeroed before a process can observe them, and a +table frame before its parent descriptor is written** (a `DSB` between), lest stale entries translate into +another's frames. *Rejected:* a **buddy allocator** *(Linux)*, whose coalescing fights colouring; a **free +list**, which cannot find `n` contiguous frames without a scan. + +## 5. Who pays: the object store and Pools (O-7) + +The kernel has no heap and must never acquire one a process can drain. **A — seL4 Untyped/retype** reclaims +through a derivation tree, deciding RFC-0003a's B1 by the back door (RFC-0003 §7 and its 2026-07-30 +amendment), and makes object layouts ABI: **rejected**. **B — a heap with creation policy** *(Zircon)* limits +*whether*, not *how much*: **rejected**. **C — static per-type tables** *(Hubris)* cannot say *who* filled one +(research/0002 Part 6): **rejected alone**. **D — C with counted attribution: verdict sought** *(the requester +pays, as in seL4; counted quotas, as in Fiasco.OC's factory limits and Genode's quota trading)*. + +**The store is typed slot arrays**, one fixed-capacity array per type in `.bss`; a slot holds the object, a +generation and a count. The kernel's implementation of `ObjectRef` (`capability/src/object.rs`, a trait) is +`(type, index, generation)`; `current_generation()` is a slot read. **Only live references count** — +capabilities at the slot's current generation, Mappings, IPC-buffer bindings; one at any other generation +counts nothing on clone or drop. A destroyed object's slot is therefore **reused at once, generation +advanced**, stale capabilities failing closed — what RFC-0003 §8's generation exists for — and no past holder +pins another's charge. A slot whose generation cannot advance retires, debited once from its payer (objects +keep 64-bit generations, RFC-0007 (proposed) §6). `object.rs`'s "takes a reference count" is qualified to +match in increment 7. **Where it lives:** generic array and Pool in `memory/`; the concrete store, one +`Kernel` value with every type's array (RFC-0004/0006/0007 objects too), behind **one** `static` in +`kernel/src/mm/` whose SAFETY argument is one core entered with interrupts masked (RFC-0006 (proposed) V1), +then the big lock. No other kernel global accretes. + +**A Pool is the accounting layer**: an RFC-0003 object holding balances of frames and of each type's slots. +At boot every free unit becomes the balance of one root Pool (RFC-0007 (proposed) hands it over). Then: + +```text +Σ balance(r) over all Pools == units of r free -- at every instant after boot +every unit of r in use == kept by the kernel (at boot, or retired), or charged to exactly one Pool +``` + +- **Charged:** Region frames; every object slot; table frames and the `Mapping` slot, to the Pool `map` + names (§8). **Kept, never charged:** image, bitmap, arrays, kernel tables, per-core stacks, boot-minted + Regions (§7). Every charge presents a Pool with `WRITE`. +- **Charge first, then take**, so the only later failure, `Fragmented`, refunds before returning. + `PoolExhausted` names the Pool and resource; nothing overcommits *(research/0002 Part 6, "budgets are + minima")*; refund goes to the payer, whose index each object records. +- **Pools subdivide by moving balance.** `pool_split(pool)` makes an empty child recording its funder; + `pool_move(from, into, r, n)`; `pool_merge(from, into)` once `from` has no outstanding charges. **A Pool + whose last capability closes** returns its free balance to its funder and stays as a forwarding slot until + its charges come home — a chain bounded by the Pool slot count; the root's balance goes to the kernel. +- **Rights:** `READ` queries; `WRITE` spends and moves; `EXECUTE` lets minted Regions carry `EXECUTE` (§9). + +**One accounting domain — decided here, as the programme gives this RFC O-7's model.** research/0002 Part 6 +wants one for memory, object quotas and scheduling contexts. **The Pool is it for every counted unit**, +SchedContext slots included. **Time is not a unit**: RFC-0006 (proposed) sells per-core bandwidth through +`Core`, which moving balance cannot conserve, and folding it in would make every Pool holder a CPU seller — a +deliberate split, congruent by attribution. O-7 would add *"kernel memory is charged to a capability-named +Pool; CPU time to a SchedContext funded through a `Core`"*, via `docs/CHANGELOG.md`. + +## 6. The kernel's virtual layout + +Both architectures get the **same layout**, the cheapest way to keep the HAL honest; the image sits in the +top 2 GiB, as `x86_64-unknown-none`'s default kernel code model expects (overridable, but that buys nothing). + +| Range (both architectures) | Contents | Attributes | +|----------------------------|----------|------------| +| `0x0000_0000_0001_0000` – `0x0000_7FFF_FFFF_EFFF` | the current AddressSpace (§7) | per mapping; not-global; never kernel-executable | +| `0xFFFF_8000_0000_0000` – `+64 TiB` | physmap: every discovered RAM frame at `base + pa` | Normal write-back; execute-never; global; RW, but the image's `.text`/`.rodata` read-only | +| `0xFFFF_C000_0000_0000` – `+1 TiB` | MMIO window: kernel-owned devices only (console, interrupt controller) | Device-nGnRE / uncached; RW; execute-never | +| `0xFFFF_FFFF_0000_0000` – `0xFFFF_FFFF_7FFF_FFFF` | per-core kernel and emergency stacks, an unmapped guard page below each | Normal; RW; execute-never; kept by the kernel at boot | +| `0xFFFF_FFFF_8000_0000` – top | image at `+0x20_0000` | `.text` RX, `.rodata` R, `.data`/`.bss` RW execute-never | + +- **Stacks.** RFC-0006 (proposed) V1 chose one kernel stack per core, allocated here at boot; core 0's boot + stack leaves `aarch64.ld`'s unguarded slot in increment 10. A fault's entry pushes onto the overflowed + stack, so **RFC-0006 (proposed) provides the overflow stack** (x86_64 IST; AArch64's EL1-origin vector + moving to the emergency stack, a kernel fault being fatal). Until then an overflow is a recursive abort. +- **The user floor is 64 KiB** *(Linux `mmap_min_addr`)*; **the ceiling leaves the last page below the hole + unmapped**, closing Intel's `SYSRET` hazard (CVE-2012-0217) for RFC-0007 by layout. The physmap is RAM only. +- **The kernel's top-level entries never change after boot.** AArch64 shares `TTBR1_EL1`; x86_64 copies PML4 + entries 256–511 into each address space *(seL4 x86)*, so every kernel-half PML4E ever used is populated at + boot — one filled later would be missing from earlier copies (Linux's vmalloc-sync bugs); lower kernel + tables may change, invalidated on every core (§12). *Rejected:* an identity-mapped kernel, where user + addresses go; no physmap, an invalidation per IPC-buffer touch. + +## 7. The objects: Region, AddressSpace and Mapping + +**Frame ownership is pKVM's state machine** (research/0002 Part 7): every frame has exactly one owner — the +kernel, or one `Region`. **A Region** is a fixed number of pages over at most eight extents of contiguous +frames, with rights `READ`, `WRITE`, `EXECUTE` and RFC-0003's `DUPLICATE`, `TRANSFER`, `REVOKE`. Mappings +and IPC-buffer bindings hold counted references, so closing the last capability does not pull memory from +under a live mapping *(Zircon: a mapping keeps its VMO alive)*. One object, three kinds: + +- **Ordinary** (`region_create`): eager, zeroed, charged; unmet in eight extents it fails `Fragmented`; DMA + memory is one extent at an alignment. Zeroing runs 512 pages per step between RFC-0006 (proposed)'s + preemption points, the half-built Region held on the caller's thread; no capability exists until done. +- **Boot-minted, read-only**, over the DTB and each boot module RFC-0007 (proposed) embeds (every segment + page-aligned): their frames **move** into the Region, never zeroed (public boot data, so O-8 is untouched), + never charged, never `WRITE` — the DTB `READ`, a module `READ | EXECUTE | DUPLICATE | TRANSFER`, so text + maps `RX` in place and W^X holds because no writable use can exist. +- **Device**, minted at boot over `Mmio` the kernel does not keep; never executable, zeroed or charged; + Phase 2. No operation maps a physical address given as a number: the catch-all right in costume. + +What the kernel fills for the root before handover (writable segments, stack, BootInfo) goes into ordinary +Regions, charged to the root Pool, bytes copied in through the physmap, and only then a capability minted. +**An AddressSpace** is a user root table, a tag (§12), the Pool paying for its tables — the only Pool `map` +may charge — and its mappings; `WRITE` permits `map`/`unmap`/`protect`, `READ` a query; binding it to a +process is RFC-0007's. **A Mapping** is a charged kernel record, not a capability: `{as, region, first_page, +vaddr, pages, perms}`, linked into its AddressSpace's list and its Region's, because RFC-0003's 2026-07-30 +amendment makes load-bearing that *a resolved capability is never cached outside the kernel table* — and **a +page-table entry is exactly such a cache**. *Rejected:* **Zircon VMOs and VMARs** (lazy commit, copy-on-write, +pagers, nesting: policy, and faults in kernel paths); **seL4's capability per frame**; **user-built tables** (Xen PV). + +## 8. Map, unmap, protect — and the rights they check + +Every operation takes handles (RFC-0003 §9), encoded as methods by RFC-0007 (proposed); a further handle +(`map`'s Region and Pool) is a **handle word in a message register**, resolved in the caller's table, never +transferred — RFC-0003 §6's move would take the Region from its mapper. + +| Operation | Needs | Refused when | +|-----------|-------|--------------| +| `region_create(pool, pages, max_extents, align, rights)` | pool `WRITE`; pool `EXECUTE` if `rights` has it | `PoolExhausted`; `Fragmented`; zero pages; `align` not a power-of-two page count; `rights` not Region rights | +| `as_create(pool, rights)` | pool `WRITE` | `PoolExhausted` | +| `map(as, region, pool, first_page, vaddr, pages, perms)` | as `WRITE`; region rights ⊇ `perms`; `pool` the AddressSpace's own, `WRITE` | `vaddr` unaligned, below the floor or outside the user half; overlap; beyond the Region; `pages > 512`; `perms ∉ {R, RW, RX}`; W^X (§9); `PoolExhausted` | +| `unmap(as, vaddr)` | as `WRITE` | no mapping based at `vaddr` — the unit is the whole mapping | +| `protect(as, vaddr, perms)` | as `WRITE` | `perms` not a subset of the mapping's current `perms` | + +User numbers are validated *as numbers*; **the kernel never chooses a virtual address** *(seL4's VSpace +discipline)*. **`map` names a Pool because spending is authority** (O-4); requiring the space's *own* Pool +keeps one payer per space, so refunds need no per-table record *(seL4's caller-supplied page tables)*. +*Rejected:* any Pool (a payer record per table); a Pool bound at `as_create` and spent through `WRITE` +(spending never granted). **`map` is atomic**: it charges missing tables and the Mapping slot first, then +zeroes and links tables, writes leaves and ends with `DSB ISHST` before `eret`; at most 512 leaves and six +new tables. `protect` only narrows; widening is `map` again *(seL4)*. 4 KiB pages; blocks later. + +**Verdict sought: `EXECUTE` joins RFC-0003's rights as bit 5**, as §5 there allows "when a subsystem needs +one". Folded into `READ`, every readable Region is potential code; a Region *kind* fails the loader, which +writes code before running it. seL4 leaves execution ungoverned; Fuchsia's `ZX_RIGHT_EXECUTE` is the lineage. +It means *map executable* on a Region, *mint executable Regions* on a Pool, and is **refused at mint on every +other type** (increment 7); `derive` cannot add it. `rights.rs`'s `ALL` is an explicit union despite its +comment; increment 4 fixes both. **On acceptance, RFC-0003 gains a dated amendment adding `EXECUTE` to §5's +table, logged in `docs/CHANGELOG.md`.** RFC-0003 §14.3's handshake: **installed permission is `perms`, +refused unless a subset of the Region's rights.** + +| perms | needs on the Region | AArch64 stage 1 | x86_64 | +|-------|---------------------|-----------------|--------| +| R | `READ` | `AP[2:1] = 0b11`, `UXN = 1`, `PXN = 1` | `P`, `U/S`, `R/W = 0`, `XD = 1` | +| RW | `READ`, `WRITE` | `AP[2:1] = 0b01`, `UXN = 1`, `PXN = 1` | `P`, `U/S`, `R/W = 1`, `XD = 1` | +| RX | `READ`, `EXECUTE` | `AP[2:1] = 0b11`, `UXN = 0`, `PXN = 1` | `P`, `U/S`, `R/W = 0`, `XD = 0` | + +Every user entry also sets `AF = 1`, `nG = 1`, inner-shareable, Normal write-back. Write-only is refused; +execute-only exists on AArch64 but not on x86_64 without protection keys, so neither offers it. + +## 9. W^X (O-13), in four layers + +1. **Unrepresentable.** `MapPerms` is `Read`, `ReadWrite` or `ReadExecute`; both encoders are total functions + from it, so no writable-executable entry can be built. Host-tested exhaustively. +2. **Per Region, across every address space.** A Region counts writable uses (`RW` mappings, IPC-buffer + bindings) and `RX` mappings: `map RX` is refused while any writable use exists, `map RW` and binding while + any `RX` mapping does. `unmap`, `protect` and unbinding decrement **only once their invalidation has + completed on every core** (§12) — until then a stale writable entry may be live somewhere. +3. **Over time.** `EXECUTE` is minted only from a Pool carrying it — the loader holds one, a JIT gets one by + explicit grant *(Fuchsia's `VmexResource`)*. O-13's Phase-3 load-path clause is policy on this. +4. **Hardware backstop.** AArch64 sets `SCTLR_EL1.WXN` (bit 19) once the final tables are in (§13); user + entries set `PXN`; kernel text has no writable alias, the physmap mapping it read-only *(Linux + `mark_linear_text_alias_ro`)*. x86_64 has no `WXN`: `CR0.WP` and `SMEP` where present. + +`map RX` makes AArch64's instruction side coherent: `DC CVAU` via the physmap, `DSB ISH`, `IC IVAU` if PIPT +(`IC IALLUIS` otherwise; Linux's `sync_icache_aliases`), `DSB ISH`, `ISB`; cortex-a72 reports PIPT (`CTR_EL0 = +0x8444c004`); x86_64 is coherent in hardware. **QEMU models no cache, so errors here pass every test.** These +and §12's `TLBI`s and `TTBR` writes are single-instruction `asm!` intrinsics in `kernel/src/arch/**`, as `wfe` +is today — a reading of "minimal assembly" for the maintainer to confirm (§17.7). The physmap still aliases +*user* code writable at EL1; writing through it only to zero, fill and reach IPC buffers is a convention (§16). + +## 10. Sharing and destruction (RFC-0004 §9.1) + +- **Share** is `derive` then transfer over IPC: the borrower receives, say, `READ | WRITE` without + `EXECUTE`, `DUPLICATE` or `REVOKE`, and maps it where it chooses; bulk data travels as RFC-0004 §5's + descriptor. No `share` syscall and no page-table work during IPC — the long-IPC grave stays shut. +- **Destruction** — at the last live reference, or through RFC-0003 §7.1's destruction case (its right is + open, §17.3) — marks the Region *dying*, so no new mapping, binding or copy resolves it; tears down every + mapping and binding in every address space; completes the invalidation (§12); advances the generation and + refunds the payer. Its preemption points fall between whole mappings. +- **Donation is not proposed.** pKVM's *donate* would be `reissue` — bump, re-mint for the caller over the + same frames, move the charge to the recipient's Pool — RFC-0003 §7's option B2 on one object. Gating it on + `REVOKE` would widen that right beyond "capabilities derived from this one", and under the amendment's + option **(a)** a peer-transferred Region carrying `REVOKE` could cut the broker off. It is **input to + RFC-0003a's (a)/(b) choice**; the demo needs none of it. + +**Concurrency.** Under RFC-0006 (proposed) V1 — non-preemptible, one big lock once SMP lands — no kernel +access to a Region's frames (zeroing, table fill, IPC copy) interleaves with its destruction: each runs whole +in one entry and re-resolves the Region; the dying mark covers destruction's gaps. Finer locking takes +**Region before AddressSpace**. A former sharer faults: RFC-0006 (proposed) binds delivery, RFC-0007 (proposed) +defines the message; under its interim the thread stops. + +## 11. How the kernel touches user memory (O-5) + +**The kernel never dereferences a user virtual address** — not through a checked copy or a fixup table, not +at all *(seL4: the IPC buffer is a frame reached through the kernel window)*. **Where a syscall carries one +— a `map` destination, an IPC-buffer location — it is a number, validated as a number and used only to +program tables or registers.** RFC-0007 inherits that sentence exactly. Everything the kernel reads or +writes for a process is named by capability and reached through the physmap: + +- **The IPC buffer** is a 1 KiB-aligned slice of one page of a Region (RFC-0007 (proposed) §5 sets size and + syscall; RFC-0006 (proposed) records it on the Thread). Binding needs `READ | WRITE`, holds a counted + reference, is a writable use for §9, and destruction severs it. +- **No kernel path faults on user memory**: frames are eager and pinned, so the slow path copies frame to + frame, and the in-kernel fault concurrency that sank L4's long IPC cannot arise. +- **Peer-writable memory is never referenced**: one `kernel/src/mm/` module copies with volatile accesses; + anything interpreted is copied once and validated as that snapshot *(virtio's double fetch, research/0002 + Part 5)*. *Rejected:* `copy_from_user` with fixups (Linux). `SMAP` and `PAN` back the rule where present; + **cortex-a72 has no PAN**, so there it stands on structure. + +## 12. TLBs, ASIDs and PCIDs + +- **Tags are kernel-private**: an ASID (16 bits when `ID_AA64MMFR0_EL1.ASIDBits = 0b0010`, else 8) or a PCID + (12 bits, where CPUID reports it); tag 0 reserved. **Destroying an AddressSpace returns its tag** after + `TLBI ASIDE1IS` (x86_64: `INVPCID` single-context), so churn does not force rollover. *Rejected:* seL4's + ASID pools — a tag is not authority. +- **Kernel entries are global, user entries never.** `map` needs no invalidation: neither architecture caches + a faulting entry (the Arm ARM, section uncited as it was unreachable; SDM Vol. 3A §4.10), and a fault whose + entry is valid on re-walk is retried. `unmap`, `protect` and teardown store, `DSB ISHST`, `TLBI VALE1IS`, + `DSB ISH`, `ISB`; x86_64 `INVLPG`. Freeing an intermediate table needs `TLBI VAE1IS` or `ASIDE1IS`, as + `VALE1IS` spares walk caches; `INVLPG`/`INVPCID` flush them (SDM Vol. 3A §4.10.4.1). **O-8's ordering: + invalidate, then free** — no frame returns to a Pool while any core can translate to it. + +**Multi-core: this RFC owns the protocol; RFC-0006 (proposed) provides the IPI**, built with its SMP +increment; the `-smp 1` demo already uses only broadcast `TLBI`s. Each AddressSpace keeps the set of cores +that have run it since its last full flush *(Linux `mm_cpumask`)*. + +- **Shootdown.** AArch64 needs no IPI: the `…IS` forms reach the inner-shareable domain and `DSB ISH` waits + for completion everywhere. x86_64 has no broadcast: the initiator IPIs the cores in the set, each + invalidates and acknowledges, and **no frame is freed nor W^X count lowered before every acknowledgement**. + A core spinning on the big lock polls its flush request, so the holder never waits on a core waiting for it. +- **Rollover.** The generation bumps, every core's *active* tag is reserved into the new one, and every core + gets a pending-flush mark, consumed by a local `TLBI VMALLE1` at its next switch. **A tag is reallocated + only after every core that ran under it has flushed** *(Linux `arch/arm64/mm/context.c`: `active_asids`, + `reserved_asids`, `tlb_flush_pending`)*. +- **x86_64 PCIDs are per core**: each core caches a few AddressSpace→PCID pairs *(Linux keeps six)*; an + invalidation where the space is not current is a per-core stale mark consumed at the next switch to it. + +## 13. Early boot: turning the MMU on + +The image is linked at `0xFFFF_FFFF_8020_0000`, loaded at 0x4020_0000 (`AT()`). QEMU translates the entry to its +physical alias **only if** it lies in an executable segment with `p_vaddr != p_paddr` (`include/hw/elf_ops.h`, +`load_elf`, v8.2.2), which `AT()` gives while `.text.boot` leads that segment. With the MMU off, the stub: + +1. Parks secondaries, installs the stack and zeroes `.bss` at physical addresses, as today. +2. `MAIR_EL1`: index 0 = `0xFF` (Normal write-back, read/write-allocate), index 1 = `0x04` (Device-nGnRE). +3. `TCR_EL1`: `T0SZ = T1SZ = 17`; `TG0 = 0b00`, `TG1 = 0b10` (both 4 KiB); `SH = 0b11`; `IRGN/ORGN = 0b01`; + `IPS` from `PARange`; `AS` from `ASIDBits`; `A1 = 0`; `TBI0 = TBI1 = 0`; `HA = HD = 0`. +4. Four page-aligned boot tables in `.bss`, with `DC IVAC` before and after writing them, so no dirty firmware + line is evicted over them and none shadows them *(Linux `head.S`)*: `TTBR0_EL1` identity-maps 0x4000_0000 + as a 1 GiB Normal block and 0x0000_0000 as a 1 GiB Device block with `UXN` and `PXN`, so the UART + survives; `TTBR1_EL1` maps `0xFFFF_FFFF_8000_0000` to 0x4000_0000 as a 1 GiB Normal block; all `AF = 1`. +5. `TLBI VMALLE1`; `IC IALLU`; `DSB NSH`; `ISB`; both `TTBR`s; `ISB`; `SCTLR_EL1` = **`0x30D4581D`**; `ISB`. +6. Branches to the high alias by absolute address, moves `SP` and `VBAR_EL1` there, calls `rust_entry`. + **Rust never executes at the low alias.** + +| `SCTLR_EL1` field (bit) | Value | Why | +|-------------------------|-------|-----| +| `M` (0), `C` (2), `SA` (3), `SA0` (4), `I` (12) | 1 | MMU and caches on; stack-alignment checks at EL1 and EL0 | +| `A` (1), `CP15BEN` (5), `ITD` (7), `SED` (8), `E0E` (24), `EE` (25) | 0 | alignment is the compiler's (`+strict-align`); AArch32 controls, and no thread runs AArch32; little-endian | +| `UMA` (9), `UCT` (15), `UCI` (26) | 0 | EL0 may neither mask interrupts (defeating preemption) nor maintain caches — the kernel does that at `map RX` (§9) | +| `DZE` (14) | 1 | EL0 `DC ZVA` is a store its mapping already permits | +| `nTWI` (16), `nTWE` (18) | 0, 1 | `wfi` traps and `wfe` does not — RFC-0006 (proposed) §8 | +| `WXN` (19) | 0, then 1 | set by Rust step (5), giving `0x30DC581D` | +| 11, 20, 22, 23, 28, 29 | 1 | RES1 on Armv8.0: Linux v4.19's `SCTLR_EL1_RES1`, plus bit 23 (`SPAN`, RES1 before Armv8.1), which Linux always sets; not re-checked against the Arm ARM | + +Every other bit is 0 (RES0 on Armv8.0, or a later extension left off). Rust then, never leaving the reporter +without a console: (1) builds the `MemoryMap`, bitmap and arrays through the **boot window** — the +frame-access trait's offset is `pa − 0x4000_0000 + 0xFFFF_FFFF_8000_0000`, so all it touches lies in the boot +GiB; (2) builds §6's final tables; (3) swaps `TTBR1_EL1` from the identity map in assembly — empty table, +`TLBI VMALLE1`, final table, as break-before-make requires *(Linux `idmap_cpu_replace_ttbr1`)* — and moves +the trait and bitmap to the physmap offset; (4) **repoints every kernel MMIO user** (UART; GIC if up); +(5) sets `TCR_EL1.EPD0 = 1` (the first AddressSpace install clears it) and `WXN`, then `TLBI VMALLE1`, `DSB +ISH`, `ISB`. **The boot tables are never freed**: freeing `.bss` would give image frames a second owner. + +The reporter gains a DFSC and fault-level decode (it prints `FAR` already); x86_64's `#PF` prints `CR2` and +its error code. **x86_64**, once the UEFI stub exists, is already paging: Rust builds §6's PML4 with a +temporary identity entry for a trampoline page and sets `IA32_EFER.NXE` (bit 11), `CR0.WP` (bit 16), +`CR4.PGE` (bit 7) and `CR4.PCIDE`/`SMEP`/`SMAP` (bits 17, 20, 21) where CPUID permits; assembly loads `CR3`, +jumps high and drops the identity entry — the same "Rust runs only high" rule. *Rejected:* a separate loader +*(seL4's elfloader)*; Rust building tables with the MMU off, sound only without absolute addresses. + +## 14. Obligations + +| Obligation | This RFC | Status after implementation | +|-----------|----------|-----------------------------| +| O-3 revocability | destruction walks the Region's mappings, invalidates, then bumps; a page-table entry is a cached resolution (§7, §10) | **destruction case extended to memory**; selective revocation and donation are RFC-0003a's | +| O-5 argument validation | no user virtual address dereferenced; carried ones are numbers; memory by capability through the physmap; snapshots (§11) | **discharged for the memory surface**; RFC-0007 inherits §11's sentence | +| O-6 kernel memory safety | new `unsafe` only in `mm/**` (window access, volatile copy, the store's static) and `arch/**` (tables, TLB, boot) | **stays Built** — every new block listed per PR | +| O-7 no unprivileged exhaustion | arrays reused by generation; every post-boot unit charged to a Pool named by capability, `map`'s too; charge-first; `map` ≤ 512 leaves; zeroing in 512-page steps; run search bounded by RAM (§4, §5, §8) | **discharged for kernel allocation**; a transferred object stays charged to its payer until destroyed — **open** with RFC-0003a (§17.2); CPU time is RFC-0006's | +| O-8 address-space disjointness | per-process tables; Regions only by capability; frames and tables zeroed before use; invalidate before free (§4, §7, §12) | **discharged** | +| O-9 no ambient side channel | no shared mapping a capability did not establish (§10) | **contributes** | +| O-13 W^X | four layers, per Region across all spaces, counts falling only on completed invalidation (§9) | **discharged at mapping**; the load-path clause is Phase-3 policy over layer 3 | +| O-2, O-4 | `perms` ⊆ rights; `protect` narrows; spending needs a Pool capability; no physical-address map | **maintained** | +| O-18 confined DMA | single-extent Regions; Device Regions minted at boot | **groundwork only** — Phase 2 | + +## 15. Graves checked (§3) + +- **Policy in the kernel.** No address choice, demand paging, copy-on-write, overcommit or OOM response. +- **Baroque capability hierarchies.** No Untyped tree; Pools are flat, with one funder index for closure. +- **Multi-copy IPC.** The slow path copies once, frame to frame; bulk data is shared, never copied (§10). +- **Bolted-on multicore.** Broadcast `TLBI` from the first line; shootdown, rollover, per-core tags designed now (§12). +- **The catch-all right.** `EXECUTE` is narrow and refused off-type; no "map any physical address" right. +- **Compiled-in unused device paths (VENOM).** The kernel maps only the devices it drives itself. + +## 16. Costs — what this makes harder + +- **Capacities are ceilings** (a rebuild); **Regions are eager and bounded** (no lazy or sparse ones). +- **`map` needs the AddressSpace's own Pool**: a loader mapping into a child holds the child's Pool. +- **47-bit halves on AArch64** give up half of what `T0SZ = 16` allows; **the 64 KiB floor is fixed**. +- **User addresses are numbers only** (§11): every RFC-0007 syscall pays in ergonomics, for a bug class gone. +- **The physmap is a large target** (§9) — a software invariant, as are W^X on x86_64 and O-5 without PAN. +- **Every boot runs RWX** from MMU-on to Rust step (5), before any process exists; a stray early write goes + uncaught. **Cache maintenance is untestable under QEMU**; **the load address is a QEMU `virt` fact**. +- **Reclaim across a transfer needs cooperation**: the payer stays charged until destruction (RFC-0003a). + +## 17. Open questions + +1. **Page-table frames on unmap.** Freed only with the AddressSpace; eager freeing needs §12's walk-cache rule. +2. **Donation and reclaim across a transfer** — `reissue` with a charge move, offered to RFC-0003a (§10). +3. **Which right authorises explicit destruction** — `REVOKE` would widen as `reissue` would; RFC-0003a. +4. **Hardware backing for software rules:** software PAN on Armv8.0; unmapping executable user frames from the physmap. +5. **Preemptible teardown**: the O(mappings) walk made restartable at RFC-0006 (proposed)'s preemption points. +6. **The firmware assumption** (§4) and O-7's new text (§5), via `docs/CHANGELOG.md`. +7. **"Minimal assembly"** (Constitution §11.1): are runtime one-instruction `TLBI`/`DC`/`IC`/`TTBR` intrinsics within it (§9)? +8. **One programme order** across RFC-0005/0006/0007 — §18 proposes one for the maintainer to fix. + +## 18. Implementation increments + +One reviewable PR each; **[demo]** marks what the demo needs. Pure logic lands in a new `memory/` crate as +`capability/` does (`no_std` in the kernel, `std` under test, both targets in CI, no `unsafe`). Each new `arch` +function gets a documented x86_64 stub — an empty `MemoryMap`, on which memory initialisation prints `mm: no +memory map (UEFI stub pending)` and halts — so the second Tier-1 build compiles the whole path. + +1. **[demo] Relink at 0x4020_0000; prove the DTB.** MMU off. `--expect "DTB 0xd00dfeed at 0x40000000"`. +2. **[demo] Addresses, `MemoryMap`, FDT reader.** Host tests on a `dumpdtb` fixture, hostile blobs and later an + OVMF dump; workspace `members`, `.github/workflows`, `CLAUDE.md` § Layout. `--expect "mm: 512 MiB RAM at 0x40000000"`. +3. **[demo] Frame bitmap.** Churn tests against a shadow model: no frame twice, none reserved, no image frame free. +4. **[demo] `EXECUTE` in `capability/`** with RFC-0003's amendment: bit 5, `ALL`, `Debug`, tests to `0..64`. +5. **[demo] `MapPerms` and both encoders.** Exhaustive: never W+X; every user entry `PXN`, `AF`, not-global. +6. **[demo] Table engine**, both formats: overlap, bounds, unpaid maps nothing, tables zeroed, root untouched by kernel maps. +7. **[demo] Slot store and one Pool.** Conservation; reuse at generation + 1; stale references count nothing; mint refuses off-type `EXECUTE`. +8. **`pool_split`/`move`/`merge` and closure forwarding**, under random churn. Host-only; not demo. +9. **[demo] MMU on (§13, stub)**, `SCTLR_EL1`, `VBAR_EL1` high, DFSC decode: `--expect "mm: running at 0xffffffff80"`. +10. **[demo] Final kernel map (§13, Rust)**, the store behind its static: physmap with the image read-only, + MMIO window with every kernel MMIO user repointed, core 0's stack behind a guard; `EPD0`, `WXN`. One + `--expect` per self-test: `provoke-ro-text` and `provoke-ro-alias` write `.text` through the image and + the physmap (`data abort, same EL`); `provoke-wxn` branches into `.data` (`instruction abort, same EL`). +11. **[demo] Region and Mapping records** with the W^X counts. Host-only. +12. **[demo] The tag allocator**: rollover, per-core reservation, return on destruction. Host-only. +13. **[demo] AddressSpace and boot-minted Regions**; `TTBR0_EL1` with ASID; `EPD0` cleared. `AT S1E0R` under + two ASIDs finds a shared Region at one frame, private ones apart: `mm: shared region agrees`. +14. **[demo] Pool, Region, AddressSpace methods via RFC-0007's `call`** (its increment 6): `[el0] map ok`. +15. **`unmap` and `protect`** with invalidation and count decrements (§9, §12). Not demo. +16. **User-memory module (§11)**: a message beyond the register budget. Not demo. +17. **Destruction (§10)**, after RFC-0007 increment 11's fault message: a destroyed sharer's fault reaches its handler. +18. **Stack overflow**, with RFC-0006's overflow stack: `provoke-stack-overflow` reaches the reporter. +19. **PAN, SMAP, SMEP** where reported, with a `provoke-user-deref` self-test under `-cpu max`. +20. **x86_64** tables, `CR3` and PCID, after the UEFI stub; **Device Regions** in Phase 2. + +**Programme order proposed** (§17.8): 1–8 beside RFC-0006 1–2 and RFC-0007 1–5; RFC-0007's MMU-off EL0 +self-test (its 3) before 9, which retires it; 9–10 before RFC-0006 3 (or 10 repoints the GIC too) and 4, +which needs the stack window; 11–13 before RFC-0006 5 and RFC-0007 6–7; 14 with RFC-0007 6. + +**Interims the demo carries, with their cost:** + +- **One root Pool** (increment 8 is not a syscall yet): server and client charges are indistinguishable. +- **No destruction or `unmap`**: a killed process's frames and slots stay charged; O-3's memory case is + designed, not built. **No IPC-buffer module**: messages beyond the register budget cannot be sent. +- **Hard-coded UART and GIC addresses**, against QEMU's warning. **Until increment 10 the kernel runs RWX.** +- **1 GiB boot blocks** cover 512 MiB with no RAM behind them, which speculation may touch on real hardware: + there, 2 MiB blocks sized from the DTB. **Zeroing in one step** until RFC-0006's preemption points. +- **A guarded-stack overflow is a recursive abort** until increment 18. +- **Not an interim:** the root's image reaches it through boot-minted and kernel-filled Regions and + increment 13's `map`, so §8's rights check runs even at boot. + +## 19. What this unblocks + +Increments 1–14 give RFC-0006 (proposed) address spaces, a guarded per-core stack and a Pool to charge threads +to; RFC-0007 (proposed) the objects its Process, root task and boot info are made of, and §11's sentence on +user addresses as a constraint inherited, not discovered. The root receives all memory as one boot-minted +Pool — RFC-0003 §14.4's bootstrap without an ambient grantor. Increments 1–8 leave the MMU off: all can land now. diff --git a/docs/rfcs/0006-threads-and-scheduling.md b/docs/rfcs/0006-threads-and-scheduling.md new file mode 100644 index 0000000..117b05e --- /dev/null +++ b/docs/rfcs/0006-threads-and-scheduling.md @@ -0,0 +1,480 @@ + + +# RFC-0006 — Threads and scheduling + +| Field | Value | +|-------|-------| +| Status | **Proposed** — 2026-09-27, awaiting the maintainer's verdict | +| Author | Drafted by Claude Code as sparring partner; verdict the maintainer's | +| Date | 2026-09-27 | +| Affects | Constitution §3 ("IPC is the product", priority inheritance, bolted-on multicore); the HAL (`kernel/src/arch/**`), `boot.s`'s park loop and `aarch64.ld`'s stack plan; RFC-0003 §14.2 (a dated note); RFC-0004 §4, §8, §9.2, §9.3 and its 2026-08-01 amendment (§13's amendments); research/0002 Part 6 (one correction); RFC-0005 §13 step 5 and §18.2; `CLAUDE.md` § Architectures (FP enabled per thread) and § Layout (gains `scheduler/`); every userspace driver | +| Depends on | RFC-0003 (capability table); RFC-0004 (IPC) and its 2026-08-01 amendment; RFC-0005 (proposed) for object memory, kernel stacks, discovery and address-space switching; RFC-0007 (proposed) for the trap path, the syscall encoding, the Process object and the root task | +| Discharges | O-7 for CPU time and the scheduler's own structures; O-4 for time; both commitments of RFC-0004's 2026-08-01 amendment **as amended by verdict 12**; answers RFC-0004 §9.2 in shape; contributes to O-5, O-9, O-17 | + +> **Proposed verdicts.** +> +> 1. **Event kernel:** one stack per core; long paths take preemption points; every wait is a state (§3). +> 2. **Thread:** ten states, one of them `Unfunded`; born at priority 0; fault handlers held in the thread (§4). +> 3. **Time is a capability:** a `SchedContext`, configured only through its core's `SchedControl` (§5). +> 4. **Budgets are caps, not minima:** a guaranteed minimum is admission policy, unlike research/0002 (§5). +> 5. **Priorities:** 256 fixed levels; any capability to a thread lends its priority ceiling; no new right (§6). +> 6. **Endpoint queues are priority-ordered,** first come first served within a level, as in seL4 MCS (§6). +> 7. **Donation:** `call` lends time to a *passive* server; a caller's death never takes it back mid-request (§7). +> 8. **Budget guard:** endpoints carry a `min_budget` checked at `call`; expiry fails one hop back (§7). +> 9. **Timer:** tickless per-core deadlines; userspace timers become deadline objects on the same queue (§8). +> 10. **FP/SIMD:** off by default, enabled per thread, saved lazily; the kernel touches it only to save it (§10). +> 11. **Interrupts and cores:** a line signals a notification; one big lock; a core starts when funded (§11–§12). +> 12. **Amendments:** three to RFC-0004, a note on RFC-0003 §14.2, a correction to research/0002 (§13). + +## 1. The question + +**Who runs next, on which core, for how long, and on whose authority — such that no thread runs on time it was +not granted, a server never runs on time nobody paid for, and the kernel never waits on anything a process +controls?** + +That is O-7's scheduler half plus RFC-0004's three hazards: direct switch, donation, and budget expiry inside a +server. This RFC designs the mechanism; priorities, admission and load are for whoever holds its capabilities. + +## 2. Which pillar + +**The kernel doctrine (§3) directly, and pillar 2 by consequence.** "IPC is the product" holds only if a `call` +hands over the CPU and the budget without a scheduler round trip (RFC-0004). Time is the one resource every +thread consumes; if it is not a capability, pillar 2 has a hole exactly where A5 lives — so, as seL4 MCS did, +it becomes one. **Borrow Ledger:** scheduler, timer and interrupt-controller code are the microkernel-core row, +*write ourselves*; Redox is reference only, since the kernel masks and signals but never services a device. + +## 3. The execution model — one kernel stack per core (verdict 1) + +- **Option A — process kernel** (a kernel stack per thread: Linux, Zircon, original L4). **Rejected:** a guarded + stack per thread with no heap, and blocking in the kernel is how "hold a lock across a wait a process + controls" (O-7) becomes possible. +- **Option B — event kernel** (one stack per core: seL4, OKL4, NOVA; Fluke's "interrupt model"). **Verdict + sought.** Entered by exception, interrupt or syscall, the kernel runs to completion with interrupts masked and + leaves by restoring *some* thread's frame. A syscall that must wait records a state; on wake its result is + written into the frame, or it restarts by rewinding the PC (4 bytes for `svc #0`, 2 for `syscall`). *(Heiser & + Elphinstone, TOCS 2016; Ford et al., "Interface and Execution Models in the Fluke Kernel", OSDI 1999.)* + +**The cost:** every path must be bounded. Long ones — destruction, RFC-0005's `reissue` and teardown, RFC-0007's +console write (both proposed) — take **preemption points**: on a pending interrupt (`ISR_EL1.I`; the LAPIC IRR) +they leave the operation restartable and exit. **A restart re-resolves every handle and re-checks every right**; +an object mid-teardown is marked *dying* so no entry invokes it meanwhile. The worst path between points is +measured and published as the interrupt latency. The boot stack becomes core 0's kernel stack in RFC-0005's +guarded window, **reversing `aarch64.ld`'s plan** to replace it "by per-thread stacks". + +**Idle is a kernel loop, not a thread,** billing nobody: `wfi` with `PSTATE.I` set (a pending interrupt still +wakes it), then unmask — DAIF only, since Linux warns that masking at `ICC_PMR_EL1` would *not* wake the core +(`arch/arm64/kernel/idle.c`); x86_64 runs `sti; hlt`, whose STI shadow issues the `hlt` first. **An interrupt in +idle abandons it:** the current-EL IRQ stub (this RFC's; RFC-0007 owns the lower-EL and `syscall` entries) saves +nothing, resets `SP` to the per-core stack top and enters the dispatcher. Idle alone unmasks, and it drops the +big lock (§12) first. + +## 4. The Thread object (verdict 2) + +A **Thread** is an RFC-0003 object belonging to one Process, which RFC-0007 (proposed) provides; its TCB is a +slot in RFC-0005 (proposed)'s typed array for threads, charged to the Pool presented at creation. + +| Field | Meaning | +|-------|---------| +| `frame` | the full user register file, written at every kernel entry (§9) | +| `state`, `blocked_on`, links | a state below; the endpoint, reply object or notification waited on; intrusive queue links | +| `priority`, `mcp` | base priority and maximum controlled priority (§6); both **0 at creation** | +| `home_sc`, `sc`, `effective` | the bound context, if any; the context held now, own or donated; the priority run at now (§7) | +| `bound_notification`, `ipc_buffer` | the notification a `recv` may also wake on (RFC-0004 §10); the IPC-buffer binding (RFC-0007, proposed) | +| `fault_ep`, `timeout_ep` | **two kernel-held capability slots** *(seL4 MCS)*: moved in by the binder, generation-checked when a fault is raised, failing closed if the endpoint died; the thread cannot close them | +| `fp_enabled`, `fp_state` | the FP/SIMD flag and save area (§10) | + +| State | Meaning | Left by | +|-------|---------|---------| +| `Inactive` | created, suspended, or faulted with no handler; in no queue | `resume` | +| `Ready` | runnable with released budget; in its core's run queue | dispatch, `suspend`, context removed | +| `Running` | the current thread on its core; in no queue | preemption, timeslice end, exhaustion (→ `Throttled`), block, `yield`, fault, `suspend`, `thread_exit`, context removed (→ `Unfunded`) | +| `Throttled` | holds a context whose released budget is spent, or below what its pending `call` needs; in the release queue | refill release, `suspend`, context removed | +| `Unfunded` | runnable, no context: a passive thread woken by `send` or `notify`, `resume`d with none, or stranded (§7); in no queue | `bind_sc`, a donation, `suspend` | +| `BlockedOnSend` | queued on an endpoint to `send` or `call` | rendezvous, endpoint destruction, `suspend` | +| `BlockedOnRecv` | waiting on an endpoint (and any bound notification) | rendezvous, signal, `suspend` | +| `BlockedOnReply` | waiting on a reply object after `call` or a fault message | reply, error completion (§7) | +| `BlockedOnNotification` | waiting on a notification alone | signal, `suspend` | +| `Exited` | finished; in no queue; the object lingers until destroyed | never | + +Faults reuse IPC: the kernel `call`s `fault_ep` for the thread, which waits `BlockedOnReply` (RFC-0007 defines +the message); a fault donates as `call` does, a timeout fault never, and both bypass `min_budget`. Destroying +a thread bumps its generation (RFC-0003 §7), unlinks it in O(1) and destroys any reply object it waits on +(RFC-0004 §8); §7 governs a context it lent. +**Every internal link survives slot reuse:** queue links, `sc`, `home_sc`, a reply object's record of a lent +context, an `IrqHandler`'s notification and a core's FP owner are each a counted reference holding the slot +(RFC-0005 §5) or an `(index, generation)` pair checked on use — never a bare index. + +Every operation is a method `call` on the **invoked** capability (RFC-0007 verdict 1). Some also name a +**presented** one — resolved and checked in the caller's table, never moved, needing no `TRANSFER` — an encoding +RFC-0007 (proposed) provides *(seL4's `extraCaps`)*. The list is closed: + +| Operation | Invoked: right | Presented: right | Effect | +|-----------|----------------|------------------|--------| +| `set_priority(t, auth, p)` / `set_mcp(t, auth, m)` | `t`: `WRITE` | `auth`: any capability to a Thread, no right checked | value `≤ mcp(auth)` (§6) | +| `bind_sc(t, sc)` / `unbind_sc(t)` | `t`: `WRITE` | `sc`: `WRITE` / — | active ↔ passive | +| `bind_notification(t, n)` / `unbind_notification(t)` | `t`: `WRITE` | `n`: `READ` / — | a `recv` also wakes on `n` | +| `set_fault_ep(t, ep)` / `set_timeout_ep(t, ep)` | `t`: `WRITE` | `ep`: `WRITE`, **moved** into the TCB | the binder derives first to keep a copy | +| `resume(t)` / `suspend(t)` | `t`: `WRITE` | — | `Inactive` ↔ runnable; a first `resume` closes the grant window (RFC-0007) | +| `read_regs(t)` / `write_regs(t, …)` | `t`: `READ` / `WRITE` | — | the frame, `TPIDR_EL0` and `FS_BASE` only, sanitised (§9) | +| `set_fp(t, on)` | `t`: `WRITE` | — | §10 | +| `sc_configure(ctl, sc, B, T, refills, 0)` | `ctl`: `WRITE` | `sc`: `WRITE` | §5; the last word, the placement class, is reserved zero (§12) | +| `sc_stats(sc)` / `ctl_info(ctl)` | `sc` / `ctl`: `READ` | — | §5's counters; the exclusivity check (§12) | +| `yield()` / `thread_exit()` | none: two of RFC-0003 §9's three authority-free exceptions | — | tail of own level / `Exited` | + +No right joins RFC-0003's set. **The supervision cost:** a process with `WRITE` on its own thread can rebind +its `fault_ep`, so a supervisor grants no `WRITE` on threads it creates for a child; threads the child creates +are supervised through the Process (RFC-0007 open question 1). A TLS runtime sets `FS_BASE` by `write_regs`, +needing `WRITE` on its thread, or its spawner sets it before `resume`. + +## 5. Scheduling contexts and `SchedControl` — time as a capability (verdicts 3, 4) + +**Options.** A timeslice on the thread (classic L4, Zircon) makes creating a thread *acquiring CPU*, with nothing +to grant or withhold — **rejected** on O-4. Partition budgets (QNX adaptive partitioning) are **subsumed**, as +what a `SchedControl` holder builds from contexts. **Verdict sought:** contexts as objects *(seL4 MCS: Lyons, +McLeod, Almatary & Heiser, "Scheduling-context capabilities", EuroSys 2018)*. A **SchedContext** holds budget +`B` and period `T` (`B ≤ T`), at most eight refills, its core and its bound thread; a thread with one is +**active**, one without **passive**, running only on donated time (§7). **The ABI unit is the nanosecond** +(`u64`) for `B`, `T` and `min_budget`, converted to ticks once, in `sc_configure` and at endpoint creation — +budgets round down, periods up — so no per-machine frequency enters the ABI. + +**What a budget means — caps, not minima (verdict 4).** research/0002 Part 6 asks for guaranteed reservations +with capping left to the broker. This kernel enforces the **cap**, because a sporadic cap is what makes +fixed-priority admission sound: a holder can promise a minimum only if every more urgent context is capped. The +**minimum** is admission, the `SchedControl` holder's policy. Dispatch is work-conserving *only among threads +with released budget*: a spent partial context leaves its core idle by design, and no budget carries over. + +| Aspect | Rule | +|--------|------| +| **`SchedControl`** | one per core, minted to the root task and listed in BootInfo (RFC-0007, proposed). Two methods: `sc_configure` (`WRITE`) binds a context to that core with its parameters — moving a context is `sc_configure` through another core's `SchedControl`, and the first one onto a parked core starts it (§12); `ctl_info` (`READ`) returns the count of contexts on the core and the object's reference count. Topology is BootInfo *data* from RFC-0005 (proposed)'s discovery; routing is `IrqControl`'s (§11). No syscall names a core by number. *(seL4 `SchedControl`; research/0002's "core-set capability".)* | +| **`MIN_BUDGET`** | `B` below twice the published worst kernel path is refused — seL4 MCS's rule, `2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE` (`include/kernel/sporadic.h`), without the scale. The path is measured *between preemption points*, which is why RFC-0007's console write must take them (§11): its 44 ms hold would make `MIN_BUDGET` 88 ms. | +| **Full and partial** | full contexts (`B = T`) are never throttled and round-robin with timeslice `T`. Partial ones (`B < T`) are sporadic servers: no window of length `T` sees more than `B` consumed; refills fall due a period after use; when all eight are in use they merge, forfeiting bandwidth rather than exceeding it. *(Sprunt, Sha & Lehoczky 1989.)* | +| **Billing** | the QNX caveat stated as design (ECRTS '21): each context's window is its own sliding period; billing is exact, from `CNTVCT_EL0` or the TSC read at every entry and exit — 16 ns on QEMU's `cortex-a72`, which keeps the pre-Armv8.6 62.5 MHz default (`target/arm/tcg/cpu64.c`, `target/arm/cpu.c`). Kernel time, **interrupts included, is billed to the context running on entry** *(as seL4)* — a leak costed in §17. | +| **Stall counters** | from the first version (research/0002 Part 6, after PSI and oomd): per context, time consumed, time and count throttled, time ready but waiting, expiries; read through `sc_stats` — the O-17 supervisor's wedged-server signal. | +| **Lifecycle** | destroying or reconfiguring a context preempts the thread running on it (an IPI on SMP), clears every link to it — `sc`, `home_sc`, a reply object's record, its release-queue entry — before its slot count can reach zero, and leaves those threads `Unfunded`. A reply whose recorded context has gone moves nothing. | +| **Accounting domain** | **decided: separate in Phase 1.** A context's memory is a slot charged to a Pool (RFC-0005); its time comes only from a `SchedControl`. One domain holding both is the broker RFC's; the cost is a broker reasoning over two ledgers. This answers RFC-0005 (proposed) open question 2. | + +## 6. Priorities and dispatch (verdicts 5, 6) + +**256 levels**, 255 most urgent, meaningful within a core. `set_priority(t, auth, p)` needs `WRITE` on `t`, any +capability to the Thread `auth`, and `p ≤ mcp(auth)`; MCP is set alike, so authority over urgency only narrows +as it is delegated — O-2's shape *(seL4 `TCB_SetPriority`, whose authority is any TCB capability)*. **Threads are +born at priority 0 and MCP 0**, so a fresh thread is no authority; the root's starts at 255 and 255 with a full +context on core 0, the one bootstrap act (RFC-0007 §9). A **rightless** capability to a thread holding the MCP +wanted delegates priority authority alone. **Rejected: `READ` or `WRITE` on `auth`**, which would make priority +authority and register access one token; **a `SCHEDULE` right**, the catch-all right in embryo (the +CAP_SYS_ADMIN grave); **dynamic priorities** (CFS, BSD decay), kernel-resident policies that churned while +accounting and enforcement endured (research/0002 Part 1). **The cost:** any capability to a high-MCP thread is +priority authority, to be handed out sparingly. + +- **Run queues.** Per core, 256 intrusive FIFO lists and a 256-bit bitmap: the next thread is a + count-leading-zeros over four `u64` words — O(1). A preempted thread re-enters at the head of its level; one + whose timeslice ended, at the tail; the running thread and one switched to directly are never queued. + *(Elphinstone & Heiser, "From L3 to seL4", SOSP 2013.)* The per-core **release queue** is sorted by next + refill, O(n) in contexts only the `SchedControl` holder adds. +- **Priority-aware direct switch** (RFC-0004 §4). When *C* wakes *W* by IPC on the same core and *W* has released + budget: if *C* blocks (`call`, `recv`, `reply_recv`), switch to *W* when its effective priority is at least the + highest ready; if *C* stays runnable (`send`, `reply`, `notify`), only when *W* is also strictly more urgent. + Otherwise *W* is queued — on the release queue without budget, on its own core with an IPI (§12). +- **Endpoint queues are priority-ordered, first-come within a level** — seL4 MCS's `tcbAppend` + (`include/object/tcb.h`, "priority ordered endpoint or notification queue"), walking back from the tail; the + FIFO `tcbEPAppend` is compiled only without MCS. The walk is O(n) with interrupts masked, *n* bounded by the + thread array's fixed capacity (RFC-0005 §5) and counted in the worst path; `set_priority` repositions a queued + thread. **Rejected: FIFO** *(classic L4, non-MCS seL4)*: O(1), but a process could create threads from its own + Pool and queue *N* calls ahead of a more urgent client of a shared server, which cannot reorder them. + +## 7. Donation, inheritance and budget expiry (verdicts 7, 8) + +**Donation.** When *C* `call`s a **passive** receiver *S*, the kernel moves *C*'s current context to *S*, recorded +in the single-use reply object *R* (RFC-0004 §8); `reply` or `reply_recv` moves it back. *S* runs at +`max(prio(S), eff(C))`, **fixed at donation**, not propagated if *C*'s priority later changes — O(1), one hop at +a time. Lending priority is safe because time is lent with it. *(Ford & Lepreau, migrating threads, 1994; QNX +priority inheritance; seL4 MCS passive servers.)* + +**An active receiver gets no donation (amendment A1).** It runs on its own context and priority, as in seL4 MCS +(`reply_push`, `src/object/reply.c`, donates only to a receiver with none): a thread holds one context, and an +active server chose to pay for itself. RFC-0004 §4 and §8 lend unconditionally, so this amends them. **The +cost:** an active server inherits nothing, and a low-priority one blocks urgent clients; Constitution §3's +inheritance holds for passive servers only. + +**Inversion, bounded.** Priority-ordered queues serve the most urgent waiter next, but the request in service +runs on its client's context and a middle-priority thread can preempt it. `prio(S)` is therefore a **ceiling +floor**, bounding inversion to one request when set to the highest client priority *(the priority-ceiling bound +seL4 MCS relies on)* — **required, not optional, for a server shared across trust domains**, passive or active. +**Rejected:** boosting a busy server to a waiting sender's priority (QNX): the kernel would guess which thread +serves an endpoint and walk unbounded chains. + +**Caller death never unfunds a server.** If *C* exits or is killed mid-request, *R* is destroyed but the context +stays with *S* until *S* next blocks in `recv` or `reply_recv` (its `reply` fails `PeerGone`); it then detaches, +and only its capability holder may rebind or destroy it. A client's `thread_exit` never pulls time from a server +*(seL4 `reply_remove_tcb` likewise leaves the context with the server)*. + +**The 2026-08-01 amendment, discharged as amended,** after seL4 RFC-14 (Mitchell Johnston, "Budget limit +thresholds on endpoints for SC Donation", seL4/rfcs pull request 24, open): + +- **Prevention — `min_budget`,** fixed at endpoint creation (0 for none; RFC-0007 encodes it). A `call` needs + released budget of at least `min_budget + MIN_BUDGET`, the margin paying for the `call` and `reply` — **this + RFC's rule**; RFC-14's exact comparison is to be quoted before acceptance. A context whose `B` can never meet + it fails `BudgetRefused`; a non-donating `send` to such an endpoint is invalid. +- **A caller short *now* waits (amendment A2),** where the amendment says "refused up front": a partial context + has its refills merged and deferred, waits `Throttled`, and the call restarts when the head refill suffices — + free in an event kernel, O(refills) ≤ 8, the deferral the RFC-14 discussion describes; a **full** context ends + its timeslice and retries on the next. Nothing is donated below the bar either way; refusal makes clients spin. +- **Recovery — one layer down.** If a donated context is exhausted with no refill due while passive *S* runs, the + kernel returns it to *S*'s immediate caller, whose wait on *R* completes with `BudgetExpired`; *R* is consumed, + so a late `reply` fails closed. *S* is left `Unfunded`, registers intact. If `timeout_ep` is live, a **timeout + fault** carries consumed time and donates nothing (seL4 MCS likewise); the handler, on its own time, abandons + the request (`write_regs`) or lends *S* a context. It carries **no identity** — badges are reserved zero until + RFC-0003a — so a handler binds one endpoint per server. Unwinding further (A → B → C) would walk the reply + stack, O(n) with interrupts masked; B gets `BudgetExpired` and can fail A itself. +- **`min_budget` 0 prevents nothing:** one client can strand a shared server for all until a handler funds it + (O-26, A5). Zero suits a server with one client, or one under a supervisor. + +**Rejected:** the unwind without timeout faults — a woken supervisor beats a polling one. **Deferred:** RFC-14's +budget limits, at a reported 22% extra fastpath cost, per-operation figures to be re-checked (Open question 3). + +## 8. The timer and preemption (verdict 9) + +One HAL surface: `now() -> Ticks`, `frequency() -> Hz`, `set_deadline(Ticks)`, `cancel()`, and a `timer_fired()` +up-call. **Tickless:** each exit programs one per-core deadline — the earliest of a partial context's +exhaustion, the timeslice end if an equal-priority thread is ready, and the next refill. A lone full context +arms nothing; a lone partial one still arms its exhaustion. + +- **AArch64: the EL1 virtual timer** — `CNTV_CVAL_EL0`, `CNTV_CTL_EL0`, `CNTVCT_EL0`, and `CNTFRQ_EL0` always + read; PPI INTID 27, the Arm BSA assignment `virt` uses (QEMU `include/hw/arm/bsa.h`). Preferred to the + physical timer, whose EL1 access an EL2 beneath can trap (`CNTHCTL_EL2`); any EL2-to-EL1 descent grants EL1 + timer access and zeroes `CNTVOFF_EL2`. *(Arm ARM DDI 0487, "The Generic Timer".)* +- **x86_64: the local APIC timer**, x2APIC where `CPUID.01H:ECX[21]` reports it, enabled by + `IA32_APIC_BASE.EXTD` (bit 10). TSC-deadline mode (LVT mode `10b`; MSR `0x6E0`) only when `CPUID.01H:ECX[24]` + **and** invariant TSC (`CPUID.80000007H:EDX[8]`) are reported; else one-shot, calibrated at boot, a past + deadline clamped to an initial count of 1, since 0 stops the timer. QEMU's TCG lacks TSC-deadline + (`target/i386/cpu.c`), so one-shot is what it runs. *(Intel SDM Vol. 3A.)* `CR4.TSD` set; `hlt` faults at CPL 3. +- **Userspace timers (RFC-0004 §9.3), named now, built later.** The watchdog is load-bearing (RFC-0004 §8) and + the timer kernel-reserved, so the kernel provides the source: a **deadline object**, bound to a notification, + armed with an absolute time in nanoseconds, kept in the release queue beside refills, charged to a Pool, its + insert bounded by the deadline array's capacity *(Zircon's timer object)*. **Rejected:** minting a second + hardware timer — AArch64 has the EL1 physical timer (PPI 30), x86_64 nothing per core short of the HPET. + +**Kernel-reserved bits, owned here.** RFC-0005 (proposed) writes `SCTLR_EL1` whole and must carry them; its §13 +step 5 says `nTWE = 0` today and needs correcting. + +| Register | Value | Why | +|----------|-------|-----| +| `SCTLR_EL1.nTWI` (bit 16) | 0 | EL0 `wfi` traps (EC `0x01`) and completes as `yield`; `ELR_EL1` holds the `wfi` itself, so the saved PC advances by 4 | +| `SCTLR_EL1.nTWE` (bit 18) | 1 | EL0 `wfe` does not trap, so spin-lock backoff costs no kernel entry; the `sev` residual is in §15's O-9 row | +| `SCTLR_EL1.UMA` (bit 9), `SA` (bit 3) | 0, 1 | no EL0 DAIF access; `SP` alignment checked at EL1 (§9) | +| `CNTKCTL_EL1`, `PMUSERENR_EL0` | 0 | no EL0 counter, timer or PMU; written at boot because their reset values are not architecturally fixed | + +## 9. The context switch — what is saved, where + +A context switch is *which frame the exit path restores*; assembly stays in the entry and exit stubs in +`kernel/src/arch/**`. **The user frame lives in the TCB.** At EL0, `SP_EL1` points at the end of the thread's TCB +frame, so the entry stub's stores land there before it loads the per-core stack from the `TPIDR_EL1` block; with +`SA` on and the frame 16-byte aligned, the current-EL `SP_ELx` synchronous vector reports a frame overwrite if +`SP` lies inside a TCB. On x86_64 an interrupt from ring 3 loads `RSP` from `TSS.RSP0`, the TCB frame; **`syscall` +does not switch `RSP`**, so its stub runs `swapgs`, parks the user `rsp` in per-CPU scratch, loads the frame +pointer, saves, then loads the kernel stack. RFC-0007 (proposed) owns both entry sequences; this RFC owns the +layout and §3's IRQ stub. The address-space switch (`TTBR0_EL1` with ASID; `CR3` with PCID) is RFC-0005's, made +on exit when the process differs — where a time-protection flush would go (Ge et al., EuroSys 2019). + +| What | AArch64 | x86_64 | +|------|---------|--------| +| Every entry, into the TCB | `x0`–`x30`, `SP_EL0`, `ELR_EL1`, `SPSR_EL1`: 34 words | `SS`, `RSP`, `RFLAGS`, `CS`, `RIP`, an error-or-vector slot, 15 GPRs: 21 words | +| Thread-local bases, per switch: 2 more words | `TPIDR_EL0` (EL0-writable) saved and restored; `TPIDRRO_EL0` restored | `FS_BASE` and user GS base restored; `CR4.FSGSBASE` off, so only the kernel sets them | +| Also per switch | `CPACR_EL1.FPEN` (§10) | `CR0.TS` (§10); `TSS.RSP0` | +| Lazily (§10) | `V0`–`V31`, `FPCR`, `FPSR`: 520 bytes, 16-byte aligned | XSAVE area, `XCR0` = x87, SSE, AVX: 832 bytes, 64-byte aligned | +| Never | kernel registers, debug and PMU state | the same | +| **TCB size** | 36-word frame (288 B) + FP area padded to 528 B + ~180 B of fields: **1 KiB** | 23-word frame (184 B, padded to 192) + 832 B XSAVE + ~180 B: **1.25 KiB** | + +**O-5 on frames.** `write_regs` never lets userspace choose its privilege: the kernel builds `SPSR_EL1` (EL0t, +DAIF clear, only NZCV from the caller); on x86_64 `CS`/`SS` are constants, `RFLAGS` takes only status flags (IOPL +0, IF set), and a non-canonical `RIP` or base is refused. It writes `TPIDR_EL0` and `FS_BASE` only; `TPIDRRO_EL0` +and the user GS base are the kernel's IPC-buffer discovery registers (RFC-0007 §5). NMI, `#DB`, `#DF` and `#MC` +use IST stacks, as they can arrive before `syscall`'s stack switch. + +## 10. FP/SIMD — owned by userspace, enabled per thread, saved lazily (verdict 10) + +- **Enabled per thread** by `set_fp`, off by default. `CLAUDE.md` says "per process"; per thread is finer, so an + FP-off server thread in an FP-using process never forces a save, and § Architectures changes with this RFC. A + thread with FP off that touches FP takes an ordinary fault. +- **Loaded on first use, saved lazily.** Each core records an FP *owner* as an `(index, generation)` pair; every + other thread runs trapped — `CPACR_EL1.FPEN = 0b00` (EC `0x07`) or `CR0.TS = 1` (`#NM`). Since `0b00` traps EL1 + too and `XSAVE` raises `#NM` under `TS`, the handler first grants itself access (`FPEN = 0b01`, EL0 still + trapped, and `isb`; or `clts`), saves a live owner, loads the new owner's registers or zeros, sets `FPEN = + 0b11`, `isb`, and returns. A `call` to an FP-off server saves nothing. +- **The owner is cleared,** unsaved, when it is destroyed or `set_fp(off)`; a thread reusing its slot fails the + generation check and loads zeros, never a dead thread's registers (O-8, O-9). +- **The kernel's only FP instructions** are those stubs in `kernel/src/arch/**`, run with access granted; the + soft-float target guarantees generated code. No `FPEN` value traps EL1 while allowing EL0. +- **Extent.** x86_64 sets `CR4.OSFXSR`, `CR4.OSXSAVE` and `XCR0 = 0b111` — the 832-byte standard-format area. + AVX-512, AMX and SVE (`CPACR_EL1.ZEN`) stay disabled and fault. **LazyFP** (CVE-2018-3665; Stecklina & + Prescher, 2018) lets a non-owner read the owner's registers speculatively on affected Intel cores: out of + scope (threat model §7), Open question 2. + +## 11. Interrupts — the controller, and device IRQs as notifications (verdict 11) + +The kernel owns the controller and nothing behind it *(seL4 `IRQControl`/`IRQHandler`)*. + +- **Objects.** One `IrqControl` (the root's) mints at most one `IrqHandler` per device line; the timer PPI, IPI + SGIs or vector and spurious INTID 1023 are never minted. `bind(irq, notification, bits)` invokes the + `IrqHandler` (`WRITE`) and presents the notification (`WRITE`); `ack(irq)` needs `WRITE`. **Phase 1 routes + every line to the boot core**; SMP routing is `IrqControl`'s, never `SchedControl`'s (Open question 6). Shared + PCI INTx lines on `q35` are **unsupported** until MSI. +- **Delivery.** The kernel acknowledges, **masks the line**, signals end of interrupt, ORs `bits` into the + notification and wakes a waiter; the driver's `ack` unmasks. A level-triggered line cannot storm, though it + fires once per `ack` (§17). A destroyed notification leaves the line masked; the `IrqHandler` outlives a + crashed driver, and a restarted one re-binds (O-17). +- **AArch64: GICv3 first.** `GICD_CTLR.ARE` and `EnableGrp1` (`virt` without `secure=on` has one security state, + `DS = 1`); SPIs through `GICD_ISENABLER`, `GICD_IPRIORITYR`, `GICD_IROUTER`; the redistributor woken + by `GICR_WAKER`, SGIs and PPIs through `GICR_ISENABLER0` and `GICR_IPRIORITYR`; every line in Group 1 (Group + 0 arrives as FIQ) at a priority numerically below `ICC_PMR_EL1`'s mask; `ICC_SRE_EL1.SRE`, `ICC_IGRPEN1_EL1`, + `ICC_IAR1_EL1`, `ICC_EOIR1_EL1`. On `virt`: distributor `0x0800_0000`, redistributors from `0x080A_0000` (QEMU + `hw/arm/virt.c`), via RFC-0005's MMIO window. *(Arm IHI 0069.)* **Cost:** `virt` picks GICv2 at eight CPUs or + fewer, so xtask adds `gic-version=3`; the Raspberry Pi 4's GIC-400 (GICv2) is a **known** second driver. +- **x86_64: LAPIC and I/O APIC.** The 8259s are masked; I/O APIC entries carry the mask bit; end of interrupt + goes to the LAPIC (x2APIC EOI MSR `0x80B`). **MSI waits for the driver RFC:** without interrupt remapping a + device can aim any vector at any core — O-18's precondition. +- **Latency** is §3's worst path between preemption points. RFC-0007's console write must take one per + FIFO-full poll, restartable by byte count; until then it holds the kernel about 44 ms per 504 bytes on + hardware (nothing on QEMU, which has no baud delay). + +## 12. Multi-core shape, placement and exclusive cores (verdict 11) + +Phase 1 runs `-smp 1`; the shape is fixed now so multicore is not bolted on. + +- **Everything scheduling-related is per core.** A thread runs on its context's core, so donation can move a + server between cores; **the kernel never load-balances.** Cross-core wake-ups (RFC-0004 §9.2) enqueue *W* on + its core and send an IPI (`ICC_SGI1R_EL1`; the LAPIC ICR). Direct switch is same-core only. +- **One big kernel lock when SMP lands**, on every entry, the fast path included *(Peters, Danis, Elphinstone & + Heiser, "For a Microkernel, a Big Lock Is Fine", APSys 2015)*. This **rejects the premise** of RFC-0003 + §14.2, sharing without a global lock on the fast path; resolve→check→act holds within an entry, and §3 covers + restarts (A4). +- **A core waiting for the lock services IPIs while it spins** *(as seL4's CLH lock does)*: two operations need + a synchronous answer from another core — RFC-0005's x86_64 TLB shootdown, lacking a broadcast, and **FP state + live elsewhere**: a thread whose registers core X owns lazily, run next on core Y, has Y ask X by IPI to save + them. Cost: a cross-core FP handoff is an IPI round trip. +- **Cores are parked until funded (default-deny).** On QEMU `virt` with `-kernel` the DTB advertises PSCI and + secondaries start powered off (checked on QEMU 8.2.2: CPU 1 never leaves the entry address), so `boot.s`'s + `wfe` loop matters only on spin-table firmware. The first `sc_configure` onto a core starts it — PSCI + `CPU_ON`, conduit from `/psci`; INIT-SIPI-SIPI on x86_64 — in increment 14, `boot.s`'s comment with it. +- **SMT placement, one sentence now** (research/0002 Part 6, after L1TF and MDS): a context will carry a class + set only by the `SchedControl` holder; SMT siblings never run different classes, donation never crosses one. + The field is reserved zero until increment 14, so no thread labels itself; SMT-off is "never fund the sibling". +- **Exclusive assignment is a degenerate case, not a mode** (research/0002 Part 6, after Jailhouse): one thread, + a full context, nothing else on the core — one bitmap bit, no timer armed, no IPI unless the `SchedControl` + holder acts, lines routed elsewhere, counters updated only at the next entry. A recipient checks the promise + with `ctl_info`: one context, reference count 1. + +## 13. Amendments proposed to accepted documents (verdict 12) + +Each, if accepted, is appended to its target as a dated amendment and logged in `docs/CHANGELOG.md` (Changed). + +| # | Target | Change | Why | +|---|--------|--------|-----| +| A1 | RFC-0004 §4, §8 | `call` donates only to a **passive** receiver; an active one runs on its own context | a thread holds one context; seL4 MCS `reply_push`; cost in §7 | +| A2 | RFC-0004 amendment 2026-08-01 | a caller short *now* waits `Throttled`; only a context that can *never* pass is refused | refusal makes clients spin; nothing is donated below the bar either way | +| A3 | the same, and research/0002 Part 6 | seL4's timeout faults ship in MCS (`seL4_Fault_Timeout`); what is unmerged is RFC-14's threshold | a factual correction to "have remained future work" | +| A4 | RFC-0003 §14.2 | the big lock covers the fast path by design; the question is closed by rejecting its premise | §12; Peters et al. 2015 | + +## 14. Lineage + +| Source | What is taken | What is left | +|--------|---------------|--------------| +| **seL4 MCS** (Lyons et al. 2018) | contexts as objects; passive servers; `SchedControl`; any-capability MCP; sporadic refills; `MIN_BUDGET`; timeout faults and TCB-held handlers; priority-ordered endpoint queues; no donation to active receivers | the WCET scale factor | +| **seL4 RFC-14** (Johnston) | the endpoint threshold, deferral, one-layer return | budget limits, for now | +| **Heiser & Elphinstone 2016; Fluke 1999; Elphinstone & Heiser 2013** | the event kernel; the running thread unqueued; priority-aware direct switch | per-thread kernel stacks; lazy scheduling; L4's unconditional switch | +| **QNX Neutrino; Ford & Lepreau 1994** | inheritance across the message; partitions on budgets; the migrating-thread `call` | inheritance to busy servers; Mach | +| **Sprunt, Sha & Lehoczky 1989; Zircon** | the sporadic server; the timer object | an unbounded replenishment list; per-thread timeslices | +| **Jailhouse; Peters et al. 2015; Linux** | parked cores, exclusive assignment; one big lock; the idle rule; PSI-style counters | static-only partitioning; fine-grained locking before measurement; dynamic priorities | + +## 15. Obligations + +| Obligation | This RFC | Status after implementation | +|-----------|----------|-----------------------------| +| O-7 no unprivileged exhaustion | time only through contexts; `MIN_BUDGET`; eight refills; O(1) expiry return; bounded queue walks; no wait holding a lock; lines masked until `ack` | **discharged for CPU time and scheduler structures, except interrupt-entry time**, billed to the running context and bounded per `ack`; memory is RFC-0005's half | +| O-4 no ambient authority | no thread runs without a context; priority through MCP, born 0; time through `SchedControl`; lines through `IrqControl`; only `yield` and `thread_exit` authority-free | **discharged for time** | +| O-5 argument validation | `write_regs` sanitises `SPSR_EL1`/`RFLAGS`, refuses non-canonical `RIP` and bases, cannot reach the discovery registers; restarts re-resolve | **discharged for this surface** | +| O-9 no ambient side channel | no EL0 counter, timer or PMU; FP owner cleared on reuse; parked cores. **Residual:** untrapped `wfe` lets a thread observe another's `sev` (Arm ARM: an SEV on any PE is a wake-up event) — one bit, no data | **contributes**; fine-grained timing channels stay out of scope | +| O-17 contained drivers | lines as notifications, masked until `ack`; `IrqHandler` outlives a crashed driver; fault endpoints the thread cannot close; stall counters | **enables**, weakened where a child holds `WRITE` on its own threads (§4) | +| O-18 confined DMA | MSI deferred until interrupt remapping is designed | **named, not discharged** | +| RFC-0004 amendment, 2026-08-01 | (1) `min_budget` at `call`, deferral per A2; (2) `BudgetExpired` on the reply object, plus timeout faults; caller death cannot bypass (1) | **both discharged as amended by A1–A2** | + +## 16. Graves checked (§3) + +| Grave | How this RFC stays out of it | +|-------|------------------------------| +| **Policy in the kernel** | no admission, balancing or budget choice; the constants it does choose are 256 levels, eight refills, `MIN_BUDGET`'s factor 2, the XCR0 extent, the thread and deadline array capacities (RFC-0005), and §19's interim constants until measured | +| **The catch-all right** | priority authority is a relation (MCP); `SchedControl` has one mutating method, selling time on one core, and a read of its own state; topology is data, routing is `IrqControl`'s; §4's list is closed | +| **Bolted-on multicore** | per-core state, IPIs, the lock and its IPI-servicing spin, FP handoff, shootdowns and core start-up are stated before any SMP code | +| **Drivers in the kernel; unused device paths** | the kernel masks and signals, never services a device; one controller and one timer per target; unclaimed lines never enabled | +| **Baroque hierarchies; multi-copy IPC** | contexts are flat; donation moves a reference to time | + +## 17. Costs — what this makes harder + +| Cost | Detail | +|------|--------| +| **Every server needs someone to think about time** | a passive server cannot run until called; an active one needs a configured context and inherits nothing (A1); "spawn a thread and it runs" is gone | +| **A stranded server is userspace's problem** | `min_budget` 0 lets one client strand it for all; a supervisor is required before any passive server on partial contexts is trusted | +| **Caps, not minima** | a spent partial context idles its core even when nothing else would run | +| **Priority-ordered endpoint queues** | an O(n) walk with interrupts masked, *n* up to the thread capacity | +| **Interrupt time is billed to whoever runs** | a driver `ack`ing a level line in a loop charges other processes, one interrupt per `ack` — seL4's choice; passive drivers (Open question 4) could bill the driver | +| **No userspace timer yet** | RFC-0004 §8's load-bearing watchdog lacks a source until increment 15 — an unmet RFC-0004 dependency | +| **Exclusivity is checkable, not revocable** | `ctl_info` shows whether a grantor kept a copy; if one did, it can still configure onto the core | +| **MCS is seL4's least-verified part** | sporadic refills are subtle — hence property tests | +| **About 1 KiB per TCB (1.25 KiB on x86_64)** | FP space included for threads that never use it | +| **Lazy FP's cure** | eager restore into another process's FP thread moves 520 bytes or an 832-byte `XRSTOR` (9 or 13 cache lines), beside a `call` round trip of roughly 380–630 cycles (research/0001) | + +## 18. Open questions + +1. **EL0 counter access.** Proposed: a property of the *context*, set by the `SchedControl` holder and switched + with it (`CNTKCTL_EL1.EL0VCTEN`; `CR4.TSD`), default deny — not a thread flag a process sets on itself. +2. **LazyFP on x86_64.** Eager restore for cross-process switches into FP threads (costed in §17)? +3. **RFC-14 budget limits.** Worth their fastpath cost, once re-measured, to stop a server overspending? +4. **Passive drivers** need a context bound to a notification (MCS); interrupt entry could then bill the driver. +5. **Numbers from measurement:** `MIN_BUDGET`, stack size, the worst path; x86_64's clock without invariant TSC. +6. **Interrupt routing on SMP:** per-(line, core) handlers minted by `IrqControl`, or a per-core interrupt-target + capability — decided with increment 14. + +## 19. Implementation increments + +Pure logic lands in a new host-tested `no_std` workspace crate, `scheduler/`, generic over a thread index as +`capability/` is over `ObjectRef` (`CLAUDE.md` § Layout gains it in increment 1); hardware behaviour is proved by +counted boot-test strings. New `unsafe` stays in `kernel/src/arch/**`. The x86_64 HAL gains stubs that compile — +`-> !` ones halt — so its entry still calls into the kernel proper. **D** marks what the demo needs. + +| # | PR | Proves; how tested | Lands after | D | +|---|----|--------------------|-------------|---| +| 1 | `scheduler` I: run queues, the ten states, MCP, the priority-ordered endpoint queue | exhaustive host transition table against §4's "Left by" column; "a new thread cannot serve as `auth` above 0"; built for both targets | — | D | +| 2 | `scheduler` II: full contexts, nanosecond conversion and rounding, billing, stall counters, interim constants | host tests against a shadow model | 1 | D | +| 3 | GICv3 and the virtual timer, kernel-only; `CNTKCTL_EL1`, `PMUSERENR_EL0` zeroed; idle and its abandon-idle stub | xtask gains `gic-version=3`; `timer: tick 3` | — (physical addresses; 0005#9 must repoint the GIC with the console) | D | +| 4 | Event-kernel dispatch at EL0, no address spaces yet: TCB frames and dispatch under RFC-0007#3's trap stub; §8's `SCTLR_EL1` bits | two EL0 self-test threads alternate under the timer: `sched: A B A B`; an EL0 `wfi` returns: `sched: wfi yields` | 3, 0007#3 | D | +| 5 | Threads in address spaces; the boot stack moved into the guarded window, `aarch64.ld`'s comment with it | a spinning EL0 thread is preempted and resumes intact: `user: still here` | 4, 0005#10 | D | +| 6a | Thread, SchedContext, `SchedControl` as RFC-0005 object-store slots; state machine wired; `(index, generation)` links | host: destroy a lent context, reuse the slot, `reply` — nothing moves | 2, 0005#7 | D | +| 6b | Methods behind RFC-0007's dispatcher: `sc_configure`, `bind_sc`, `resume`, `set_priority`, `write_regs`, `thread_exit` | the root runs two EL0 threads at one level: `[a] 1 [b] 1 [a] 2` | 5, 6a, 0007#6 | D | +| 7a | The direct-switch decision as a pure function | host tests over every §6 case | 1 | D | +| 7b | Endpoint queues and the IPC blocking states, wired | host: queue order; `suspend` from each blocked state | 6b, 7a | D | +| 7c | Integration with RFC-0007#10 | its three `Kaya!` lines, then `[client] preempted` from a spin after the reply | 7b, 0007#10 | D | +| 8 | Passive servers, donation, inheritance, the caller-death rule | host: a client exits mid-request, the server finishes and serves the next; `passive: served` | 7c | stretch | +| 9 | `scheduler` III: partial contexts, refills, merge, release queue | property test: no window of length `T` sees more than `B` consumed | 2 | | +| 10 | `min_budget`, deferral, expiry return, fault and timeout endpoints, `Unfunded` | `BudgetRefused`, then `BudgetExpired` and `timeout fault` for an overrunning server | 8, 9, 0007#11 | | +| 11 | Lazy FP/SIMD | two FP threads load markers into `v0`, each finds its own: `fp: isolated`; host: owner destroyed, slot reused, zeros loaded | 6b | | +| 12 | `IrqControl` and `IrqHandler`; xtask gains serial input injection | PL011 receive (SPI 1, INTID 33) reaches an EL0 driver: `irq: notified` | 7c | | +| 13 | x86_64 scheduling HAL (IDT, TSS, IST, LAPIC, `#NM`, `XSAVE`) | 3–5 and 11 again | its boot RFC, 0007#12 | | +| 14 | SMP: PSCI `CPU_ON`, INIT-SIPI, the lock and its IPI-servicing spin, FP handoff, shootdowns, classes, routing | `-smp 2` boot-tests | 13 | | +| 15 | Deadline objects (RFC-0004 §9.3) | host tests on the shared release queue; `deadline: fired` | 9 | | + +**What the demo takes as interim, honestly.** It needs 1–7c and runs full contexts only. + +- **Its server is active** — the root doubles as server (RFC-0007 §18) — so the demo exercises **A1's semantics, + not RFC-0004 §4's**: nothing is donated. Increment 8 is one more PR, safe before 9 and 10 because a lent full + context refills at once; expiry inside a server needs a partial context. +- **Provisional constants** in `scheduler/src/config.rs` until measured: `MIN_BUDGET_INTERIM` = 100 µs; + `ROOT_TIMESLICE` = 5 ms, a full context; root priority and MCP 255, the root putting itself and the client at + 100 to share a level; `KERNEL_STACK_SIZE` = 16 KiB. Cost: the budget floor is a guess. +- **No fault handler** (a faulting thread goes `Inactive`, RFC-0007 §7); **a non-preemptible console write** + (free on QEMU, 44 ms on hardware); **no userspace timer** for RFC-0004's watchdog; **x86_64 stubs** that halt. + +## 20. What this unblocks + +RFC-0004's implementation gets threads to rendezvous between; drivers get interrupts as notifications (O-17); +the broker gets levers to sell time without the kernel knowing why — `SchedControl`, MCP, `min_budget`, stall +counters. Next on paper: the x86_64 boot RFC (increment 13), an SMP amendment (14), and §13's dated entries. diff --git a/docs/rfcs/0007-system-calls-and-process-bootstrap.md b/docs/rfcs/0007-system-calls-and-process-bootstrap.md new file mode 100644 index 0000000..c86f70a --- /dev/null +++ b/docs/rfcs/0007-system-calls-and-process-bootstrap.md @@ -0,0 +1,500 @@ + + +# RFC-0007 — System calls and process bootstrap + +| Field | Value | +|-------|-------| +| Status | **Proposed** — 2026-09-27, awaiting the maintainer's verdict | +| Author | Drafted by Claude Code as sparring partner; verdict the maintainer's | +| Date | 2026-09-27 | +| Affects | Constitution §3 (capabilities are the only authority; the Language clause) and §4 (a Borrow Ledger reading, §12); `CLAUDE.md` § `unsafe` policy and § Layout; threat model O-6's text; RFC-0003 (a dated amendment: the handle word, a slot-generation bound, `free_slots`, one error variant split); RFC-0004 §8 (a dated amendment: reply objects are unbound, not destroyed); `docs/CHANGELOG.md`; the workspace (`user/`), the comments in `Cargo.toml` and `xtask/Cargo.toml`, `kernel/src/main.rs`'s grep scope; `xtask`, `kernel/build.rs` and `aarch64.ld`; the kernel's trap path | +| Depends on | RFC-0003 (accepted; §9 binds every syscall); RFC-0004 (accepted; §5, §6, §8, §9.4, §10 and the 2026-08-01 amendment); RFC-0005 and RFC-0006 (proposed, drafted alongside); a future x86_64 boot RFC for the UEFI stub | +| Discharges | O-5 (argument validation) for the syscall surface; O-27 (explicit authority at spawn); binds O-1, O-2 and O-4 at B1; keeps O-6 Built with a third designated tree; contributes to O-7, O-9 and O-13; designs O-17's fault path | + +> **Proposed verdicts.** +> +> 1. **Uniform invocation:** every kernel-object operation is a `call` on its capability; twelve syscalls in all (§4). +> 2. **Method arguments in registers:** handle words in MR0–MR3 are *presented* — resolved, checked, never moved — unless marked *moved* (§4). +> 3. **Reply objects are reusable:** `reply`, budget expiry and caller death unbind them — a dated RFC-0004 amendment (§4). +> 4. **Registers:** AArch64 `svc #0`, number in `x8`; x86_64 `syscall`, number in `rax`; threads start with zeroed registers but four (§3). +> 5. **Messages:** four physical and 64 virtual message registers, three capabilities, an optional 1 KiB IPC buffer, fetched once at rendezvous (§5). +> 6. **IPC-buffer discovery:** a kernel-set, user-read-only register — `TPIDRRO_EL0`; the user GS base with a self-pointer at `gs:[0]` (§5). +> 7. **Handle word:** 20-bit index, 44-bit slot generation; word `0` is null; recorded as a dated RFC-0003 amendment (§6). +> 8. **Errors in two layers:** numbered transport status in a register, method result in the reply label; faults are not errors (§7). +> 9. **Process object:** table, one AddressSpace for life, threads; born empty; `GRANT` only until the first `resume`; then `WRITE` means `KILL` (§8). +> 10. **One root task,** built once from a load descriptor, every boot capability listed in BootInfo, no "is root" branch anywhere (§9). +> 11. **Boot images:** `arch::boot_modules()` yields descriptors a host-side ELF reader made; the kernel parses no ELF; AArch64 embeds, as an interim (§10). +> 12. **Console as a capability:** one `WRITE` of at most 24 bytes that never waits; deleted when the Phase-2 UART driver lands (§11). +> 13. **`user/abi`** is the microkernel-core row; its `src/arch/**` — trap instructions and entry stubs only — is the third `unsafe` tree (§12). + +## 1. The question + +**How does userspace ask the kernel to do anything, and how does the first userspace come to exist — +such that every request names a capability, no argument is trusted, and no process is born holding +authority it was not explicitly handed?** + +RFC-0003 §9 fixed the rule and RFC-0004 §10 the IPC semantics; both left the encoding here. This RFC +designs it, the trap, the process as a kernel object, and the bootstrap seam RFC-0003 §14.4 named. It does +not design address spaces (RFC-0005), threads (RFC-0006), or any policy on which programs run holding what. + +## 2. Which pillar + +**Pillar 2 and the doctrine that capabilities are the only authority.** The syscall surface is the whole +of B1; one entry naming a resource without a handle makes RFC-0003's table decorative. Spawn is where +research/0002 found the freshest scar (Part 4: runc CVE-2024-21626, one inherited descriptor became host +traversal), and O-27 exists because of it. Boot images reach userspace read-only (pillar 1). + +## 3. Entering the kernel + +**AArch64 — `svc #0`** traps from EL0 to `VBAR_EL1 + 0x400` with `ESR_EL1.EC = 0x15`, the immediate in +`ISS[15:0]`, `ELR_EL1` past the `svc`, DAIF masked and `SP_EL1` selected *(Arm ARM DDI 0487)*. The stub +saves `x0`–`x30`, `SP_EL0`, `ELR_EL1` and `SPSR_EL1` into the thread's frame (RFC-0006 (proposed) §9 owns +the layout) and dispatches on EC: `0x15` is a syscall, anything else a *fault* (§7). A non-zero immediate +answers `InvalidArgument`, so a later ABI revision is detectable. `eret` uses an `SPSR_EL1` the kernel +builds: EL0t, DAIF clear, NZCV from the frame, `DIT` and `SSBS` where implemented (the Cortex-A72 has +neither), every other bit zero. + +**x86_64 — `syscall` / `sysretq`.** `syscall` needs `IA32_EFER.SCE`, loads `RIP` from `IA32_LSTAR`, leaves +the return `RIP` in `rcx` and `RFLAGS` in `r11`, clears the `IA32_FMASK` bits (here IF, DF, TF and AC) and +does **not** switch stacks *(Intel SDM Vol. 3A, "Fast System Calls in 64-Bit Mode")*. As RFC-0006 §9 +requires, the stub runs `swapgs`, parks the user `rsp` in per-core scratch, loads the TCB frame pointer, +saves into the frame, and only then loads the per-core kernel stack. **The exit uses `sysretq` only when +`rcx` is canonical and the frame's `RFLAGS` has TF and RF clear and IOPL 0, else `iretq`:** a +non-canonical `rcx` makes Intel's `sysretq` fault *in ring 0* on the user's stack (CVE-2012-0217), and +`sysretq` sets `RFLAGS` to `r11 AND 3C7FD7H OR 2` (SDM Vol. 2B, SYSRET), which passes TF — Linux takes +`iretq` for TF or RF likewise (`arch/x86/entry/entry_64.S`). RFC-0005's unmapped top user page and +RFC-0006's sanitising `write_regs` already prevent both; the exit checks anyway. **Rejected:** `sysenter`, +absent on AMD in long mode; an `int` gate, a full IDT delivery per call. + +| Role | AArch64 | x86_64 | +|------|---------|--------| +| syscall number (in) | `x8` | `rax` | +| invoked handle (in) / status (out) | `x0` | `rdi` in, `rax` out | +| message tag (in/out) | `x1` | `rsi` | +| MR0–MR3 (in/out) | `x2`–`x5` | `rdx`, `r10`, `r8`, `r9` | +| reply-object handle (in) | `x6` | `r12` | +| error detail (out) | `x7` | `r13` | +| clobbered by hardware | — | `rcx`, `r11` | + +Other registers are restored from the frame and result registers carry a result or zero, so no kernel +value leaves in a register (O-9). `x8`/`rax` follow Linux; the x86_64 column avoids `rbx` and `rbp`, which +Rust inline assembly cannot name. **No argument is a pointer** (RFC-0005 (proposed) §11 owns the rule): only +the IPC buffer is touched, by frame (§5) — on the Cortex-A72, which lacks PAN, the whole defence. + +**Every thread starts** at its entry PC with SP as given (16-byte aligned) and two start values in `a0`, +`a1` (`x0`/`x1`, `rdi`/`rsi`); every other general register zero; EL0t with DAIF clear, or ring 3 with +`RFLAGS` = `0x202`; FP/SIMD trapped until RFC-0006 enables it; `TPIDR_EL0` and `FS_BASE` zero. The entry +symbol is an `abi` assembly stub that calls a Rust `extern "C" fn`, so AAPCS64 and SysV each see their +entry alignment. The trap wrappers are single-instruction `asm!` intrinsics (Open question 4). + +## 4. The syscall set + +**Options.** **A — one syscall per operation** *(Zircon, Linux)*: every object type grows the table and no +server can stand in for a kernel object. **B — uniform invocation** *(seL4; KeyKOS)*: a handful of IPC +syscalls, a kernel-object operation being a `call` on its capability with the method in the tag's label, +answered as a server would answer. **C — B plus a separate `invoke`**: callers could tell a kernel object +from a server, which removes B's one advantage. + +**Verdict sought: B,** for interposition: a Console and a logging server's endpoint are invoked alike, so +Phase 2's UART driver replaces the Console with no client changing. **The claim is scoped:** a server can +stand in for a kernel object whose methods take no handle-word arguments — the Console, and every protocol +a server defines — but not for `map` or `bind_sc`, whose extra handle word means something only in the +caller's table (§16). So `cap_rights` reports rights, never the object's kind. + +| # | Syscall | Handles | Beyond the tag and message registers | +|---|---------|---------|--------------------------------------| +| 0, 11 | `yield`, `thread_exit` | — | authority-free (RFC-0003 §9); `thread_exit` leaves the caller `Exited` | +| 1, 2 | `send`, `nb_send` | object | endpoint: send, blocking or failing `WouldBlock`; notification: signal | +| 3 | `call` | object | endpoint: send and await the reply; kernel object: invoke a method, donating nothing | +| 4, 5 | `recv`, `nb_recv` | endpoint or notification; reply object | receive, blocking or polling; a bound notification may wake it | +| 6 | `reply` | reply object | reply once to the bound caller | +| 7 | `reply_recv` | endpoint; reply object | `reply` then `recv` in one entry — the server loop *(seL4 `ReplyRecv`)* | +| 8 | `cap_derive` | object, with `DUPLICATE` | in: MR0 the rights wanted, MR1 a badge (reserved, zero); out: MR0 the new handle word | +| 9, 10 | `cap_close`, `cap_rights` | object | the handle is dead on return; out: MR0 the rights bits | + +The `cap_*` calls touch only the caller's table and build `Rights` from the crate's named constants, +refusing undefined bits. **A signal sets bit 0** of a notification until badges exist (RFC-0003a), then the +capability's badge, fixed at derivation *(seL4)*: no sender chooses bits, so it stays RFC-0004 §8's +payload-free doorbell; an `IrqHandler` ORs its bound bits (RFC-0006 §11). **Rejected:** a `debug_putc` +(§11); anything taking a PID, path or address; seL4's depth-addressed pointers, made for CNode trees. + +**Reply objects** are created once from a Pool and reused *(seL4 MCS)*: `recv` binds one to a caller, and +`reply`, budget expiry or the caller's death **unbinds** it; `reply` on an unbound one fails `PeerGone`. +RFC-0004 §8 says it "is destroyed if the caller dies", which would let a client that calls and exits in a +loop cost the server a Pool allocation per request — an O-7 drain — so RFC-0004 needs a dated amendment and +RFC-0006 §4 and §7 read "unbinds". + +**Kernel-object methods.** A method is a `call` whose label names it and whose MR0–MR3 carry every +argument; one needing more is split. A handle word there is **presented**: resolved in the caller's table, +checked for its row's right, never moved, never needing `TRANSFER` *(seL4's `extraCaps` on an +invocation)*. A handle word marked **moved** leaves the caller's table, which always needs `TRANSFER` +(RFC-0003 §6). `tag.caps` is zero on every method (`InvalidArgument`): `caps[]` belongs to endpoint +messages, whose receiver needs its new handle words delivered to memory. Replies carry new handle words +from MR0; labels count from 1 per kind; the `abi` data half (increment 2) is the table of record. + +| Invoked (right) | Label: method | MR0 | MR1 | MR2 | MR3 | Reply | +|-----------------|---------------|-----|-----|-----|-----|-------| +| Pool (`WRITE`) | 1 `region_create` | pages | alignment, pages | max extents | rights | Region | +| Pool (`WRITE`) | 2 `as_create` · 3 `process_create` | rights · AddressSpace, presented `WRITE`, bound for life | — | — | — | AddressSpace · Process | +| Pool (`WRITE`) | 4 `thread_create` | Process, presented `WRITE` | its AddressSpace, presented `WRITE` | IPC-buffer address, or 0 for none | — | Thread | +| Pool (`WRITE`) | 5 `sc_create` · 6 `endpoint_create` · 7 `notification_create` · 8 `reply_create` | — · `min_budget` in ns (RFC-0006) · — · — | — | — | — | the new object | +| AddressSpace (`WRITE`) | 1 `map` · 2 `unmap` · 3 `protect` (RFC-0005 §8) | Region, presented · vaddr · vaddr | the space's Pool, presented `WRITE` · — · perms | vaddr | first page (bits 0–31), pages (32–41), perms (48–49) | — | +| Region (`WRITE`) | 1 `region_copy` (RFC-0005, proposed here) | source Region, presented `READ` | source page | destination page | pages, at most 16 | — | +| Process (`WRITE` / `READ`) | 1 `GRANT` · 2 `KILL` · 3 `INFO` (§8) | handle words, **moved**, count in `tag.length` | | | | `GRANT`: words in the child; `INFO`: counts | +| Thread (`WRITE` / `READ`; RFC-0006 §4) | 1 `write_regs` · 2 `read_regs`, a four-word group of RFC-0006's frame in label bits 8–15, group 0 being PC, SP, `a0`, `a1` | `write_regs`: the group's four words in MR0–MR3 | | | | `read_regs`: the group | +| Thread (`WRITE`; RFC-0006 §4) | 3 `resume` · 4 `suspend` · 5 `bind_sc` · 6 `unbind_sc` · 7 `set_priority` · 8 `set_mcp` · 9 `bind_notification` · 10 `unbind_notification` · 11 `set_fault_ep` · 12 `set_timeout_ep` · 13 `set_fp` | 5: SchedContext, presented `WRITE` · 7, 8: `auth`, presented, no right checked · 9: Notification, presented `READ` · 11, 12: endpoint, **moved** · 13: on or off | 7, 8: the value | — | — | — | +| SchedControl (RFC-0006 §5) | 1 `sc_configure` (`WRITE`) · 2 `ctl_info` (`READ`) | SchedContext, presented `WRITE` | budget, ns | period, ns | refills (bits 0–7), class (8–15, zero) | `ctl_info`: counts | +| SchedContext (`READ`) · Console (`WRITE`) | 1 `sc_stats` · 1 `WRITE` (§11) | — · byte count, at most 24 | · bytes | · bytes | · bytes | counters · bytes accepted | + +`IrqControl` and `IrqHandler` (RFC-0006 §11) follow the same rule, labelled when built. Endpoints and +notifications have no methods: they are what `send`, `call` and `recv` act on. + +## 5. Messages, the register budget and the IPC buffer (RFC-0004 §9.4) + +The **tag** is one word: bits 0–6 length in words (0–64); bits 7–8 capabilities (0–3); bit 9 set by the +kernel, on a returned tag only, when a bound notification woke a `recv` (MR0 then holds the bits); bits +16–63 a 48-bit label — user-defined for endpoints, the method for kernel objects, its result on a kernel +reply *(seL4's `seL4_MessageInfo`)*. **Bits 9–15 must be zero in every tag userspace supplies**, so no +sender can forge the notification flag. **Four physical message registers on both architectures:** seL4 +uses four, research/0001 found the in-register payoff small and shrinking (10% on ARM11, negative on modern +x86), and a per-architecture count would make a message fast on one Tier-1 target only. Up to **64 words** +spill MR4–MR63 to the buffer — below seL4's 120 on purpose: 512 bytes bounds the non-preemptible copy, and +RFC-0004 §5 sends bulk through shared regions. **Three capabilities**, a 2-bit field with no invalid +encodings. **Rejected:** six physical registers on AArch64; seL4's 120 words. + +**The IPC buffer** is 1 KiB and 1 KiB-aligned, so it never straddles a page: `#[repr(C)]` words 0 (its own +user address, written by the kernel), 4–67 (MR0–MR63, the first four never read) and 68–70 (`caps[]`), the +rest untouched. **It is optional and reached by frame.** `thread_create` takes its user address, or 0; the +kernel checks it against the AddressSpace's mapping list (RFC-0005 (proposed) §7) — aligned, inside a +read-write mapping — then binds that page of the backing Region, a counted reference and a writable use for +W^X, and reaches it only through the physmap. The address is never dereferenced. A syscall needing a buffer +(a length over four, or any capability) from a thread with none, or a severed one, fails `NoBuffer`. + +**Discovery: a kernel-set, user-read-only register.** The kernel loads the buffer's address into +`TPIDRRO_EL0` (EL0 reads, only EL1 writes) and, on x86_64, into the user GS base with `CR4.FSGSBASE` off, +`abi` reading the self-pointer at `gs:[0]` — the ELF TLS convention of a block whose first word is its own +address *(Drepper, "ELF Handling For Thread-Local Storage")*. RFC-0006 restores both on every switch. +**Rejected:** `TPIDR_EL0` and `FS_BASE`, which a relibc port needs for TLS; seL4's thread-local +`__sel4_ipc_buffer` (libsel4 `functions.h`), which needs TLS first. + +**Transfer and single fetch (O-5).** Another thread can rewrite a buffer mid-syscall, so every buffer word +the kernel acts on is read **exactly once** into kernel memory before any check depends on it; no Rust +reference is formed into it, and payload moves through RFC-0005's volatile-copy module, never interpreted +*(research/0002 Part 5, virtio's double fetch)*. A blocked sender's tag and MR0–MR3 wait in its frame; +**the rest is fetched at rendezvous, in one kernel entry** *(seL4)*: `caps[]` read once, every word resolved +and checked for `TRANSFER`, the receiver's free slots counted exactly by the crate's new `free_slots()` (a +retired slot is neither free nor live), and only then any move. A failure moves nothing, completes the +sender with its status and leaves the receiver waiting. **Rejected:** removing the capabilities at entry +into the sender's TCB — in-flight state per thread, and a refused delivery could not restore their slots. + +## 6. Handles in one register + +RFC-0003's `Handle` — a `u32` index and a 64-bit generation — fits no register. The ABI word is +**`slot_generation << 20 | index`**: 2^20 slots, Linux's default `fs.nr_open` (1,048,576); 2^44 slot +generations, about two hundred days of one close-and-reopen per microsecond on one slot. **Word `0` is +never live**, because `Generation::FIRST` is 1: it is the null handle. Separately, **the width is the +invariant RFC-0003's amendment asked to be stated:** only the slot generation crosses the ABI, bounded at +2^44 − 1; a slot whose next generation would pass it retires through the crate's `Retired` state, never +wrapping. Object generations stay in kernel memory at 64 bits. Rights travel in RFC-0003's bit order — +`DUPLICATE` 0, `TRANSFER` 1, `READ` 2, `WRITE` 3, `REVOKE` 4 — and RFC-0005's `EXECUTE` 5, pinned in `abi` +by a `const` assertion. **Rejected:** two registers per handle (halves the budget); 32/32 (seventy minutes +at the same rate); a 16-bit index (too few for server workloads). + +**The crate changes, as one dated RFC-0003 amendment** logged in `docs/CHANGELOG.md`, so the width lives +in RFC-0003: `Handle::to_word`/`from_word`, `MAX_SLOT_GENERATION`, a `const` bound of `N` by 2^20 and +`free_slots()` (§5); later, with destruction (increment 14), a split so a destroyed object reports +`ObjectDestroyed` rather than the holder's own use-after-close as `StaleGeneration`. + +## 7. The error model + +**Transport status** (`x0`/`rax`) is what the syscall layer found, identical for a kernel object or a +server. Every failure is atomic. The detail register names the culprit: 0 the invoked handle, 1–4 a handle +word in MR0–MR3, 5–7 `caps[0..2]`, 8 the tag, 9 the reply handle, 10 the IPC buffer. + +| # | Status | Meaning | +|---|--------|---------| +| 0 | `Ok` | done | +| 1 | `InvalidSyscall` | no such number — a closed error, not a fault: the surface stays total | +| 2 | `InvalidArgument` | a reserved bit, a length over 64, a non-zero `svc` immediate, an undefined rights bit, `tag.caps` on a method, a bad buffer address | +| 3 | `InvalidHandle` | word 0, index out of range, empty slot, stale slot generation: the handle names nothing *of yours* | +| 4 | `Revoked` | the slot is live but its object was destroyed (from increment 14; nothing is destroyed before it) | +| 5 | `WrongType` | live handle, wrong kind of object | +| 6 | `InsufficientRights` | lacking the right the operation needs | +| 7 | `TableFull` | a moved capability found no free slot in the receiving table; nothing moved | +| 8 | `WouldBlock` | `nb_send` or `nb_recv` found no partner | +| 9 | `PeerGone` | the object or party waited on went away, or a `reply` found its object unbound | +| 10 | `BudgetRefused` | a `call` whose context can never meet the endpoint's `min_budget`, or a `send` — which donates nothing — to an endpoint that has one | +| 11 | `BudgetExpired` | the donated budget expired inside the server; the kernel completed the wait on the reply object | +| 12 | `NoBuffer` | the syscall needs an IPC buffer the thread does not have | + +`BudgetRefused` follows RFC-0006 (proposed) §7, which refuses only a context that can *never* pass — its +amendment A2 to RFC-0004's "refused up front"; the status stands either way. **Method results** (the reply +label) share one vocabulary for kernel and server, so a stand-in reports errors alike *(seL4's reply +label)*: the numbers above, then 13 `InvalidMethod`, 14 `PoolExhausted`, 15 `Fragmented` (RFC-0005) and 16 +`WindowClosed` (§8). + +**Faults** — EL0 exceptions that are not syscalls — are not return values: the thread is suspended and a +fault message goes to its `fault_ep` (RFC-0006 §4), so a supervisor can restart a driver (O-17). +**Interim, until increment 11:** the kernel prints one line (thread, `ESR`, `ELR`, `FAR`) and leaves the +thread `Inactive`. **Its cost:** an **ambient output channel** — a thread holding no Console can put two +chosen words on the operator's line by faulting, once per thread it can create, each line about 100 bytes +of kernel UART time. It builds only under a `report-user-faults` feature `xtask` enables for Phase-1 +boot-tests and `run-qemu`, and it qualifies the O-4 and O-9 rows (§14). + +## 8. The Process object and spawning (O-27) + +A **Process** holds one RFC-0003 table, one AddressSpace (RFC-0005) and its threads (RFC-0006) — a real +object *(Zircon)*, not seL4's thread naming a CSpace and VSpace. For first authority, **A — inherit** +*(Unix `fork`/`exec`)* is **rejected** by O-27 by name; **B — one bootstrap handle** *(Zircon's +`zx_process_start`)* makes a parent serve its child a protocol over an unbuffered rendezvous before the +child can act; **C — explicit grants before start** *(seL4's root task writing a child's CSpace)* is the +**verdict sought**. `process_create` **binds its AddressSpace for life** — one already bound is refused, so +two tables never share one memory (O-8) — and the Process is born with an **empty table** and no thread. + +| Method | Right | Effect | +|--------|-------|--------| +| `GRANT` | `WRITE`; `TRANSFER` on each moved capability | before the first `resume` only: move up to three capabilities in, all or nothing; the reply carries their handle words *in the child* | +| `KILL` | `WRITE` | stop every thread, drop the table, release the address space; the generation bump makes every capability to the process inert | +| `INFO` | `READ` | live capabilities in the table; threads not `Exited`; whether the window is open | + +**The grant window** closes at the first `resume` of any of its threads, which RFC-0006 reports by +flagging the Process; `GRANT` then answers `WindowClosed`, and authority arrives only by IPC, which the +process consents to by receiving. It is **single-use** in research/0002's sense (Part 3, after Vault's +response-wrapping) but lacks **prior-use detection**, which is the broker RFC's. + +**What the window closes, exactly: capability injection.** Once started, no holder of the Process +capability adds to its table, and `WRITE` on it means `KILL` alone, so a supervisor can hold kill-and- +inspect authority without the child's power (O-17). It does **not** close **control**: `WRITE` on the +child's AddressSpace maps into it and, beside `WRITE` on the Process, creates threads in it; `WRITE` on a +Thread rewrites its registers (RFC-0006 §4). That is authority over the child's code and data, which its +loader always had — and why thread creation presents the AddressSpace: a Process capability alone cannot +start code in a child. + +**The spawn protocol**, encoded and host-tested in increment 9's loader plan: the spawner never maps the +child's writable memory into itself — data arrives by `region_copy` (§10); before `resume` it grants the +child whichever of its AddressSpace, Thread and Region capabilities the child needs, closes the rest, and +keeps only the Process capability. A spawner that derived copies first keeps control; the kernel cannot +tell, and the child cannot yet check (Open question 3). + +**Lifetime.** A Process ends by `KILL`, or when no capability names it and none of its threads can run +again. One whose threads have all `Exited` is dead but intact, inspectable through `INFO` until then +*(seL4: objects live until destroyed)*. **Rejected:** ending with the last thread *(Zircon)* — undefined for +a newborn, and it destroys what a supervisor would inspect. The spawner passes handle words in `a0` and +`a1` (the demo's Console and endpoint), or a start Region in `a0` — a runtime convention, not kernel ABI. + +## 9. The root task and boot info + +The one act the kernel performs unasked: at boot it builds **exactly one** process from the first boot +module and gives it every boot capability *(seL4's root task; research/0002 Part 3, "the bootstrap seam is +a one-time kernel act")* — an AddressSpace, the segments mapped as in §10, a stack, a read-only +**BootInfo** page, a Process and a Thread in §3's entry state with `a0` = BootInfo's address and `a1` = 0. +Its priority, ceiling and full context are RFC-0006 (proposed) §6's one bootstrap act. + +**BootInfo**, in `user/abi`, is a header (magic, version, length), one `#[repr(C)] BootCap { kind: u32, +flags: u32, handle: u64, base: u64, size: u64 }` per initial capability, and a string table for module +names, pinned within a page by a host test. Every initial capability is *listed*, none at a well-known +slot, so a reviewer can enumerate the whole grant. Kinds: the root's Process, the Console (§11), a +read-only Region per further module with its descriptor; RFC-0005 adds the AddressSpace, the one root Pool +and the DTB; RFC-0006 the Thread, a `SchedControl` per core and the `IrqControl`. Kinds appear as built. + +**The root is not a superuser.** Its capabilities are ordinary, droppable and generation-checked, and **no +kernel code branches on "is this the root task"**. They are **not revocable** until RFC-0003a, though +research/0002 Part 3 asks for revocable init capabilities. **Rejected:** a kernel boot manifest (policy in +the kernel); a `spawn_from_module` syscall (a loader as a kernel service); a `system:masters` superuser. + +## 10. Getting the first images into memory + +**Verdict sought — the mechanism:** the kernel reaches modules through `arch::boot_modules()`, which yields +fixed-shape **load descriptors** made on the host, and **never parses ELF**. A dependency-free, host-tested +ELF64 reader in `xtask` emits an entry point; text (`R+X`), optional read-only (`R`) and data (`R+W`, +zero-padded to a page, with a `bss` size) segments, page-aligned in the user half; and stack and BootInfo +addresses. It **refuses** a writable-and-executable, overlapping or unaligned `PT_LOAD`, `PT_DYNAMIC`, +`PT_INTERP`, `PT_TLS`, `PT_GNU_RELRO` and an executable `PT_GNU_STACK`, ignoring `PT_NOTE` and a +non-executable `PT_GNU_STACK`; `user/link/.ld` declares `PHDRS` so lld emits no other. W^X is checked +before the image exists (O-13), and the kernel validates one fixed structure — Nexen's finding that kernel +code validating structures built elsewhere is the bug farm (research/0002 Part 7). **Rejected:** an +in-kernel `elf/` crate, a parser in the TCB for no gain. + +**The source — an AArch64 interim: embedded in the kernel image.** QEMU's `-initrd` and `-device loader` +add a second, QEMU-only artefact (`hw/arm/boot.c`, read at QEMU 8.2.2 and to be re-read at the pinned +11.0.3, loads `-initrd` only for Linux images); children linked into the root's ELF *(seL4's CPIO +archive)* would tie the root to each image. So `xtask` writes `payload.bin` — a versioned header, then per +module a name, descriptor and segment bytes — named by `SETONIX_PAYLOAD`; `kernel/build.rs` re-runs on that +variable and substitutes an empty bundle when it is unset, so a bare `cargo build` prints `boot modules: +0`. A `global_asm!` `.incbin` under `kernel/src/arch/aarch64/` embeds it; `aarch64.ld` places it in a +page-aligned, read-only, `KEEP`ed `.payload` section *(Hubris's `xtask dist`)*. **Cost:** a user change +relinks the kernel. **On x86_64**, a future x86_64 boot RFC provides the UEFI stub that loads the same +bundle as a file; increment 12 depends on it. + +**Loading.** The kernel loads **module 0 only**; the others reach the root as **read-only Regions** +(RFC-0005 §7) with descriptors in BootInfo *(Genode's core hands init boot modules read-only)*. Every +loader, kernel or root, maps text `RX` and read-only data `R` **in place**, copies data pages into a fresh +Region with `region_copy` — which RFC-0005 (proposed) provides as a page-granular, frame-to-frame copy, the +one it already makes for the root (§7 there), so the demo needs that half of its copy module — and takes +`bss` as fresh zeroed pages, so no loader maps a child's writable memory into itself. The programs are soft-float `no_std` crates on `abi` alone with no `unsafe`; +on `x86_64-unknown-none` `xtask` passes `-C relocation-model=static -C code-model=small`. + +## 11. The console as a capability + +Userspace reaches the kernel's UART only through a **Console** object with one method, `WRITE`: the byte +count in MR0, at most 24 bytes in MR1–MR3, sent verbatim (`abi`'s writer supplies `\r\n`). **It never +waits:** the kernel stores bytes while the PL011's transmit-full flag is clear and returns the count +accepted, and `abi` yields and retries the rest, so any waiting happens at EL0, preemptibly. The hold is at +most 24 flag reads and 24 stores, inside RFC-0006 (proposed)'s measured worst path, so the console sets no +floor under `MIN_BUDGET` and needs no preemption point. The root receives it with `DUPLICATE | TRANSFER | +WRITE` (no input path, so no `READ`) and derives `WRITE`-only copies for chosen children; a program not +handed one cannot print, but for §7's interim. **Rejected:** seL4's `DebugPutChar`, any thread's in a +`CONFIG_PRINTING` build; a console at a well-known handle. **Adopted in spirit:** Zircon's write-only +debuglog. Once a userspace UART driver exists the root hands out an endpoint speaking `WRITE`, no client +changes, and the Console object is **deleted** (increment 13). + +## 12. `user/abi` — the kernel's own binding + +**Which ledger row.** The libc/runtime row ("port code — relibc pieces") gives a program an environment +and issues no syscalls: relibc sits on `redox_syscall`, versioned with the Redox kernel, and seL4 keeps +libsel4 in its kernel's repository. The binding is the user half of §3's table, with nothing to port. +**Verdict sought: the microkernel-core row, write ourselves**; anything that would read the same on +another kernel moves out. Appending "syscall ABI binding (`user/abi`)" to that row is constitution text, +the maintainer's (Constitution §4, logged in `docs/CHANGELOG.md`); increments 2 and 7 wait on it. `abi` +holds the numbers, `Handle`, `Tag`, `Status`, labels, `BootCap`, the layouts with `const` assertions and +safe wrappers — no allocator, no formatting. The kernel and `xtask` build it without its `syscalls` +feature, the one that compiles `src/arch/**`, so all three share one data half. + +**The third designated `unsafe` tree**, approved in principle on 2026-09-27, is `user/abi/src/arch/**`, +holding only the `svc`/`syscall` wrappers, the discovery-register read and the entry stubs. `root_start` +copies the BootInfo page by volatile reads onto its stack and hands `main` a reference to the copy — sound +because the kernel mapped the page read-only before the process's first instruction and nothing else has +run; `child_start` passes `a0` and `a1`. User programs contain no `unsafe`, and no Rust reference is formed +into memory another thread may write. **Sought separately, not for the demo:** volatile IPC-buffer word +accessors in `user/abi/src/buffer/**`, whose invariant — the buffer stays mapped at its bound address while +the thread runs — the process itself upholds; broken, it faults that thread and touches no other process. + +**The edits, all in increment 7:** `CLAUDE.md` § `unsafe` policy gains "`user/abi/src/arch/**` — trap +instructions and process entry stubs" and § Layout gains `user/`; threat-model O-6 names three trees; the +`Cargo.toml` comment ("the two trees") and `kernel/src/main.rs`'s grep widen to the repository; and +`xtask/Cargo.toml`'s "No dependencies" becomes "no external dependencies". + +## 13. Lineage + +Named inline. Mostly **seL4** (root task, invocation as IPC, `extraCaps`, reply objects, transfer at +rendezvous; not CNodes, `DebugPutChar` or 120-word messages) and **Zircon** (the process object, debuglog; +not a syscall per operation), with **Linux**, **Hubris**, **Genode** and **Redox** for smaller pieces. + +## 14. Obligations + +| Obligation | This RFC | Status after implementation | +|-----------|----------|-----------------------------| +| O-1 unforgeability | handles reach the kernel only as words resolved through the caller's table; word 0 and out-of-range indices fail closed (§6) | **binds at B1** — RFC-0003's mechanism made live | +| O-2 non-widenability | `cap_derive` is the only duplication and is subset-only; presented handles move nothing; moves never widen (§4, §8) | **binds at B1** | +| O-4 no ambient authority | twelve syscalls, each handle-indexed or authority-free; methods take handles; console by capability (§4, §11) | **discharged at the ABI, except the fault-report interim** (§7) until increment 11; each new method checked at review | +| O-5 argument validation | no pointer arguments; reserved tag bits zero; single fetch at rendezvous; transfers all-or-nothing; kernel-built `SPSR_EL1`; `sysretq` guards (§3, §5, §7) | **discharged for the syscall surface**, with RFC-0005 §11 for user memory | +| O-6 kernel memory safety | a third designated tree, trap instructions and entry stubs only; threat-model O-6 names it (§12) | **stays Built**, with a repository-wide grep | +| O-7 no unprivileged exhaustion | 512-byte copy bound; creation paid by a named Pool; reusable reply objects; fixed tables fail closed; a console that never waits (§4, §5, §11) | **contributes** — RFC-0005 owns the accounting | +| O-9 no ambient side channel | result registers carry results or zero; no grant after start; no ambient console (§3, §8, §11) | **contributes**, except the fault-report interim (§7) | +| O-13 W^X | the build refuses writable-and-executable segments; loaders map per descriptor (§10) | **contributes** — RFC-0005 owns enforcement | +| O-17 contained drivers | fault messages to `fault_ep`; `KILL`-only authority over a started Process; dead processes inspectable (§7, §8) | **designed, deferred** — the interim stops the thread | +| O-27 explicit authority at spawn | empty table at birth; grants only by explicit move before start; root's grant enumerated; a host test and a boot-test count the child's table (§8, §9, §18) | **discharged** in its letter; the spawner's retained control is named (§8), not claimed away | + +## 15. Graves checked (§3) + +- **Policy in the kernel.** The kernel runs one image and lists what it granted; the rest is the root's. +- **The catch-all right.** No root identity survives `eret`; no right is added. A Process capability reaches + its table only through `GRANT` before start, then means `KILL`; control of a running child lives in + separate AddressSpace and Thread capabilities, each droppable. +- **Baroque hierarchies; multi-copy IPC.** Flat handles, no receive window, a flat BootInfo; one copy. +- **Bolted-on multicore.** Entry is per-core from the first stub (`SP_EL1`, `TPIDR_EL1`; `swapgs`). + RFC-0006 (proposed) §12 provides the big kernel lock taken on entry, answering RFC-0003 §14.2; single + fetch stays necessary under it, because other threads write the buffer from EL0 without the lock. +- **Drivers pulled in; unused device paths.** The Console alone is reachable from EL0, bounded, its + deletion scheduled. + +## 16. Costs — what this makes harder + +- **`call` is overloaded** — per-type method decoding and two error layers, the price of interposition — + and **interposition is partial:** a forwarder for a method with handle-word arguments must first be handed + those capabilities, costing the client a `TRANSFER` it may not hold (input to RFC-0003a). +- **Four physical registers and 64 words:** past 32 bytes a message touches memory, a 65–120-word message + seL4 would copy needs a Region here, and raising either later breaks binaries. +- **Handles are 20/44 for good,** the accepted crate changes by amendment, and `TPIDRRO_EL0` and the user + GS base belong to the ABI rather than a runtime. +- **A spawner keeps control if it wants to:** the window stops injection, not a loader that kept derived + copies of the child's AddressSpace or Threads, and the child cannot yet check. +- **The root is the most sensitive process,** as in seL4, and not revocable until RFC-0003a; it must stay + small. **No ambient printing; late grants need a willing child; every console writer loops** on short + 24-byte writes. **No PAN on the demo CPU;** `user/abi` is a third `unsafe` tree to audit. + +## 17. Open questions + +1. **Fault messages and death** — their layout (this RFC's), how a supervisor learns a process died, and + how it supervises threads a child creates itself (RFC-0006 §4); likely a notification bound at creation. +2. **Badges** — `cap_derive`'s badge word is reserved zero until RFC-0003a; notification signals then carry it. +3. **A sovereignty check** — should RFC-0005's AddressSpace query report its live-capability count, as + RFC-0006's `ctl_info` does for `SchedControl`, so a child can confirm it holds the only one? +4. **The Language clause** — do single-instruction `svc`/`syscall` wrappers and entry stubs in userspace + fall within "minimal assembly … for boot and context switching", as RFC-0005 §17.7 asks for `TLBI`? +5. **The 64-word budget** — a verdict now, to be revisited with the first measurements. + +## 18. Implementation increments + +Each is one reviewable PR; **[demo]** marks what the Phase-1 demo needs. Userspace boot-tests expect +prefixed strings, since bare `Kaya!` matches the kernel's greeting; every demo line fits one `WRITE`. + +1. **[demo] `capability`: the handle word**, `free_slots`, with RFC-0003's amendment. Host tests: round + trips; word 0 and index ≥ 2^20 refused; retirement at the bound; `free_slots` exact beside retired slots. +2. **[demo] `user/abi`, data half**, after the ledger verdict, no `unsafe`. Host tests refuse every + reserved-bit (tag bits 9–15 included) and over-length encoding; CI builds both targets. +3. **[demo] AArch64 trap path, MMU off** — one kernel-held frame (RFC-0006's increment 4 moves frames into + TCBs), dispatch, `eret`; `yield`, `thread_exit`, `InvalidSyscall`; an EL0 fault stops the self-test, not + the kernel: `--features syscall-selftest --expect "syscall round trip"`. **Deleted** by RFC-0005's 9. +4. **[demo] `xtask`: repeated `--expect`, matched in order**, host-tested. +5. **[demo] The bundle** — the ELF reader, host-tested on W+X, overlapping, truncated, `PT_TLS`, `PT_DYNAMIC` + and executable-stack fixtures; `build.rs`, `.incbin`, `.payload`: `--expect "boot modules: 0"`. +6. **[demo] Objects, `cap_*`, the dispatcher, the Console and the Process's kernel half** (create, `INFO`) + on RFC-0005's store and root Pool, with its 14: an EL0 self-test in a kernel-built process prints + through a Console handle, `--features syscall-selftest --expect "[el0] Kaya!"`. +7. **[demo] The root reaches EL0** — `user/abi/src/arch/**` and every §12 edit in one PR, once the tree is + approved; module 0 becomes the root: `--expect "boot modules: 2" --expect "[root] up"`. +8. **[demo] `GRANT`, the window, `INFO`, `KILL`** in a host-tested `process/` crate, then wired: born empty; + `GRANT` all-or-nothing; `WindowClosed` after the first resume; an AddressSpace bound once. +9. **[demo] The root spawns the client,** in three PRs: + - **a.** A host-tested `no_std` `user/loader` crate: descriptor in, method calls out, W^X and overlaps + refused; a host test that the spawner ends holding only the Process capability. + - **b.** The root runs the plan, granting a `WRITE`-only Console and a send-only endpoint: + `--expect "[root] up" --expect "[client] up"`. + - **c.** O-27 evidence: the client probes indices 0–63 at generation 1 with `cap_rights` (exhaustive + while no slot has been vacated), printing `[client] 2 handles`, and the root prints `INFO`'s count, + `[root] client: 2 caps`. Evidence, not proof: the proof is increment 8's host test. +10. **[demo] IPC syscalls** over RFC-0004 endpoints, reusable Reply objects and RFC-0006's blocking states: + `[client] -> Kaya!`, `[server] <- Kaya!`, `[client] <- Kaya!` in order. Host test: clients that exit + mid-call leave the server's Pool balance unchanged. +11. **Fault messages and death notification** (§17.1): the root prints `[root] child faulted`, and + `report-user-faults` leaves the boot-tests. +12. **x86_64 trap path and `abi` stubs** (`EFER.SCE`, `LSTAR`/`STAR`/`FMASK`, `swapgs`, the `sysretq` + guards), after the x86_64 boot RFC's UEFI stub: the demo boot-tests on `q35`. +13. **Delete the Console object** when the Phase-2 UART driver lands. +14. **`Revoked`**: the crate's `ObjectDestroyed` split, with RFC-0005's destruction (its 17). +15. **The root spawns the server** and stops serving, removing that interim. + +**Demo order across the three RFCs,** for the maintainer to fix: RFC-0005 1–8, RFC-0006 1–2 and this +RFC's 1, 2 and 4 in any order → 3 → RFC-0006 3–4 → RFC-0005 9–10, retiring the MMU-off self-tests → +RFC-0005 11–14 → RFC-0006 5 → 5–6 → 7 → 8 → RFC-0006 6a–6b → 9 → RFC-0006 7a–7b → 10 with RFC-0006 7c. +RFC-0006 puts its 3–4 before RFC-0005's MMU and RFC-0005 after; this takes RFC-0006's, with RFC-0005's 10 +repointing the GIC, as RFC-0005 allows. + +**The demo's interims, with their costs:** + +- **Faults print and stop** (§7): an ambient output channel and ~100 bytes of kernel UART time per fault. +- **The in-kernel Console** (§11); **modules in the AArch64 image** (§10), relinking the kernel per change. +- **One root Pool, no destruction** (RFC-0005): charges unattributed, `KILL` releases nothing, no `Revoked`. +- **Register-only messages** (RFC-0005's IPC-buffer module, its 16, is not demo): no thread has a buffer + and no capability crosses an endpoint; the demo's grants use `GRANT`, whose words are registers by design. +- **An active server** (RFC-0006's A1), so RFC-0004's donation is not exercised; **the root doubles as + server**, running client-facing code in the process holding every boot capability, until increment 15. +- **The MMU-off self-test** (increment 3); **RFC-0006's provisional constants** for the root's scheduling. + +## 19. What this unblocks + +The first userspace, and every Phase-2 paper: the **scheme registry** and **broker** (processes, grants, +`call`), the **driver framework** (faults, interrupt notifications, the console moving out), a **relibc +port** over `user/abi` with both TLS registers its own, and the **x86_64 bring-up**. RFC-0003a gains an ABI +and two inputs: partial interposition (§16) and the sovereignty check (§17.3).