docs: RFC-0005, RFC-0006, RFC-0007 (WIP — under review, do not merge)

[MatejGomboc]

Pull Request

Summary

This adds two foundational RFCs to the design record: RFC-0005 specifies the memory management subsystem (address spaces, physical memory, frame allocation, and W^X enforcement), and RFC-0006 specifies the threading and scheduling model (the event kernel, scheduling contexts as capabilities, priority dispatch, and budget donation). Together they discharge O-7 (resource accounting), O-8 (memory safety), O-13 (W^X), and answer open questions from RFC-0003 and RFC-0004.

Explanation for the maintainer

These two RFCs form the load-bearing layer between the capability model (RFC-0003) and the IPC mechanism (RFC-0004), and between the abstract design and the concrete system calls (RFC-0007, proposed). They are tightly coupled — RFC-0006 depends on RFC-0005 for kernel stacks and object memory, RFC-0005 depends on RFC-0006 for the scheduler's own structures — and were drafted together as a coherent whole.

RFC-0005 (Address spaces and physical memory) establishes:

• Physical memory discovery from firmware tables (DTB on AArch64, UEFI on x86_64) into a bounded MemoryMap
• A bitmap frame allocator with colour support, every frame zeroed before userspace sees it
• Typed fixed-capacity slot arrays as the object store, with Pool as the accounting layer (O-7)
• A unified virtual layout on both architectures: 47-bit user and kernel halves, a non-executable physmap, guarded kernel stacks
• Three new objects: Region (memory), AddressSpace (page tables), and Mapping (records, not capabilities)
• EXECUTE as a new right (bit 5) on RFC-0003's set, meaningful only on Regions and Pools
• W^X enforcement in four layers: unrepresentable in the type, per-Region across all address spaces, per-Pool at mint time, and hardware-backed by SCTLR_EL1.WXN
• Sharing and donation as derive-and-transfer, with reissue as the destruction-case operation that tears down all mappings
• The invariant that the kernel never dereferences a user virtual address (O-5)

RFC-0006 (Threads and scheduling) establishes:

