Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
183826d
wip(docs): snapshot RFC-0005 and RFC-0006 drafts mid-review
claude Sep 27, 2026
4c69180
wip(docs): snapshot RFC-0005 and RFC-0006 revisions in progress
claude Sep 27, 2026
79d8583
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
62ec182
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
d93de1d
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
dd53cf5
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
4fc242f
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
f6e05cd
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
f94bd19
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
b5c0154
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
6ba18c6
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
d2029e9
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
9ba399a
wip: autosave 14:40Z
claude Sep 27, 2026
7ad90e8
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
eedc4d6
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
ad537ed
wip(docs): snapshot RFC revisions in progress
claude Sep 27, 2026
28c49a9
docs(rfc-0006): threads and scheduling, reviewed and revised
claude Sep 27, 2026
4cbc926
docs(rfc-0007): system calls and process bootstrap, reviewed and revised
claude Sep 27, 2026
8d9feb0
docs(changelog): record RFC-0005, RFC-0006 and RFC-0007 as proposed
claude Sep 27, 2026
647ff5d
docs(changelog): RFC-0006 was reviewed through three lenses, not two
claude Sep 27, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 45 additions & 0 deletions docs/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading