docs: Run 3 — close the claiming hole, six steps, no open questions
One field settles both outstanding questions. The kernel records who gave each device. device_claim then refuses anything that has a giver, and on death a device reverts to its giver rather than to nobody. The framebuffer needs no exemption: nobody delegates it, so it has no giver, so the display service claims it exactly as today. The rule never mentions display. And restart stops racing. Today a dying driver releases its claim to nobody and the manager re-claims first-come, so every restart reopens the hole this run closes; a loan that reverts to its lender removes the window entirely. The zero-resource inventory question is dropped from the plan rather than carried as a blocker. It is real but nothing depends on it.
This commit is contained in:
@@ -95,6 +95,59 @@ They land together, with the manager claiming only for drivers in an explicit
|
|||||||
anything in D4 — recorded rather than dismissed, because D4 moved the `hello` earlier
|
anything in D4 — recorded rather than dismissed, because D4 moved the `hello` earlier
|
||||||
and so did shift boot timing. Watch it across the remaining steps.
|
and so did shift boot timing. Watch it across the remaining steps.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## Run 3 — close the claiming hole
|
||||||
|
|
||||||
|
*Every driver now receives its hardware. What remains is that `device_claim` still
|
||||||
|
works for anyone, so a device nobody holds can still be taken. Six steps, no open
|
||||||
|
questions.*
|
||||||
|
|
||||||
|
### The rule this run implements
|
||||||
|
|
||||||
|
The kernel records, per device, **who gave it**. From that one field everything follows:
|
||||||
|
|
||||||
|
- `device_transfer` and the spawn-fused grant set the giver.
|
||||||
|
- **`device_claim` refuses a device that has a giver.** A device that was given to
|
||||||
|
someone is delegated hardware and must be handed on, never taken.
|
||||||
|
- **On death a device reverts to its giver**, if that task is still alive; otherwise its
|
||||||
|
claim clears. A grant is a loan, not a gift.
|
||||||
|
|
||||||
|
Two things fall out rather than being special-cased:
|
||||||
|
|
||||||
|
- **The framebuffer is untouched.** Nobody delegates it, so it has no giver, so the
|
||||||
|
display service can still claim it exactly as today. No exemption in the kernel, no
|
||||||
|
mention of display anywhere in the rule.
|
||||||
|
- **Restart needs no race.** A dying driver's device returns to the manager, which
|
||||||
|
re-delegates it on respawn. Today the kernel releases it to nobody and the manager
|
||||||
|
re-claims first-come, so every restart reopens the hole this run closes.
|
||||||
|
|
||||||
|
| Step | What |
|
||||||
|
|---|---|
|
||||||
|
| E1 | Record a giver per device; `device_transfer` and the spawn grant set it |
|
||||||
|
| E2 | On task death a device reverts to its giver if alive, else its claim clears |
|
||||||
|
| 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 |
|
||||||
|
| E6 | Delete the delegated-set scaffolding — every driver is delegated now |
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
### Not in this run, and not blocking it
|
||||||
|
|
||||||
|
**Zero-resource devices stay in the kernel.** Moving them out needs an answer to who
|
||||||
|
mints their ids, given that the id is the `device_token` on the usb-transfer wire and
|
||||||
|
the kernel's idempotency is what keeps it stable across a bus restart. Nothing depends
|
||||||
|
on it: both invented ceilings are already gone and this run does not need it. Recorded
|
||||||
|
as future work.
|
||||||
|
|
||||||
|
**Not every driver hellos.** Delivery no longer needs it, so it stands or falls on its
|
||||||
|
own merits — uniform liveness and one class of driver. Also future work.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
### Question 9 — answered: a singleton gets every device that matched it
|
### Question 9 — answered: a singleton gets every device that matched it
|
||||||
|
|
||||||
The 8042 is one controller described by two ACPI nodes, so it cannot be split across
|
The 8042 is one controller described by two ACPI nodes, so it cannot be split across
|
||||||
|
|||||||
Reference in New Issue
Block a user