• An event kernel (one kernel stack per core, non-preemptible, every wait is a thread state) as the load-bearing choice
• A Thread object with nine states, a fixed-size TCB, and authority-free yield and exit
• SchedContext as an object holding budget, period, and refills — time as a capability (O-4)
• A Core object, one per core, minted to the root task, as the authority to sell time on that core
• 256 fixed priority levels with O(1) bitmap run queues and FIFO endpoint queues
• Priority inheritance on call to passive servers at max(own, caller's) priority
• Budget donation and the 2026-08-01 amendment: thresholds on endpoints, one-hop BudgetExpired on exhaustion, timeout faults for stranded servers
• Tickless one-shot deadlines: AArch64 EL1 virtual timer, x86_64 LAPIC (TSC-deadline with invariant TSC, else one-shot)
• FP/SIMD enabled per thread, loaded on first use, saved lazily by owner tracking
• GICv3 interrupts first, with device lines as IrqHandler objects that signal notifications
• Per-core state with a big lock for SMP, cores parked until funded, SMT placement classes

Both RFCs are proposed verdicts awaiting the maintainer's decision. They are written as design records, not specifications: they state the mechanism, not the policy. They discharge commitments from RFC-0003 and RFC-0004, answer open questions those RFCs left, and establish the invariants the system calls (RFC-0007) and the HAL will rely on.

The RFCs are complete

https://claude.ai/code/session_01D1gBBT3tN99wzeJjf3tLWW

[MatejGomboc]

CI red on f94bd19: known, and this PR's to fix. Checks (pins, spelling, fmt, clippy, markdown) fails on markdownlint MD013 (line length > 170). The seven offending lines are 17–24 of docs/rfcs/0005-address-spaces-and-physical-memory.md, in the RFC's verdict box. I've reproduced it locally with markdownlint-cli2 0.23.1; spelling, fmt and clippy are clean.

The file is still being revised by the drafting workflow, so it will be rewrapped in the final pass rather than now, which would mean racing the reviser's edits. This PR is a draft of work-in-progress snapshots and cannot merge in this state. Before it's marked ready, the final pass will run the full CI suite locally on the finished text.

---

Generated by Claude Code

[MatejGomboc]

Hand-off: paused 2026-09-27, ~17:10 CEST (credits)

State: three proposed RFCs, each drafted twice (once by Opus 5.5, once by Fable 5.1), blind-judged by two judges, synthesised, reviewed through three lenses (constitution, technical correctness, implementability) and revised. Head 4cbc926. Markdownlint and British spelling are clean locally. Not mergeable yet: the three were revised in parallel and have not been cross-checked against each other, and there are known seams (below). Keep this PR a draft until that pass is done and the maintainer has given his verdicts. There is no code in this PR; the Phase-1 demo was not started.

RFC	Lines	Verdicts	Review findings	Duel (both judges agreed)
0005 Address spaces and physical memory	461	13	55, 0 blockers	Opus won, 49–44 / 50–47
0006 Threads and scheduling	480	12	62, 2 blockers (addressed in revision)	Opus won, 45–42 / 47–46
0007 System calls and process bootstrap	500	13	48, 3 blockers (addressed in revision)	Opus won, 51–43 / 47–44

The verdict boxes at the top of each RFC are the twenty-minute read.

Next session, in order

1. Cross-RFC coherence pass over 0005/0006/0007 (/check-coherence docs/rfcs/0005* docs/rfcs/0006* docs/rfcs/0007*). Known seams:
   • Increment order: 0006 wants its timer increments with the MMU off; 0005 orders them after MMU-on. 0007 proposes a merged order.
   • region_copy: proposed in 0007 but belongs to 0005's domain.
   • Moving a capability into a kernel object needs TRANSFER: 0007 says it always does, but 0006 §4's row names only WRITE.
   • Reply objects: "destroyed" (RFC-0004) vs "unbound" (0007's amendment).
   • Accounting pointer: 0005's open question 2 should point to 0006's decision to keep memory and time accounting separate.
   • Wording: 0007 §18 should say "the single root Pool" for its interim.
2. Add docs/CHANGELOG.md entries for the three RFCs. Each workflow drafted one; they were not kept in the repo.
3. Verify the unverified. Each RFC lists claims it could not check: RFC-14 threshold figures (seL4/rfcs PR 24), Arm ARM section numbers (the manual was unreachable), and QEMU hw/arm/boot.c at 11.0.3.

Decisions only the maintainer can make (full lists are in each RFC's Open questions)

• Amendments to accepted RFCs:
  • 0006 A1: a call to an active server donates no time (seL4 MCS). This contradicts RFC-0004 §4/§8, and the demo relies on it.
  • 0007: reply objects become reusable (RFC-0004).
  • 0007: the handle-word encoding, a 44-bit slot generation bound (RFC-0003).
  • 0005: EXECUTE as a new right, bit 5 (RFC-0003).
• §11.1 "minimal assembly": do single-instruction asm! helpers count, meaning the TLBI/DC/IC/TTBR writes in arch/ and the svc/syscall wrappers in user/abi? Or does the clause need amending?
• Borrow Ledger: is user/abi part of the microkernel-core row? And its src/arch/** as a third designated unsafe tree, now narrowed to trap wrappers and entry stubs.
• Threat model §10: add "firmware tables describe memory truthfully" as an assumption.
• Departure from research/0002 Part 6: budgets are enforced as caps, not minima. A guaranteed minimum is admission policy.

x86_64 boot findings (input for a future RFC-0008)

• CLAUDE.md says "q35 has no bare-ELF equivalent of -kernel". That's wrong: QEMU has accepted an ELF64 with a Xen PVH note since v4.0, and a probe kernel printed Kaya! on q35 under QEMU 11.0.3 using only files from QEMU's own install.
• Recommended: PVH now, with a UEFI stub later as a second front end, both feeding one kernel boot-info record. Multiboot is rejected: QEMU only implements v1, and only for 32-bit images.
• Traps:
  • The x86_64 target defaults to static-PIE, so the 32-bit entry stub needs -C relocation-model=static.
  • The link script needs an explicit PT_NOTE aligned to 4 bytes.
  • The pvh.bin shipped with QEMU dates from 2019, so the RSDP pointer always arrives as 0. The kernel must scan for the RSDP itself.
  • The PVH start_info data sits in RAM marked usable, so copy it before the frame allocator runs.
• QEMU's own install already carries SeaBIOS, qboot and EDK2 for both architectures. The Dockerfile's apt ovmf package could go, but that needs a §7 amendment.

Model comparison, as asked

Opus 5.5 won all three drafting duels, and the Fable 5.1 judges agreed each time. Fable's drafts were often the cleaner read and carried better review aids (bit-position tables, "refused when" columns), and those were grafted in. They also carried design-level errors in exactly the unforgiving places: boot-time page tables that left the UART unmapped, missing barriers in the cache and TLB sequences, an FP/SIMD scheme that reopened CVE-2018-3665, and a syscall ABI with no register for the received tag.

Recommendation: use Opus to draft and decide, and Fable as an adversarial technical reviewer. That split looks promising, but these three duels are the only evidence behind it.

Environment notes

• Local boot-tests used QEMU 11.0.3 built from GitLab tag v11.0.3 (commit aeec49e8). The tag's signature was not verified, because the keyserver was unreachable. download.qemu.org is blocked by this environment's network policy.
• The hourly check-in trigger and the autosave loop are both stopped. The WIP snapshot commits on this branch are backups; squash them as you prefer before merging.

---

Generated by Claude Code