Devices and the platform
The SoC's devices are written in sysr like the core: a 16550 UART subset with a real serial line, and a PLIC whose claim is proven to pick the right source. Their register layouts are functions the SoC decodes addresses with, and their properties have names. From both, tools/platform.rkt generates what a kernel compiles against, and a contract that turns assumptions in sysk's trusted base into proven statements.
uart.sysr and plic.sysrcustom.S)The obligation counts are what sysr check devices/uart.sysr --top uart and --top plic printed when this page was written.
The UART: devices/uart.sysr
The UART is the subset of a 16550 that QEMU's virt machine has and sysk uses: 8 data bits, no parity, one stop bit, at a fixed rate of div clock cycles per bit (a module parameter; there is no divisor latch). Its registers, by address: 0 is RBR when read (the oldest received byte, popped by the read) and THR when written (send a byte, if the transmitter is idle; a write while it is busy is lost); 1 is IER, the two interrupt enables; 2 is IIR; 5 is LSR, with data ready in bit 0, overrun in bit 1 and transmitter idle in bits 5 and 6. Received bytes go into a 16-byte FIFO. Both interrupts are levels: received data while enabled and waiting, transmitter idle while enabled and idle.
The serial line is real, and its timing is exact so that the ISS can model it to the cycle. Type a byte to see its frame. A byte written to THR in cycle c is on tx from cycle c+1 for ten bit times, lowest data bit first. The receiver, seeing a start bit begin in cycle b, checks it half a bit in and samples each later bit in its middle.
tx; the dashed green marks are the cycles in which a receiver with the same div samples it, by the timing in uart.sysr's header. Enter one character or a hex byte such as 0x0a.What is proven about it
These are the UART's named properties, read from uart.sysr as it is. Each is an invariant over every reachable state, proven by k-induction; the unnamed ones beside them keep the counters in range. A driver relies on the last three: the receive interrupt is exactly "enabled and data waiting", and LSR tells the truth about data and the transmitter.
The programs that drive it poll exactly these bits. This is the core's hello.s, which waits on LSR bit 5 before each store to THR, and what the ISS printed when the docs were built:
cores/rv64im/programs/hello.s
racket tools/rviss.rkt hello.s
The PLIC: devices/plic.sysr
The PLIC collects interrupt lines and hands the core one at a time. It has 32 level-triggered sources (source 0 does not exist) and one context, hart 0 in machine mode. Each source has a priority from 0 to 7 (0 never interrupts) and an enable bit; the context has a threshold. A source whose line is high and that is not claimed is pending. Reading the claim register returns the highest-priority pending enabled source above the threshold, the lowest id among equals, or 0, and claims it: it is no longer pending until the driver completes it by writing its id back.
The hardware finds that source with a chain: b0 is 0, and each bi is i if source i is eligible and its priority is strictly greater than that of bi-1, else bi-1. Strictly greater is what sends ties to the lower id. Try it: raise lines, change priorities, enables and the threshold, then claim and complete. The UART is source 10.
b1 to b31: green where it changes.plic.sysr's registers in your browser: pending is the line and not claimed, the chain is the b0…b31 lets, a claim sets the claimed bit of best, and a completion clears the written id's bit only if that source is enabled. "level" is the source's input line, "en" its enable bit.What is proven about it
The first group says the claim is right: best-none, best-eligible and one best-max per source together say that the source returned is eligible and that no eligible source beats it. The second group is what sysk relies on: a claimed source forwards nothing more until it is completed, and a completion the PLIC did not issue changes nothing. The PLIC requires that an access is a read or a write, not both; a counterexample found that one: a claim and a completion in the same cycle lost the completion.
The properties were tested by planting bugs. The proofs caught ties going to the higher id, a claim that does not quiet its source, a completion of a disabled source, a FIFO that takes a byte when full, a line that is not high when idle, an overrun not always flagged, and bytes with bit 7 clear never sent. The disabled completion was missed at first, because the property was stated with the implementation's own complete signal; the properties are now stated from register accesses, which is why they mention wr, claim-at and wdata.
One SoC
cores/rv64im/soc.sysr puts both devices on the core's I/O bus with the test device: the UART at 0x10000000, the PLIC at 0x0C000000, decoding address bits with the same uart-base and plic-base functions that cores/rv64im/platform.sysr defines. The UART's interrupt line is PLIC source uart-irq, and the SoC proves that as a named invariant, virt.uart-source. The ISS models both devices to the cycle, and every run of the SoC, sysk's boot included, is compared with it register for register and byte for byte on the serial line (The ISS and the comparisons).
The platform: what a kernel compiles against
A kernel needs the hardware's numbers: where RAM is and how big, the UART's address and register offsets, the PLIC's offsets, which source the UART is. Written by hand, they can drift from the hardware. tools/platform.rkt reads them from the sysr sources the SoC is built from, with sysr's own reader, so they are the numbers the hardware decodes with, not a description of them. The sources are:
It writes one directory per platform, platform/virt (QEMU's virt machine, which the SoC was built to match) and platform/ulx3s (the board), and only after sysr check has proven the platform's top. Each file starts with its provenance: the sysr version, the platform, and the first 16 hex digits of a SHA-256 over the sources.
| File | For |
|---|---|
devices.sysk | sysk's device list: each device a system may hand to a task, with the page its driver's PMP entry covers and its PLIC source |
platform.sysp | the numbers as sysp functions whose contract is their value, and the custom instructions (Custom instructions) |
platform.inc | the same numbers as .equ lines for the trusted assembly |
CONTRACT.md | what a kernel may rely on: the map, the custom instructions, and the named properties with their text |
custom.S | ulx3s only: the custom instructions as functions |
Every constant of platform.inc, where it comes from, and its value on each platform, read from the generated files. They differ only where the boards do: RAM's size. The board's RAM comes from its ram-words; mtime is 10 MHz on both, QEMU's timebase on virt and 2 of every 3 cycles of the 15 MHz clock on the ULX3S (On a ULX3S).
| platform.inc | from | virt | ulx3s |
|---|
Copied, checked, required
sysk copies a platform directory into its own tree rather than reading ../sysr, so it builds without sysr, and a change of hardware arrives as a diff it can review. --check-dir DIR regenerates the files without proving and reports each one that differs or is missing; make platform-check SYSK=../sysk runs it on every copy it finds. --check SYSK instead compares numbers sysk still writes by hand (its devices.sysk, constants and plic-write offsets in kernel/sched.sysp, the .equ lines of its assembly) with the hardware's.
The kernel states what it relies on in its own file, requires.sysk: each statement in its words, with the properties that carry it (platform/requires.example.sysk is sysr's example). With --requires, CONTRACT.md lists exactly those statements, and generation fails if a property they name is not in the hardware, so a property renamed in sysr shows up as a failed regeneration in sysk, not as a silent gap.
What moves out of sysk's trusted base
sysk's docs/trusted.md assumes, about QEMU's virt machine, the PLIC's layout; that a claimed source forwards nothing more until it is completed with the same number, and a completion the PLIC did not issue is ignored; that the UART raises its interrupt while its receive FIFO holds data; and that its device list gives each device's page as the machine has it. On the SoC, the layout and the device list are generated from the hardware's sources, and the behaviour is proven: plic.claim-quiets, plic.claimed-silent, plic.complete-releases, plic.complete-only-own, plic.unissued-ignored, uart.rx-level and the rest, which CONTRACT.md cites.
What stays trusted. The assembly that touches the registers must do what its comments say, with these numbers. And on QEMU, where sysk also runs, the statements remain assumptions about QEMU: the numbers are QEMU virt's (the SoC was built to its map), but the properties are the SoC's devices'. That QEMU's devices behave the same in what sysk uses is tested, by sysk running on the ISS's models of them, not proven.
tests/platform-test.rkt checks that both directories are what the sources generate now, that every file carries the provenance, that the platforms differ only in RAM size, that a missing property in the requirements is an error, that an edited or missing copy is reported as drift, that the ISS (written independently) has the hardware's map, and that --check finds the three wrong numbers planted in a small sysk tree.