Daniel Samson
3c9f454398
P4 of docs/establishment-planes-plan.md. The new usb-two-controllers case is
the Ryzen mouse bug pinned in the suite: a second xHCI controller with its
own keyboard while the boot controller keeps the default one — both must
come up, on different device ids, which requires each class driver to reach
ITS OWN controller. Discrimination: at 72807c2 (name-based establishment)
the case fails — one keyboard is unreachable, exactly the bench failure —
verified against a checkout of that merge; with lineage routing it passes.
The existing second-controller cases could not prove this: the boot bus
always carries a keyboard, so their expects were satisfiable by it.
Docs updated with the code: device-manager.md (hello moves the channels,
paged enumerate, delegation as built, reap-and-rebuild in the restart
sequence), device-authority.md (the fourth as-built decision: driver-layer
channels ride the hello; hello is no longer only the liveness handshake).
Full suite: 118/119, the one failure being iommu-fault's fixed 200 ms
fault window under end-of-run host load — 3/3 green standalone, deflake
flagged separately. usb-two-controllers passed inside the full run.
188 lines
11 KiB
Markdown
188 lines
11 KiB
Markdown
# Device authority: the implementation of delegation
|
|
|
|
*Implementation design, 2026-08-08. The **what** is settled in
|
|
[device-manager.md](../device-driver-development/device-manager.md) — "structure in the
|
|
manager, authority in the kernel", and delegation as the step after `hello`. This
|
|
document is the **how**, and the decisions that paragraph leaves open.*
|
|
|
|
Read first: [drivers.md](../device-driver-development/drivers.md) (the claim is the
|
|
capability), [driver-model.md](../device-driver-development/driver-model.md) (the three
|
|
invariants), [device-manager.md](../device-driver-development/device-manager.md) (the
|
|
tree, the matcher, the supervisor).
|
|
|
|
## The one thing not yet true
|
|
|
|
`device-manager.md` says assignment "stays argv for now", and names the next step:
|
|
|
|
> The step after `hello` exists is delegation: the manager claims (or is granted) the
|
|
> devices and passes the claim to the driver over IPC (the M13 capability-transfer
|
|
> mechanism), replacing first-come-first-served `device_claim` with policy.
|
|
|
|
Until that lands, the manager's matching is advisory. `device_claim` checks only that
|
|
the device exists and is unheld ([devices-broker.zig](../../system/kernel/devices-broker.zig)):
|
|
|
|
```zig
|
|
pub fn claim(id: u64, owner: u32) ClaimError!void {
|
|
if (id >= count) return error.NoSuchDevice;
|
|
if (claimed[@intCast(id)] != null) return error.AlreadyClaimed;
|
|
claimed[@intCast(id)] = owner;
|
|
}
|
|
```
|
|
|
|
A driver is spawned with its device id in `argv[1]` and claims it; any process could
|
|
pass any integer instead. Since a claim is a licence to map physical memory, that is the
|
|
gap this document closes.
|
|
|
|
## Decision 1: the manager claims, then transfers
|
|
|
|
`device-manager.md` leaves "claims (or is granted)" open. **Claims.**
|
|
|
|
The manager runs before any driver exists — `init` starts it from `init.csv`, and it is
|
|
what spawns drivers — so it takes the seeded devices unopposed and there is nothing
|
|
unheld left for anyone to race for. One new call moves ownership on:
|
|
|
|
```
|
|
device_transfer(device_id, task_id) -> 0/-errno
|
|
```
|
|
|
|
The kernel checks only that the caller currently holds the device. No names, no
|
|
attestation, no notion of "the device manager" — the rule is *you may give away what you
|
|
hold*, which is the capability discipline already in force.
|
|
|
|
The alternative was the kernel granting roots to a task it recognises by binary path
|
|
plus a PID-1 supervisor. It is more robust — it does not depend on the manager being
|
|
first — but it puts a binary name inside the kernel, and the goal is that the kernel
|
|
keeps only what cannot safely live in user space. A name is not that.
|
|
|
|
**The residual, stated plainly:** authority here rests on the manager claiming first.
|
|
That holds because `init.csv` decides what starts and in what order, so it is an
|
|
operator-visible ordering rather than an attacker-controlled one — but it is an
|
|
assumption, not an enforced invariant. The enforced version arrives with the spawn
|
|
capability [drivers.md](../device-driver-development/drivers.md) already names as
|
|
missing ("`system_spawn` is currently ungated … because there is no spawn capability
|
|
yet"). This design is compatible with it and does not block on it.
|
|
|
|
## Decision 2: the kernel stops holding inventory
|
|
|
|
The kernel reads exactly three things out of a descriptor: **physical ranges** (to check
|
|
a mapping falls inside one), **interrupt numbers**, and **one PCI BDF** (to key an IOMMU
|
|
domain). Vendor, device and subsystem ids, class triples, `_HID` strings, bus addresses
|
|
and names are stored only so `device_enumerate` can hand them back — which
|
|
`device-manager.md` already resolves: that call "fades to a manager-internal (then
|
|
deleted) seam", because the manager owns the tree as data.
|
|
|
|
So the kernel's table becomes: **parent, resources, holder, BDF.** That is what cannot
|
|
safely run in user space; the rest moves.
|
|
|
|
**Devices with no resources leave the kernel entirely.** A USB device is addressed
|
|
through its controller and carries `resource_count = 0`
|
|
([driver-model.md](../device-driver-development/driver-model.md): "that case is allowed
|
|
and is the common one"). It conveys no mapping authority, so there is nothing for the
|
|
kernel to enforce and no reason for it to know. It is inventory, and inventory is the
|
|
manager's — reported by `child_added`, which already carries everything needed.
|
|
|
|
That is also the case that made `maximum_children_per_parent` necessary: a zero-resource
|
|
child sidesteps containment, so a driver could loop `device_register` and fill the
|
|
shared table. Once such children are not kernel objects, every remaining entry is a real
|
|
contained subdivision of something the caller holds.
|
|
|
|
## Decision 3: no shared ceiling; a per-holder quota instead
|
|
|
|
`maximum_devices = 64` and `maximum_children_per_parent = 16` are numbers we invented,
|
|
and both are shared — one driver's enumeration starves every other driver, which is how
|
|
an AMD Ryzen booted with no USB and no storage.
|
|
|
|
- **The table becomes dynamic.** It is built after `heap.init` (`kernel.zig`: `pmm.init`
|
|
at 137, `heap.init` at 179, `devices_broker.init` at 202), so nothing prevents it. No
|
|
specification bounds how many devices a machine has, so nothing should bound ours.
|
|
- **`maximum_children_per_parent` is deleted**, because the authorisation it stood in
|
|
for now exists.
|
|
- **A per-holder quota replaces them.** Dynamic storage without a bound moves the
|
|
ceiling to the kernel heap, which is shared and fatal rather than partial — strictly
|
|
worse. The bound that is *not* worse is one charged to the task that caused it: a
|
|
driver that loops `device_register` exhausts its own allowance, is refused with an
|
|
attributable errno, and is restarted by its supervisor while every other driver
|
|
carries on. That is the microkernel property rather than a workaround for it, and it
|
|
is declared through [bounds.md](bounds.md) like any other.
|
|
|
|
## The shape of the change
|
|
|
|
| | Before | After |
|
|
|---|---|---|
|
|
| Manager gets its devices | claims them, unauthorised | claims them (first, unopposed) |
|
|
| Driver gets its device | `argv[1]` + `device_claim` | receives it in the `hello` reply |
|
|
| Kernel checks | is it free? | do you hold it? |
|
|
| Kernel stores | the full descriptor | parent, resources, holder, BDF |
|
|
| Zero-resource devices | kernel table entries | manager records only |
|
|
| Table size | `maximum_devices = 64` | dynamic, per-holder quota |
|
|
| Children per parent | `maximum_children_per_parent = 16` | deleted |
|
|
|
|
Bring-up order changes for the five claiming drivers: `hello` must precede the claim,
|
|
because the reply is where the device arrives. `pci-bus` today does the reverse — its
|
|
own comment reads "Claim the bridge, map the ECAM, hello the manager, then scan."
|
|
|
|
## What does not change
|
|
|
|
- The three invariants of [driver-model.md](../device-driver-development/driver-model.md):
|
|
a claim is exclusive, a descriptor is a licence to map physical memory, therefore
|
|
containment. This design strengthens the first and touches neither of the others.
|
|
- The display service's GOP path. The framebuffer is not a device — it is where pixels
|
|
go, handed over by the loader, and the compositor uses it as the boot floor until a
|
|
real display driver announces itself
|
|
([display-v2.md](../device-driver-development/display-v2.md)). The kernel wraps it in
|
|
a display-class descriptor so `mmio_map` can hand it over write-combining; that is
|
|
plumbing for a mapping, not a claim about what it is.
|
|
- Supervision, restart, pruning and re-report
|
|
([device-manager.md](../device-driver-development/device-manager.md),
|
|
[process-lifecycle.md](process-lifecycle.md)). Delegation slots into the existing
|
|
`hello` exchange and changes none of it.
|
|
- `device_register` idempotency, which is what lets a restarted bus rebuild the same
|
|
ids.
|
|
|
|
## How it is verified
|
|
|
|
The invariant is: **a process holds what it was handed and cannot name its way into
|
|
holding more.** The suite has no adversarial device case today — the audit's lesson was
|
|
that "the suite contains no attacker" — so this adds one: a process that was handed
|
|
nothing calls `device_claim` and `device_transfer` on a device another driver holds, and
|
|
on one nobody holds, and is refused each time with its own errno.
|
|
|
|
The Ryzen is the acceptance test for the ceiling half: it is the machine that found the
|
|
constants, and the one that proves them gone.
|
|
|
|
## As built (2026-08-09)
|
|
|
|
Three details settled differently, or beyond, what the sections above say:
|
|
|
|
- **The device arrives with the spawn, not in the `hello` reply.** `system_spawn` grew a
|
|
sixth argument: the manager names the device it is giving, the kernel verifies the
|
|
caller holds it before the child exists, and the child holds it before its first
|
|
instruction. A give that fails after the spawn (the device stopped being the giver's,
|
|
or its confinement was refused) kills the child — a driver running without the
|
|
hardware it was spawned for is worse than no driver. `hello` stays what it was: the
|
|
liveness handshake.
|
|
- **A given device is a loan.** When the holder dies, the device returns to the giver if
|
|
the giver is still alive — so a respawned driver is handed the same device by its
|
|
manager instead of racing anyone for a released claim. Only if the lender is also dead
|
|
does the device become unheld.
|
|
- **Confinement moves with the device, and is rebuilt when the loan comes back.** A
|
|
transfer re-points the existing IOMMU record; but a death tears the domain down
|
|
*before* the loan returns, so the next delegation of that device finds no record and
|
|
confines afresh — under the same fail-closed rule as a first claim (`ECONFINE`, the
|
|
give does not stand). Without that, one driver crash left its device silently
|
|
unconfined forever. Both give paths (`device_transfer` and spawn's give) share one
|
|
body in [process.zig](../../system/kernel/process.zig) (`giveDeviceLocked`), and the
|
|
`iommu` kernel test drives the death-and-respawn sequence against it directly.
|
|
|
|
A fourth followed on 2026-08-09, when a real three-controller machine broke the last
|
|
name-shaped assumption ([communication.md](communication.md) "Establishment: two
|
|
planes, one namespace"): **driver-layer channels ride the same hello.** A driver's
|
|
serving endpoint goes up as the hello's capability; consumers get their provider's
|
|
channel down in the reply, routed by the manager's lineage — the reporter for a
|
|
class driver, the bound driver for a `.consumer`. `usb-transfer` and `block`
|
|
stopped being registry names, and a reporter's death now reaps its class-driver
|
|
subtree so the re-report can rebuild it against the successor — the manager half of
|
|
the loan story above. One correction to the earlier bullet: `hello` is no longer
|
|
*only* the liveness handshake; it is also where establishment happens. The device
|
|
itself still arrives with the spawn.
|