kernel: a grant is a loan — a dead borrower returns the device to its lender

When a driver dies, a device it was *given* now goes back to whoever lent
it, rather than to nobody. The device manager gets its hardware back the
instant a driver dies and hands it to the replacement, with no window in
between.

That window was real: the kernel released the claim to no one and the
manager re-claimed first-come, so every driver restart reopened the hole
this run is closing. It also becomes load-bearing at the next step — once
claim refuses a device that has a giver, releasing to nobody would strand a
dead driver's hardware permanently, because nobody could ever take it again.

A dead lender is no lender: the claim and the giver clear together, so a
device is never owed to a ghost. A device nobody lent is released outright,
exactly as before.

The broker cannot see the task table, so liveness arrives through the same
hook idiom the scheduler already uses. Null means assume dead, so a kernel
built without the hook frees claims rather than handing them to a ghost.

A stale binary nearly passed as proof for the third time this session: the
first discrimination patch left `alive` unused, the build failed with three
errors, and the old binary reported every assertion passing. Checking the
build before reading results is what caught it.

Suite 118/118.
This commit is contained in:
Daniel Samson
2026-08-08 22:21:25 +01:00
parent 4ca57fc37e
commit 1a1d92cba9
4 changed files with 55 additions and 4 deletions
+1 -1
View File
@@ -125,7 +125,7 @@ Two things fall out rather than being special-cased:
| Step | What |
|---|---|
| E1 | Record a giver per device; `device_transfer` and the spawn grant set it — **done** |
| E2 | On task death a device reverts to its giver if alive, else its claim clears |
| E2 | On task death a device reverts to its giver if alive, else its claim clears — **done** |
| E3 | `device_claim` refuses a device that has a giver |
| E4 | The manager claims every resource-bearing device at boot, so nothing is left takeable |
| E5 | The attacker fixture gains the claim half it has been waiting for since D2 |