establishment: the two-controller proof, and the docs catch up
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.
This commit is contained in:
@@ -74,13 +74,26 @@ one world.
|
|||||||
|
|
||||||
| Direction | Packet | Purpose |
|
| Direction | Packet | Purpose |
|
||||||
|---|---|---|
|
|---|---|---|
|
||||||
| driver → manager | `hello { role, version }` @ the assigned device | confirms the argv assignment, starts the deadline clock |
|
| driver → manager | `hello { role, wants_channel, version }` @ the assigned device | confirms the assignment, starts the deadline clock — **and moves the channels** (below) |
|
||||||
| bus → manager | `child_added { parent, bus_address, identity, bus, vendor, device, subsystem, hid }` @ the registered device id | one node the bus discovered |
|
| bus → manager | `child_added { parent, bus_address, identity, bus, vendor, device, subsystem, hid }` @ the registered device id | one node the bus discovered |
|
||||||
| bus → manager | `child_removed { parent, bus_address }` | unplug, or the bus lost it |
|
| bus → manager | `child_removed { parent, bus_address }` | unplug, or the bus lost it |
|
||||||
| app → manager | `enumerate` (reserved verb 1) | snapshot of the tree: one `ChildEntry` per record in the reply's tail |
|
| app → manager | `enumerate` (reserved verb 1) @ start index | one page of the tree, one `ChildEntry` per record in the reply's tail; a short page is the end |
|
||||||
| app → manager | `subscribe` (reserved verb 2) | receive published add/remove events; the subscriber's endpoint rides as the call's capability |
|
| app → manager | `subscribe` (reserved verb 2) | receive published add/remove events; the subscriber's endpoint rides as the call's capability |
|
||||||
| manager → app | `child_added` / `child_removed` events | the same two structs, pushed rather than called |
|
| manager → app | `child_added` / `child_removed` events | the same two structs, pushed rather than called |
|
||||||
|
|
||||||
|
**`hello` is also the establishment plane for driver-layer channels**
|
||||||
|
([communication.md](../os-development/communication.md) "Establishment: two
|
||||||
|
planes, one namespace"). A provider's hello carries its serving endpoint UP as
|
||||||
|
the call's capability (the xHCI bus its transfer endpoint, usb-storage its
|
||||||
|
block endpoint — several processes provide those contracts, so neither is ever
|
||||||
|
a registry name). A hello with `wants_channel` set is answered with a
|
||||||
|
capability DOWN: for a `.device`-role driver, the channel of its device's
|
||||||
|
*reporter* (a class driver reaching its own controller); for a `.consumer`
|
||||||
|
(not a spawned driver at all — fat looking for its volume), the channel of the
|
||||||
|
driver *bound to* the target device. No channel in an acked reply means the
|
||||||
|
provider is mid-restart and its re-report is on the way — retryable, never a
|
||||||
|
verdict.
|
||||||
|
|
||||||
The watcher table behind those last two rows is the **service harness's**
|
The watcher table behind those last two rows is the **service harness's**
|
||||||
(`service.Subscribers`, shared with input and power), not the manager's: it
|
(`service.Subscribers`, shared with input and power), not the manager's: it
|
||||||
answers `subscribe`/`unsubscribe`, frames each event once for the fan-out, and
|
answers `subscribe`/`unsubscribe`, frames each event once for the fan-out, and
|
||||||
@@ -113,10 +126,11 @@ the stop sequence and the restart policy. Everything else lifecycle-shaped
|
|||||||
(terminate, the common `ping` liveness call, exit reasons) arrives through
|
(terminate, the common `ping` liveness call, exit reasons) arrives through
|
||||||
[process-lifecycle.md](../os-development/process-lifecycle.md)'s vocabulary, not this protocol.
|
[process-lifecycle.md](../os-development/process-lifecycle.md)'s vocabulary, not this protocol.
|
||||||
|
|
||||||
Assignment stays argv (`usb-xhci-bus <device id>`) for now — simple, and it works.
|
Delegation is BUILT (docs/os-development/device-authority.md "As built"): the
|
||||||
The step after `hello` exists is delegation: the manager claims (or is granted) the
|
device arrives WITH the spawn — `system_spawn`'s sixth argument moves the
|
||||||
devices and passes the claim to the driver over IPC (the M13 capability-transfer
|
claim before the child's first instruction — and the id still rides argv for
|
||||||
mechanism), replacing first-come-first-served `device_claim` with policy. Identity in
|
the driver to name itself by. A given device is a loan that returns to the
|
||||||
|
manager on the holder's death. Identity in
|
||||||
`child_added` is per-bus: PCI children carry the class triple (`pci_class`, as the
|
`child_added` is per-bus: PCI children carry the class triple (`pci_class`, as the
|
||||||
xHCI match already uses); USB children carry the (class, subclass, protocol) triple
|
xHCI match already uses); USB children carry the (class, subclass, protocol) triple
|
||||||
from usb-ids.zig — each bus's native language, decoded by the shared ids modules.
|
from usb-ids.zig — each bus's native language, decoded by the shared ids modules.
|
||||||
@@ -133,13 +147,19 @@ On a death notification:
|
|||||||
Clean exit → it meant to; don't restart. Fault or missed `hello` deadline →
|
Clean exit → it meant to; don't restart. Fault or missed `hello` deadline →
|
||||||
restart with **backoff**, and a crash-loop cap (three fast deaths → mark failed,
|
restart with **backoff**, and a crash-loop cap (three fast deaths → mark failed,
|
||||||
stop respawning, log loudly; a later `reload` to the manager can retry).
|
stop respawning, log loudly; a later `reload` to the manager can retry).
|
||||||
2. **Prune the subtree** the dead bus driver reported. Its children describe
|
2. **Prune the subtree** the dead bus driver reported, **reaping the class
|
||||||
protocol state (xHCI slot ids, transfer rings) that died with the process;
|
drivers bound to its children**. Its children describe protocol state (xHCI
|
||||||
keeping the nodes would be keeping a lie. Watchers receive `child_removed` — the
|
slot ids, transfer rings) that died with the process; keeping the nodes
|
||||||
input service losing, then regaining, a keyboard is the *honest* description of
|
would be keeping a lie — and the class drivers hold channels into the dead
|
||||||
what happened. The restarted instance rediscovers and re-reports.
|
process they cannot observe dying (an HID driver blocks on reports that
|
||||||
3. **The claim is already free** because the kernel released it at death — the
|
simply never come). Each is killed and its entry cleared, so the matcher
|
||||||
restarted instance claims the same controller and comes up.
|
can respawn a fresh generation when the re-report arrives; their hellos
|
||||||
|
fetch the successor's channel. Watchers receive `child_removed` — the input
|
||||||
|
service losing, then regaining, a keyboard is the *honest* description of
|
||||||
|
what happened.
|
||||||
|
3. **The device is already back** because the loan returned at death — the
|
||||||
|
manager re-delegates the same controller with the respawn, and the kernel
|
||||||
|
confines it afresh.
|
||||||
|
|
||||||
Who supervises the supervisor: **init** (PID 1), which already supervises the
|
Who supervises the supervisor: **init** (PID 1), which already supervises the
|
||||||
services it starts. If the manager dies, drivers keep running (they hold their
|
services it starts. If the manager dies, drivers keep running (they hold their
|
||||||
|
|||||||
@@ -173,3 +173,15 @@ Three details settled differently, or beyond, what the sections above say:
|
|||||||
unconfined forever. Both give paths (`device_transfer` and spawn's give) share one
|
unconfined forever. Both give paths (`device_transfer` and spawn's give) share one
|
||||||
body in [process.zig](../../system/kernel/process.zig) (`giveDeviceLocked`), and the
|
body in [process.zig](../../system/kernel/process.zig) (`giveDeviceLocked`), and the
|
||||||
`iommu` kernel test drives the death-and-respawn sequence against it directly.
|
`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.
|
||||||
|
|||||||
@@ -692,6 +692,28 @@ CASES = [
|
|||||||
r"(?=.*hub slot \d+ port \d+ device:.*0x0627)"
|
r"(?=.*hub slot \d+ port \d+ device:.*0x0627)"
|
||||||
r"(?=.*usb-hid-keyboard: ok \(device 3)",
|
r"(?=.*usb-hid-keyboard: ok \(device 3)",
|
||||||
"fail": r"DANOS-TEST-RESULT: FAIL"},
|
"fail": r"DANOS-TEST-RESULT: FAIL"},
|
||||||
|
# Establishment P4 — the Ryzen mouse bug, pinned (docs/establishment-planes-plan.md).
|
||||||
|
# A real machine carried THREE xHCI controllers; the transfer contract was one
|
||||||
|
# exclusive registry name, so every class driver reached whichever bus instance
|
||||||
|
# bound first, and a device behind any other controller was unreachable
|
||||||
|
# ("could not open device 50"). This case is the minimal reproduction: a second
|
||||||
|
# controller with its own keyboard, while the boot controller keeps the default
|
||||||
|
# keyboard — BOTH must come up, on different device ids, which requires each
|
||||||
|
# driver to reach ITS OWN controller. Under name-based establishment exactly one
|
||||||
|
# can; under lineage routing (the manager answers each hello with the reporter's
|
||||||
|
# channel) both do.
|
||||||
|
{"name": "usb-two-controllers",
|
||||||
|
"build_case": "usb-hid",
|
||||||
|
"smp": 4,
|
||||||
|
"timeout": 150,
|
||||||
|
"qemu_extra": ["-device", "qemu-xhci,id=xhci2",
|
||||||
|
"-device", "usb-kbd,bus=xhci2.0,port=1"],
|
||||||
|
# Two bus delegations, then two keyboards alive with distinct ids: the
|
||||||
|
# second `ok` must name a different device than the first, so one keyboard
|
||||||
|
# answering twice can never satisfy it.
|
||||||
|
"expect": r"(?s)(?=(?:[\s\S]*delegated device \d+ to /system/drivers/usb-xhci-bus){2})"
|
||||||
|
r"(?=[\s\S]*usb-hid-keyboard: ok \(device (\d+)\b[\s\S]*usb-hid-keyboard: ok \(device (?!\1\b)\d+)",
|
||||||
|
"fail": r"DANOS-TEST-RESULT: FAIL"},
|
||||||
# The driver must never truncate a configuration block. Its size is the DEVICE's
|
# The driver must never truncate a configuration block. Its size is the DEVICE's
|
||||||
# choice (wTotalLength, a u16); the driver used to read the first 512 bytes into a
|
# choice (wTotalLength, a u16); the driver used to read the first 512 bytes into a
|
||||||
# fixed buffer and parse those, so interfaces past the cut did not exist while
|
# fixed buffer and parse those, so interfaces past the cut did not exist while
|
||||||
|
|||||||
Reference in New Issue
Block a user