From 5930c9653c64a16b40a789f5902a33d3b546c3fe Mon Sep 17 00:00:00 2001 From: Daniel Samson <12231216+daniel-samson@users.noreply.github.com> Date: Sun, 9 Aug 2026 10:17:46 +0100 Subject: [PATCH] =?UTF-8?q?docs:=20device-authority=20as=20built=20?= =?UTF-8?q?=E2=80=94=20spawn=20carries=20the=20device,=20the=20loan,=20con?= =?UTF-8?q?finement=20rebuilt=20on=20return?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/os-development/device-authority.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/docs/os-development/device-authority.md b/docs/os-development/device-authority.md index 9509214..d2aedbb 100644 --- a/docs/os-development/device-authority.md +++ b/docs/os-development/device-authority.md @@ -149,3 +149,27 @@ 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.