IO and drivers

Lines on their way out

Every line on the screen comes from the shell (sysk 018): its own replies and prompts, and every line its jobs send on out, the pool channel it reads them on. It sends them on its stream answers to the terminal, the one task that writes to the UART driver, on the stream screen. Press Play to watch the lines of the last make docs take that way; the kernel's ring for screen fills as lines wait for the driver.

A line is a message

A line is a buffer of 64 bytes: byte 0 holds the length, bytes 1 to 63 the text. Tasks build lines in their own heap with lib/text.sysp (line-set, line-text, line-u for decimal numbers), all verified with no hand-written invariants, and send each as one message. The driver adds the newline. Because a line is one message, lines from different tasks can never interleave, and nothing needs to hold off the timer while a task prints.

Neither the terminal nor the driver decides how anything looks. Since sysk 044 each answer says what it is, in the two top bits of its length byte: text, a value, or the shell's own (the prompt, the region that follows). On a plain line the terminal shows them as before: text as it is, a long value wrapped between its fields, and the prompt as an unfinished line, which the driver writes without the newline, so the person types after it. A host that says (syst 1) gets them as messages instead, and lays them out itself (syst).

A system with no input needs no terminal. There the UART goes to drivers/uart-printer.sysp, which receives lines on one shared channel and writes them, as every task printed before sysk 015. The pipeline system in tests/pipeline works that way.

Who does IO, before and after

A device is a page

A device's registers sit in one 4096-byte page of the address space. Since sysk 023 the capability for a device is that page: (private struct Device (base i64)) in kernel/devices.sysp, the page's base address. Only device makes one, and it takes a Wire, so only the generated wiring can: for (task uart-driver (device uart) …) it writes (device w 268435456), the base from arch/rv64/devices.sysk. device ensures the opaque predicate device-ok: the base is a multiple of 4096 and below 4 GiB. A driver carries device-ok from its requires to every register access.

A driver reaches its registers with four functions, each a load or a store at an offset into the page. Their contracts prove the offset is inside the page, and for the 32-bit ones that it is a multiple of 4:

Each adds the offset to the Device's base and calls a trusted extern: load8, load32, store8, store32, one or two instructions each in arch/rv64/platform.S. The externs are private to kernel/devices.sysp, so these four functions are their only callers, and the base is a private field, so no driver can read it, change it or make a Device of its own (N003). A driver can name an offset into its own page and nothing else: there is no address in its hands to get wrong. The fences matter for a device that reads memory itself: store32 fences before telling the device to look, and load32 after reading the index that says the device is done (Storage).

The UART's driver is sysp all the way to its registers: uart-tx, uart-rx, uart-rx-on and write-line are sysp functions in drivers/uart-write.sysp, on an NS16550's offsets: 0 the byte received or to send, 1 the interrupt enable, 5 the line status. Each register and bit has a name, a constant (sysp 021), so the code says which it means: (mmio-read8 dev uart-status), status-room. Before sysk 023 the first three were trusted assembly in platform.S; a second device that way would have added its own, and now each new driver adds verified code instead.

Three locks on one device

1. The type system. Touching a register needs a Device, which only the wiring makes, with the base the platform file gives, for the task the manifest names. tools/wire.rkt refuses a device handed to two tasks. The four accessors prove each access lands inside that Device's page.
2. The interface. kernel/interface.sysk lists the device names in one clause, (device page (types Device Queue Lent) (preds …) (calls device-ack) (library mmio-read8 … virtio-lend …)), and tools/interface.rkt lets only files in drivers/ use them.
3. The hardware. The device's page comes from arch/rv64/devices.sysk. ctx_init makes it PMP entry 7 for the holder only; every other task faults if it stores there, and a test checks that it does.

The type system and PMP name the same page, because the wiring writes both from the same line of devices.sysk: the Device's base, and the region ctx_init loads for that task. They guard against different mistakes. PMP holds even if a driver's proof were wrong, or the trusted store8 were: a user-mode access outside the task's regions faults, whatever the code meant. The proof holds before anything runs: a driver whose access might leave its page does not compile, so it never faults on a register, and a driver can only say which register, never which address. Neither covers a device that reads and writes memory on its own (DMA): PMP checks the CPU's accesses, not the device's. For the disk, what the device may touch is proven instead; see Storage.

The platform's devices

The devices a system may hand to a task, as QEMU's virt board has them: the UART, since sysk 023 a virtio block device, the disk (Storage), and since sysk 046 a virtio entropy device, /dev/rng (Devices as files). One PMP entry covers a device's page, and the accessors' proofs assume a page of 4096 bytes, so each page is 4096 bytes, aligned, below 4 GiB; wire.rkt checks that. A device that interrupts names its PLIC source, which reaches only its driver; a driver acknowledges with device-ack.

Input

The driver also receives. The UART's interrupt reaches it and no other task, it sends each byte it reads on keys, and the terminal makes lines of them for the interactive task. Input follows a typed line the whole way.