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

device-manager: delete the delegated-set scaffolding

Browse Source 
The name list and its predicate existed so drivers could move to delegation
one at a time with the suite green throughout. Every driver is delegated
now, so the manager simply hands over whatever device a driver was assigned.

Deleting it caught a real consequence: crash-test finally got delegated too,
and it was still claiming its device — so it got AlreadyClaimed because it
already held it, exited, and the restart drill had nothing to restart. Its
own comment named what the case was really checking: "the respawn only
reaches this line because the kernel released the previous instance's claim
at death". That property still holds, by a different mechanism — the device
reverts to the manager on death and is handed to the replacement, which is
the same guarantee without the race it used to rely on.

All four delegation paths verified: the xHCI controller, the PCI bridge, the
PS/2 two-node singleton, and virtio-gpu's restart re-attach.

Run 3 complete. Suite 118/118.
This commit is contained in:
Daniel Samson
2026-08-08 23:01:29 +01:00
parent df9c1ed827
commit 0eb2420690
3 changed files with 16 additions and 39 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/bounds-track-plan.md
+5 -1
View File
@@ -137,12 +137,16 @@ giver, and its comment says so rather than implying a protection it is not provi
| E3 | `device_claim` refuses a device that has a giver — **done**, but unreachable: E2 already closed the window |
| E4 | The manager claims every resource-bearing device at boot, so nothing is left takeable — **done** (boot snapshot only; see below) |
| E5 | The attacker fixture gains the claim half it has been waiting for since D2 — **done with E4** |
| E6 | Delete the delegated-set scaffolding — every driver is delegated now |
| E6 | Delete the delegated-set scaffolding — every driver is delegated now — **done** |
Ordering: E1 alone changes no behaviour. E2 must precede E3, or a restart cannot
re-acquire. E4 must precede E5, or the attacker will find takeable devices and the
assertion will be wrong about why. E6 is cleanup.
**Run 3 complete.** Suite 118/118. Every driver receives its hardware; a grant is a
loan that returns to its lender when the borrower dies; nothing firmware-discovered is
left unheld except the framebuffer, which the compositor owns.
### E4's scope, stated
It covers the **boot snapshot**. A device *reported* later and matched to no driver