daniel/danos
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects 1 Releases Wiki Activity

docs: reorder the Run 2 table to the plan order and note the executed sequence

Browse Source
This commit is contained in:
Daniel Samson
2026-08-08 21:58:53 +01:00
parent b7d97ebb5d
commit 337b981c07
1 changed files with 14 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/bounds-track-plan.md
+14 -10
View File
@@ -39,17 +39,21 @@ that cannot safely run in user space.**
| Step | What | State |
|---|---|---|
| D0 | The grant rides `system_spawn` — atomic, so no driver need change to receive one | **done** |
| D1 | `device_transfer(device_id, task_id)` — the holder gives a device away | **done** — syscall 54; a move, not a copy |
| D2 | Adversarial case: a process handed nothing is refused, on a held device and a free one | **done** — `device-authority-test`; the claim half joins it at D6 |
| D3 | The manager claims the seeded devices at boot, before any driver is spawned | **merged into D4** — see below |
| D4 | The manager claims + delegates on `hello`; `usb-xhci-bus` is the first driver converted | **done** — caught an IOMMU regression I introduced; see below |
| D5 | The other four claimants converted: `pci-bus`, `ps2-bus`, `virtio-gpu`, `acpi` | **done** — every driver now receives its hardware; question 9 answered |
| D0 | The grant rides `system_spawn` — atomic, so no driver need change to receive one | **done** — and caught a test-marker bug that made the D2 fixture unfailable |
| D10 | Every driver hellos, on its own merits (liveness, one class of driver) | not started — optional, independent |
| D6 | `device_claim` refuses a device the caller was not handed; the hole is closed | **blocked on question 10** — only the display service's GOP path still claims |
| D7 | Zero-resource devices stop being kernel objects — inventory moves to the manager | **blocked** — nothing else mints their ids; see question 8 |
| D8 | **`maximum_children_per_parent` deleted** | **done** — it was unblocked from the moment D9 landed; I kept reading my own stale label |
| D9 | The device table becomes dynamic; **`maximum_devices` deleted**; per-holder quota declared | **done** — one of the two invented numbers is gone |
| D2 | Adversarial case: a process handed nothing is refused | **done** — `device-authority-test`; the claim half joins it at D6 |
| D3 | The manager claims the seeded devices before any driver is spawned | **merged into D4** |
| D4 | `usb-xhci-bus` receives its controller | **done** — caught an IOMMU regression I introduced |
| D5 | `pci-bus`, `virtio-gpu`, `ps2-bus`, discovery receive theirs | **done** — every driver now receives its hardware |
| D6 | `device_claim` refuses a device the caller was not handed | **blocked on question 10** |
| D7 | Zero-resource devices stop being kernel objects | **blocked on question 8** |
| D8 | **`maximum_children_per_parent` deleted** | **done** |
| D9 | Dynamic table; **`maximum_devices` deleted**; per-registrar allowance | **done** |
| D10 | Every driver hellos, on its own merits | not started — optional, independent |
*Executed in the order D1, D2, D4, D5(part), D9, D0, D5(rest), D8 — the numbering is
the original plan's, not the sequence. D0 was added mid-run, D3 merged into D4, and D8
turned out to have been unblocked since D9.*
**Run 2 stops, blocked on one question.** Landed: D0, D1, D2, D4, D8, D9, and D5 for
three of five claimants (`usb-xhci-bus`, `pci-bus`, `virtio-gpu`). Suite 118/118.