The boundary · L3 and L2

Storage

sysk reads and writes a disk, a 512-byte sector at a time, and what it writes is there after a reboot (sysk 023). The driver is a task in sysp, down to the device's registers. The disk reads and writes memory by itself, and no hardware stops it from reaching the wrong memory. So the proofs do: the device can reach only memory its driver lent it.

A request's path

A client task asks the disk driver to write sector 2. Step through it. The colours say whose memory each step touches. Blue is a task's own memory. Purple is memory lent to the device: the driver cannot touch it until the device gives it back.

Devices are pages

A driver holds a Device. It carries the base address of the device's 4096-byte page of registers, and only the generated wiring can make one. The driver reads and writes registers with mmio-read32 and mmio-write32, and their contracts prove each access lies inside that page. The disk is the second device to work this way, after the UART (IO and drivers). It needed no new trusted code for its registers: the four loads and stores that the UART uses serve every device. arch/rv64/devices.sysk names the page and the interrupt:

(devices
  (uart (mmio 268435456 4096) (irq 10))
  (virtio-blk (mmio 268439552 4096) (irq 1)))

What the device may touch

PMP keeps a task inside its own memory, and that includes its device's page. A device that reads and writes memory itself (DMA) is not a task: PMP does not apply to it. Give it a wrong address, and it writes to the kernel, or to another task, or to a heap block that has since been freed. So the question is what addresses a device is ever given. sysk answers it by proof, in kernel/devices.sysp:

• Only one file makes addresses. buf-addr, the address of a buffer's bytes, is private to it, and it is the only way any sysp code gets an address. Every address written into a descriptor or a register comes from it.
• Only of memory the queue owns. The Queue owns its ring, and a Lent owns a request's buffer. Both are private resource structs: no driver can read their fields or make one.
• Lending is a move. virtio-lend takes the buffer. Until virtio-take gives it back, the driver cannot write it, free it, or lend it twice: the buffer is no longer the driver's to name. virtio-take needs the queue idle, which only virtio-poll can show, and the Lent names its queue, so a buffer lent on one of a device's queues cannot come back through another while the device still has it (sysk 042). A buffer the device may never return, one lent to receive a frame, comes back only by stopping the device: virtio-reset writes status 0 and waits until the device reads as reset, when it has let go of every queue (virtio 1.2 §4.2.3.1; sysk 052).
• What the device wrote is unknown. A buffer comes back through from-device, whose contract says only that its length is the same. No proof can rely on what the driver wrote into it before. The used ring, which the device changes at any time, is read only with a volatile load32, never as ordinary memory.

Each way of breaking these rules is a program the tests show sysp rejects:

The queue in memory

virtio talks through a split virtqueue. The descriptor table says where buffers are. The driver adds to the available ring, and the device adds to the used ring. Here all three fit in one 256-byte buffer of the driver's heap, starting at the first 16-byte boundary. One request is in flight per queue, in descriptors 0 to 2. The indices count modulo 65536, as virtio's do.

The kernel's queue knows no device's requests (sysk 042). A driver lends a buffer cut at two points into up to three parts, one descriptor each, and says from which part on the device writes: virtio puts what the device reads first. Empty parts are left out. When the request comes back, virtio-written says how many bytes the device wrote, never more than the buffer.

(virtio-lend dev q b cut1 cut2 wfrom)     ; parts before wfrom: read; from it on: written

the disk, a read     header 0–16 | data 16–528 | status 528–529     cut 16 528, written from 1
the disk, a write    the same                                         written from 2
a frame, received    the whole buffer                    cut n n,    written from 0
a frame, sent        the whole buffer                    cut n n,    written from 3: never

The disk's request is 529 bytes: the header the device reads, 512 bytes of data, and the status byte it writes. Its layout is the driver's, in drivers/disk.sysp; before sysk 042 it was the kernel's. The general queue found an assumption the old one hid: the buffer used to be 544 bytes, padded to a multiple of 16, and the status's descriptor exactly one byte. Lent as a part to the buffer's end, the status became 16 bytes, and the device wrote it at their end, as virtio's block device does, where the driver never looked. So the request is now exactly as long as its parts.

The driver

drivers/disk.sysp serves requests on a stream, ask, and answers each on answer, until ask ends. Both message types are 528 bytes:

A write is done when the device says so, which may only mean its cache has it. A flush is virtio's FLUSH: when it is done, every write done before it is on the disk. The driver asks for that feature when it sets the device up, in three steps that serve any virtio device: start it with the features it wants (it agrees to those the device offers), set up each queue, go live, and the file server flushes before and after each root it writes (sysk 029). Size answers from the device's configuration, without a request. The driver answers "not done" without asking the device for an unknown operation, a sector past the disk's end, or when there is no disk. It fills a fresh buffer, lends it, and waits for the interrupt:

(let live (virtio-start dev block-device feature-flush))
(let q (virtio-queue dev 0 (alloc h ring-bytes) live))   ; a network card: queues 0 and 1
(virtio-go dev (queue-ok q))
…
(let l (virtio-lend dev q b request-data request-status (if (== op #\r) 1 2)))
(while (not (virtio-poll q))
  (invariant (and (running k) (queue-busy q) (lent-for q l) (== (len wants) 3)))
  (let s (alt k wants 2))      ; its one wanted source: the device
  (virtio-ack dev)             ; at the device: InterruptACK
  (device-ack k dev))          ; at the PLIC: the claim completes
(let done (virtio-take q l))

The loop checks first and waits after, so it cannot miss a completion that came before the wait. A stale wake-up costs one more turn. To the deadlock check, a wait on the device is never stuck, as for the UART: the world may signal it at any time.

Tested across reboots

The test system tests/disk has the driver, a client and the printer. The client reads sectors 0 to 3 to see what the last boot left. It writes them again with this boot's number in every byte's pattern and reads them back. Then it asks for a sector past the end, flushes, and asks the disk's size. One fresh image, booted twice:

first boot
disk: boot 1
disk: fresh
disk: 4 sectors written and read back equal
disk: a sector past the end is refused
disk: flushed, 2048 sectors
second boot, same image
disk: boot 2
disk: what boot 1 wrote is there
disk: 4 sectors written and read back equal
disk: a sector past the end is refused
disk: flushed, 2048 sectors

The test also reads QEMU's trace: thirteen requests reached the device (twelve, and the flush), the driver acknowledged its interrupts at the device, and none was left pending. Booted with no disk, the same system answers every request "not done", says disk: not flushed, 0 sectors, and still finishes. make run attaches build/disk.img, a 16 MiB disk, all the file server's format uses, kept until make clean.

The file system on top is a task too: Files on the disk. Not yet: more than one request in flight per queue, and memory regions as capabilities a driver could lend without copying.