ADR-0003 makes a shared-memory ring (io_uring-style) the primary high-frequency kernel interface, with the trap reserved for waking idle peers. It's marked contested on purpose — it's the design's biggest bet and the one most likely to be wrong.
The honest alternative is a clean trap-per-syscall interface (seL4-style): smaller, simpler, more verifiable, at the cost of throughput we cannot measure because nothing runs yet.
What I'd love feedback on:
- Does the ring complexity justify itself before there's anything to benchmark?
- TOCTOU / shared-memory attack surface on ARM's weak memory model — is this underestimated?
- Does this tension with the small-TCB goal (ADR-0001) too much?
See docs/adr/0003-ring-based-syscall-interface.md. Disagreement with reasoning is exactly what this issue is for.
ADR-0003 makes a shared-memory ring (io_uring-style) the primary high-frequency kernel interface, with the trap reserved for waking idle peers. It's marked contested on purpose — it's the design's biggest bet and the one most likely to be wrong.
The honest alternative is a clean trap-per-syscall interface (seL4-style): smaller, simpler, more verifiable, at the cost of throughput we cannot measure because nothing runs yet.
What I'd love feedback on:
See docs/adr/0003-ring-based-syscall-interface.md. Disagreement with reasoning is exactly what this issue is for.