docs: prior-art review — validate the spine, prune one legacy, correct RFC-0004 - #10
Merged
Conversation
"Keep the proven, prune the legacy" turned into an actual audit. Three
research passes against the systems that already fought these fights —
seL4, Zircon/Fuchsia, KeyKOS/EROS, Barrelfish, CHERI, Genode, QNX, L4, and
the Rust-OS field (Tock, Hubris, RedLeaf, Asterinas, Theseus, Redox) —
recorded in docs/research/0001 with a primary source for every claim.
Verdict: both RFCs' spines are validated and correctly cited. The flat
capability table is the 60-year-old C-list; subset-only rights and
no-ambient-authority are textbook; §9 is the direct cure for Hardy's
confused deputy; synchronous rendezvous is still the fast-microkernel
consensus, corroborated by Hubris in production. Three bounded corrections:
- PRUNE: RFC-0004 §5's page-mapping large transfer is L4's "long IPC",
removed by seL4/NOVA/Fiasco.OC and hostile to verification. (Folded
into RFC-0004 separately.)
- ADOPT: first-class one-time reply objects (seL4 MCS), virtual message
registers, priority-aware direct switch / scheduling-context donation,
seL4 badges by name.
- DECIDE: RFC-0003's revocation deferral is a decision RFC-0003a must
make, not a deferral it may keep — §6's broker-bypassing TRANSFER makes
broker-mediated revocation unreachable, and one-level links cannot do
multi-level transitive revoke.
This commit lands the research note and the RFC-0003 amendment (spine
holds; revocation upgraded to a decision; per-client eviction named a
day-one gap; §6's compile-time claim scoped to kernel-internal, since the
borrow checker cannot span protection domains — RedLeaf's own group proved
this). RFC-0004's revisions and the Constitution §3 reword are handled
separately (the latter flagged, not taken — §3 is the maintainer's).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
# Conflicts: # docs/CHANGELOG.md
The prior-art review's IPC findings, applied to RFC-0004 (still Proposed).
Four corrections, each tracing to a cited source in docs/research/0001:
- §5 no longer maps the sender's pages into the receiver during a message.
That is L4's "long IPC" — removed by seL4, NOVA and Fiasco.OC on
minimality grounds and, decisively for a verification-minded kernel,
because a page fault during the in-kernel copy introduces concurrency
that makes the kernel far harder to reason about. Bulk data now travels
through a shared Region capability established out of band, with IPC
carrying only a small descriptor; the in-message slow path is a bounded
small copy (seL4-IPC-buffer sized). This is the single most valuable
finding of the whole review: we had reinvented a legacy mistake.
- §5 fast path uses virtual message registers (seL4) rather than a
hard-committed physical x0-x7 set — the rigidity L4 engineered away —
and the ~100-cycle figure is reframed as software-logic overhead, not a
round-trip RPC (real one-way IPC is ~190-320 cycles on cited hardware).
The fast path is also stated to be capability-transfer-free by design:
a cap-carrying message leaves the register path.
- §4/§8 direct switch is priority-aware, and call is framed as
scheduling-context donation (migrating threads -> QNX priority
inheritance -> seL4 MCS). The review found the real synchronous-IPC
hazard is scheduling coupling, not deadlock; a client timer capability
cannot fix a server monopolising the caller's budget, only donation can.
This couples IPC to the scheduler RFC earlier than the draft implied.
- §8 reply is a first-class one-time object (seL4 MCS), destroyed on
caller death, with the withheld-reply denial (Shapiro 2003) named and
answered by the userspace watchdog.
Folded into this PR rather than a separate one because merging main
(RFC-0004 landed via PR #9) already brought RFC-0004 onto this branch and
resolved the changelog here; a second PR would only re-conflict on the same
changelog region. The RFC keeps its Proposed status — these are revisions
to a proposal, and the maintainer's verdict on the corrected design is
still owed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
MatejGomboc
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
You asked us to research the capability and IPC designs against real OSes and the literature. Three research passes (seL4, Zircon/Fuchsia, KeyKOS/EROS, Barrelfish, CHERI, Genode, QNX, L4, and the Rust-OS field), one primary source per claim, in
docs/research/0001.Verdict: both RFCs' spines are validated (the flat table is the 60-year-old C-list; §9 no-ambient-authority cures Hardy's confused deputy; synchronous rendezvous is the fast-microkernel consensus, shipped by Hubris). This PR lands the research note and every correction it forced:
Prune (a legacy we nearly re-adopted)
Regioncapability out of band + small descriptor over IPC; bounded small copy for the rest. (The single most valuable finding.)Adopt (proven refinements — folded into RFC-0004)
callas scheduling-context donation — the real hazard is scheduling coupling, not deadlock.Decide (RFC-0003 amendment)
TRANSFERmakes broker-mediated revocation unreachable; one-level links can't do multi-level transitive revoke; per-client eviction named a day-one gap.The slogan "Rust's ownership models capability transfer at compile time" overreaches (the borrow checker sees one compilation unit — RedLeaf's own group proved ownership types can't span protection domains). Recommended reword in the changelog + RFC-0003 amendment. Flagged, not taken — §3 is yours.
What this PR contains
docs/research/0001-…— the full literature review (3 parts + synthesis).RFC-0004 keeps Proposed status — your verdict on the corrected design is still owed.
unsaferegisterunsafeblocks: None — documentation only.Checklist
docs/threat-model.mddocs/CHANGELOG.mdupdated; conflict with main resolved🤖 Generated with Claude Code