kernel: device_transfer — you may give away what you hold

The mechanism behind delegation, which device-manager.md named as the step
after hello: the device manager claims what discovery seeded and hands each
device to the driver it matched, so assignment stops being
first-come-first-served.

It is a MOVE, not a copy. A claim is exclusive (driver-model.md, invariant
1), so the giver stops holding the device the instant the receiver starts.
That is why this is a new syscall rather than the M13 capability path, where
a passed handle is shared refcounted — exclusivity cannot be expressed that
way.

The kernel's whole rule is that you may give away what you hold. It has no
notion of which task is the device manager and deliberately gains none: a
binary name inside the kernel is not something that cannot safely live in
user space. A recipient that does not exist is refused, because a device
moved to nobody would be unreachable for the rest of the boot — nothing
un-holds a device but task death.

Three errnos, each naming its own rule: ENODEV no such device, EPERM you do
not hold it, ESRCH no such recipient.

Nothing uses it yet. The five claimants move across one at a time in D4-D5,
so the suite stays green throughout and a regression names the driver that
caused it.

Ten assertions, verified to discriminate: removing the ownership check flips
four of them, including the giveaway that an illegal transfer then blocks
the legitimate claim behind it.

Suite 116 -> 117.
This commit is contained in:
Daniel Samson
2026-08-08 17:11:59 +01:00
parent 547d0ec46b
commit 3111c7c5e6
7 changed files with 148 additions and 1 deletions
+1
View File
@@ -85,6 +85,7 @@ pub const SystemCall = enum(u64) {
dma_bind = 51, // dma_bind(device_id, region_handle) -> 0/-errno: map a DMA-region capability into the claimed device's IOMMU domain (idempotent). The caller must own the device and hold the handle
dma_unbind = 52, // dma_unbind(device_id, region_handle) -> 0/-errno: unmap a previously bound region from the device's domain and invalidate
handle_close = 53, // handle_close(handle) -> 0/-errno: drop one capability handle and free its table slot (endpoints, shared-memory, DMA regions)
device_transfer = 54, // device_transfer(device_id, task_id) -> 0/-errno: give a device you hold to another task. A MOVE, not a copy — a claim is exclusive (-ENODEV no such device, -EPERM you do not hold it, -ESRCH no such task)
_,
};