Bring the docs up to the M17-M18 reality; pre-settle M19-M20 ambiguities
resilience.md: steps 1-4 of the ladder are built — supervision, exit reasons, restart with backoff, crash-loop caps, all proven by scenario; what remains is scope, not mechanism. README statuses follow. drivers.md gains the driver-contract section (harness, hello, crash-freely). The M19-M20 plan pre-settles three things the loop would otherwise have had to decide alone: the memory-map pass-through for apertures, the manager spawning 'discovery' from M20.1, and hid[8] riding ChildAdded for ACPI string identity until the FDT widening.
This commit is contained in:
+8
-6
@@ -45,20 +45,22 @@ rather than restate it. Roughly in the order things happen at runtime:
|
|||||||
until its hardware interrupts it**. The claim is the capability; `irq_ack` is the
|
until its hardware interrupts it**. The claim is the capability; `irq_ack` is the
|
||||||
unmask.
|
unmask.
|
||||||
14. **[driver-model.md](driver-model.md) — buses, classes and host controllers.** How
|
14. **[driver-model.md](driver-model.md) — buses, classes and host controllers.** How
|
||||||
real driver stacks factor into three shapes, how families share code, and the
|
real driver stacks factor into three shapes and how families share code. The
|
||||||
proposed ABI for the three primitives still missing (capability passing, DMA +
|
three primitives it proposed are long since built (M13 capability passing,
|
||||||
memory barriers, MSI).
|
M14 DMA + barriers, M15 MSI), and the driver *contract* on top of them —
|
||||||
|
hello, supervision, restart — is built too (device-manager.md, M18).
|
||||||
15. **[process-management.md](process-management.md) — process management.** The
|
15. **[process-management.md](process-management.md) — process management.** The
|
||||||
microkernel's `ps`/`kill`/SIGCHLD: enumerate as a table snapshot, the
|
microkernel's `ps`/`kill`/SIGCHLD: enumerate as a table snapshot, the
|
||||||
supervision link as the kill authority, and child-exit notifications over the
|
supervision link as the kill authority, and child-exit notifications over the
|
||||||
same endpoints IRQs arrive on.
|
same endpoints IRQs arrive on.
|
||||||
16. **[process-lifecycle.md](process-lifecycle.md) — the process lifecycle.** Design:
|
16. **[process-lifecycle.md](process-lifecycle.md) — the process lifecycle.** Built
|
||||||
signals over IPC as the one lifecycle vocabulary every process speaks — the
|
(M17): signals over IPC as the one lifecycle vocabulary every process speaks — the
|
||||||
POSIX.1-1990 words with message delivery instead of stack hijack, the stable
|
POSIX.1-1990 words with message delivery instead of stack hijack, the stable
|
||||||
`runtime.process` interface, exit reasons, published exit events any stateful
|
`runtime.process` interface, exit reasons, published exit events any stateful
|
||||||
service can subscribe to (the VFS releasing dead clients' handles), and the two
|
service can subscribe to (the VFS releasing dead clients' handles), and the two
|
||||||
iron rules (cleanup is the kernel's job; kill is not a signal).
|
iron rules (cleanup is the kernel's job; kill is not a signal).
|
||||||
17. **[device-manager.md](device-manager.md) — the device manager.** Design: the
|
17. **[device-manager.md](device-manager.md) — the device manager.** Built (M18,
|
||||||
|
through the app surface): the
|
||||||
tree, the matcher, and the supervisor. Tree structure lives in the manager,
|
tree, the matcher, and the supervisor. Tree structure lives in the manager,
|
||||||
authority stays in the kernel; bus drivers report what they see; drivers are
|
authority stays in the kernel; bus drivers report what they see; drivers are
|
||||||
restarted through the lifecycle vocabulary — the plan that turns
|
restarted through the lifecycle vocabulary — the plan that turns
|
||||||
|
|||||||
@@ -362,3 +362,23 @@ the first DMA driver to protect and test against) and these smaller items:
|
|||||||
- **Interrupt priority / threaded IRQ latency.** `notifyFromIsr` enqueues the woken
|
- **Interrupt priority / threaded IRQ latency.** `notifyFromIsr` enqueues the woken
|
||||||
driver but doesn't preempt (`wakeLocked` deliberately leaves that to the caller), so
|
driver but doesn't preempt (`wakeLocked` deliberately leaves that to the caller), so
|
||||||
a woken driver waits for the next scheduling point.
|
a woken driver waits for the next scheduling point.
|
||||||
|
|
||||||
|
## The driver contract (M17–M18)
|
||||||
|
|
||||||
|
Claiming and mapping is half of being a danos driver; the other half is the
|
||||||
|
**lifecycle and protocol contract**, and the runtime makes it nearly free:
|
||||||
|
|
||||||
|
- Build on `runtime.service.run` — one replyWait loop folding protocol
|
||||||
|
requests, signals, and notifications into callbacks. The harness answers the
|
||||||
|
universal zero-length ping and turns `terminate` into a clean exit for you
|
||||||
|
([process-lifecycle.md](process-lifecycle.md)).
|
||||||
|
- A driver spawned with an assignment (its device id as argv[1]) sends the
|
||||||
|
versioned `hello` to the device manager inside the deadline, and a **bus**
|
||||||
|
driver reports what it discovers with `child_added`
|
||||||
|
([device-manager.md](device-manager.md); usb-xhci-bus is the reference
|
||||||
|
implementation).
|
||||||
|
- Crash freely — that is the design. The kernel releases your claims, IRQ
|
||||||
|
bindings, and MSI vectors at death; the manager reads your exit reason,
|
||||||
|
prunes what you reported, restarts you with backoff, and your fresh instance
|
||||||
|
re-claims and re-reports. Never depend on your own cleanup running
|
||||||
|
(iron rule 1).
|
||||||
|
|||||||
+10
-1
@@ -122,7 +122,9 @@ branch is green; keep branches; push everything.
|
|||||||
## Phase notes
|
## Phase notes
|
||||||
|
|
||||||
**M19.0 apertures:** the boot memory map already crosses the handoff
|
**M19.0 apertures:** the boot memory map already crosses the handoff
|
||||||
([boot-handoff]); the holes computation belongs where the bridge node is built
|
([boot-handoff]), but discovery never sees it today — expect a small
|
||||||
|
pass-through (kernel init hands the map to the platform layer) before the
|
||||||
|
holes computation, which belongs where the bridge node is built
|
||||||
(`parseMcfg`). Sanity-check on QEMU q35: the xHCI BAR (`0xc0000000`-region
|
(`parseMcfg`). Sanity-check on QEMU q35: the xHCI BAR (`0xc0000000`-region
|
||||||
values seen in the M18 logs) must land inside a derived aperture, asserted in
|
values seen in the M18 logs) must land inside a derived aperture, asserted in
|
||||||
the kernel unit test.
|
the kernel unit test.
|
||||||
@@ -142,6 +144,13 @@ scenario can assert it.
|
|||||||
kernel still enumerates (timers, ACPI nodes until M20.3). The PCI arm of
|
kernel still enumerates (timers, ACPI nodes until M20.3). The PCI arm of
|
||||||
`pciDriverFor` switches source; `driverFor` doesn't move until M20.3.
|
`pciDriverFor` switches source; `driverFor` doesn't move until M20.3.
|
||||||
|
|
||||||
|
**M20.1 spawn and identity (pre-settled 2026-07-13):** the manager spawns
|
||||||
|
`discovery` by its neutral ramdisk name at startup, as an ordinary protocol
|
||||||
|
driver (hello, supervision) — from M20.1 on, on every boot. For reporting ACPI
|
||||||
|
devices, `ChildAdded` gains `hid: [8]u8` (EISA ids fit; zero = none):
|
||||||
|
firmware *string* identity travels beside the numeric `identity` field until
|
||||||
|
the FDT-driven widening replaces both (decision 7).
|
||||||
|
|
||||||
**M20.1 Hal in ring 3:** `mapMmio` → `device.mmioMap` over the claimed
|
**M20.1 Hal in ring 3:** `mapMmio` → `device.mmioMap` over the claimed
|
||||||
acpi-tables node (plus a table-offset map for blobs); `pioRead`/`pioWrite` →
|
acpi-tables node (plus a table-offset map for blobs); `pioRead`/`pioWrite` →
|
||||||
`device.ioRead`/`ioWrite` against its io_port resource. The interpreter cannot
|
`device.ioRead`/`ioWrite` against its io_port resource. The interpreter cannot
|
||||||
|
|||||||
+12
-5
@@ -1,10 +1,17 @@
|
|||||||
# Resilience: fault isolation and live restart
|
# Resilience: fault isolation and live restart
|
||||||
|
|
||||||
Steps 1–2 of the ordering below are **built**: user-mode isolation, and fault →
|
Steps 1–4 of the ordering below are **built** (M17–M18, 2026-07-13): user-mode
|
||||||
kill the process → keep the core (`onException` in `system/kernel/kernel.zig`; the
|
isolation; fault → kill the process → keep the core (`onException`; the
|
||||||
`fault-recovery` test proves a crashing ring-3 process dies alone while the system
|
`fault-recovery` test); the supervisor notification **with exit reasons**
|
||||||
keeps running). The supervisor notification and restart policy (steps 3+) are
|
([process-lifecycle.md](process-lifecycle.md) — clean exit, fault class, or
|
||||||
still design. This is the property danos is really chasing:
|
killed, recorded before the notice posts); and the **restart policy itself**
|
||||||
|
([device-manager.md](device-manager.md)): the device manager supervises every
|
||||||
|
driver, restarts crashes with backoff, caps crash loops, and re-claims work
|
||||||
|
because the kernel releases a dead process's claims. The `driver-restart` and
|
||||||
|
`usb-report` scenarios prove kill → release → respawn → re-claim → re-report
|
||||||
|
end to end. What remains of this document's ladder is scope, not mechanism:
|
||||||
|
more of the system moved into restartable processes (the discovery migration,
|
||||||
|
[m19-m20-plan.md](m19-m20-plan.md), is the next rung). This is the property danos is really chasing:
|
||||||
**if a part of the OS breaks, isolate it, and re-initialise it — without rebooting.**
|
**if a part of the OS breaks, isolate it, and re-initialise it — without rebooting.**
|
||||||
A crashed driver gets restarted; a wedged service gets killed and brought back. It's
|
A crashed driver gets restarted; a wedged service gets killed and brought back. It's
|
||||||
the reason the [microkernel](vision.md) shape was chosen, and it's a *separate* goal
|
the reason the [microkernel](vision.md) shape was chosen, and it's a *separate* goal
|
||||||
|
|||||||
Reference in New Issue
Block a user