Build, tests, docs

What you need

• ../sysp, next to sysk, with Racket and the Z3 solver on your path.
• clang with the RISC-V target, and ld.lld. Apple's clang has no RISC-V backend: brew install llvm lld qemu, then pass CLANG=$(brew --prefix llvm)/bin/clang LLD=$(brew --prefix lld)/bin/ld.lld.
• qemu-system-riscv64.

From sources to a running machine

What make does, and make run-proven after it, in order. Every check comes before any machine code is produced: a system that fails one is never built. make run skips the proofs and the model (sysk 070): it checks types, names and contracts, builds apart in build/unproven, which no proven target reads, and says before the boot that nothing is proven, so a store gone cold after a change to sysp never keeps anyone from typing at sysk.

The board

make board (sysk 098) builds the system for the ULX3S, sysr's RISC-V core on an ECP5 board: boards/ulx3s.sysk, the shell's system without what the board does not have, a disk, an entropy device and a network card, so without fsd, the rng's /dev and netd, and with the catalogue's programs that need no service. It is proven and modelled as the default system is, into build/ulx3s/, and linked by arch/rv64/link-ulx3s.ld. The board's first 384 KiB are block RAM, which the bitstream loads and the only memory instructions are fetched from, so the image, code, constants and data, goes there, and the link stops if it is larger; make board says how much it takes (282,632 bytes today). Above it, in the board's 32 MiB of SDRAM, whose contents are unknown at power-up, go .bss, which boot.S zeroes, and the heaps, which never rely on memory being zero. The shell is written for three tree servers, the disk's, /dev's and /net's; on the board each is an empty tree, svc/none.sysp's none-serve run as three tasks (none, none-dev, none-net), a directory with nothing in it, until the shell's namespace takes the servers its profile mounts, as many as there are. Nothing in the kernel knows the board: its UART, timer, PLIC and test device sit where QEMU virt's do, so the same image boots on QEMU (the board test does that), and sysr's make sysk-ulx3s runs it on the board's core against its instruction-set simulator. There it first never reached its prompt: memcpy copied a byte at a time, and every kernel call that reads the kernel's state copies its 384 bytes, so one task's poll took two of the 15 MHz core's 1 ms quanta; copying by words (sysk 100), the board's session ends in 1.25 million cycles, which a board test now checks on the core's simulator.

Through sysi

make check and make test build the kernel a second way (sysk 097, Retire C step 1): sysi asm turns the same sources into RISC-V assembly, build/sysi/kernel.S, with no C compiler, after build/kernel.c, so it reads the proofs sysp has kept; it is assembled and linked with the same gates and trusted assembly into build/sysi/sysk.elf. sysc's keyed code is given --clear-cases, so it clears the stack and the registers it used on return. The image is accepted, build/sysi/gate.ok, only when both of sysi's checks pass on it: sysi refine, that each function's lowering does what its sysp says, and sysi validate, that the linked machine code does what the lowering says, block by block, by sysr's description of the instruction set. Their reports are build/sysi/refine.txt and validate.txt. Then tests/sysi-test.rkt types the README's session (a line into a file, wc on it, ls /prg) into both images, each on a fresh disk, and compares what they print. Each check keeps a function it passed by what its check reads, refine in tools/store refine and validate in tools/store validate, validate keying the machine code by the symbols it reaches and not by where it lies (sysi 039). A warm gate checks again only the functions that changed, in under a minute. Plain make and make run stay on C, which every other test boots, until the switch, step 2.

The tests

make test runs its test files side by side, up to four at a time (eight before sysk 102: the machine is shared by every part's gates), each building into its own directory under build/test/, and only those whose files changed: ../tools/tested.rkt notes every file a test file reads, through the racket programs it starts too (tested-racket), and keeps a pass by their hashes, so a file that read the same as when it last passed is not run again (sysx 101, sysk 096). sysp's sources count for a test that runs sysp, and the versions of clang, lld, QEMU and z3; lld's link script is read by the test itself, since what lld reads is not seen. tests/make-test.rkt reads what make run would do from make -n, and make starts racket unseen, so it is a file of its own, a few seconds run every time; the disk's systems are a file of their own, tests/disk-test.rkt, and so are the systems of servers with several clients, tests/clients-test.rkt, so they boot beside the others. An image is built once per run for what goes into it, each source by its name and text, so the boot tests that build the same kernel build it once. Output order on QEMU depends on timing, so the boot tests check properties (each job's output whole and in order, its end reported; the spinners interleave) rather than a fixed transcript, and compare the shell's replies with its prompts stripped. A boot feeds the serial line its input, by default just 0x04, the end of input; the session test types commands at the shell (sysk 018): pipelines on one line and over three, a program alone, every refusal followed by a command that runs, a command left open when input ends, the listings; the same session typed as sugar and as s-expressions must give the same jobs, and a small system with a recorder checks what sugar makes of a table of lines. The time system in tests/time (sysk 022) checks the clock against the host's, and the shell's (uptime) and (sleep) are typed at it. The storage system in tests/disk (sysk 023) is booted twice on one fresh disk image: the second boot must find the sectors the first wrote, QEMU's trace must show every request answered by an interrupt and acknowledged, and without a disk every request is refused and the system still finishes (Storage). boot in tests/common.rkt takes #:disk, #:trace and #:trace-log for that. The file server's systems in tests/fsd (sysk 029) are booted twice on one disk, with a small file and with one past an index sector; booted with a recorder that cuts the power at every one of their writes, cut clean and torn, each run must find a state the changes went through, never an earlier one than a later cut; and five damaged disks must be refused. The shell's files are typed at it across two boots (Files on the disk). A launcher lends parts of the tree to jobs, and a probe job reports what it may and may not do; wc is typed at the shell with a path, a missing one, one of the kernel's, none, and with its line into a file (Files for jobs, sysk 031). A job is run in the background while file commands are typed beside it, and input ends beside one; both must show the job whole and finish (The shell, sysk 032). follow is run in the background on a file that grows: each line once, a second job refused, and its end at least five seconds after the last change (Reads that wait, sysk 033); in the foreground it is stopped by Ctrl-C, and wc on the same file runs after it (The shell, sysk 074), and so it is behind five lines typed ahead, more than the terminal, sugar and the commands hold, while a Ctrl-C at an empty prompt stops nothing later (sysk 084). A line ending in ?? says what its command is, a program's spec and doc, a part's command, a path's entry, the catalogue, and runs nothing (The shell, sysk 075). The systems with a terminal on its own (tests/board, tests/sugar, tests/terminal) give its interrupts to their receiver, which reads them to their end. The pipeline system in tests/pipeline is booted and checked too, and so is the jobs system in tests/jobs (sysk 017): a launcher that runs ten jobs in one pool and has seven refused, one for each reason; and tests/waits-test.rkt runs the deadlock rule against the exact check on 300 small systems generated at random. Tests that check one mistake run against a small system, tests/small.sysk (the printer and one spinner), which proves in a few seconds instead of the whole system's seconds. All of them share the proofs make keeps, in the store every checkout of the suite shares (../tools/store proofs): each function is proven once, by whichever build or test reaches it first, and a test that adds one mistake proves only that again. A failure is never kept, so every negative test still sees its error. Each test's sysp proves two functions at a time, not one per processor, since eight test files run side by side; and a proof run is stopped only after half an hour (PROOF-TIMEOUT), a z3 that has stopped answering, so a machine busy with other sessions' proofs slows the tests but does not fail them. A function's proof may take at most 50M units of z3's work, the suite's budget (sysp 059, 061); the few that take more, each a loop that serves a protocol, are listed in work.allow with why, and make and the tests pass it to every sysp they run.

How these docs stay current

There are two kinds of content on these pages, and each has its own guard.

1. Facts read off the code. Numbers, lists, tables, quoted code and every page's In the source section come from docs/site/data.js, which tools/docs.rkt generates from the sources: the manifest, the interface, the devices, each definition with its doc comment and contract, the model's state graphs. It is made, never kept (sysk 072): make data, make docs and make docs-check make it, and so does the suite's publishing, so a landing elsewhere that moves a fact changes nothing in sysk's tree. What needs a build and a boot (the verifier's counts, a transcript, the memory map read from the ELF) is in run.js, kept and refreshed by make docs when sysk finishes a feature. A page names each fact it shows by its path, data-fact="manifest.tasks.length" or data-run="check.obligations", and a test checks that every one is there, not what it says. The manual, Commands, is read from the wiring the manifest makes, each program's file in /prg as the kernel serves it, and a test checks it has one for every program of the catalogue: the wiring once came out empty, since wire.rkt was not handed the other parts' files a runner reads (sysc 014), and every fact was still there (sysn 032). It proves nothing: the verifier's counts are the report the build kept, build/check.json (sysp 058), and the time a whole proof takes, which a build from the store cannot say, is kept as it was measured last; make docs FRESH=1 proves everything again to measure it (sysk 066).
2. One look across the suite. The stylesheet and the script every page shares (the suite's row of parts, the rail, the pager, facts, In the source) are sysx's docs kit, loaded from the root's kit/; this site's site.js keeps only its pages and its data (sysk 034; one kit, with no copy, since sysx 010; the suite).
3. Prose. Each page names the files it explains, in <meta name="covers">. A test fails if a source file is explained by no page, or if something a covered file defines changed since the page was last reviewed: a definition's signature or contract, an assembly entry point, a manifest clause, a tool's usage, a test's name. The failure says which page, which file and what changed. Reread the page, fix what is wrong, then record the review: racket tools/docs.rkt review ../sysp PAGE.html. Function bodies are not tracked; contracts are what the pages explain. Another part whose code is in sysk's image keeps its own site the same way: --root ../sysh checks ../sysh/docs/site against sysh's own files, what git keeps there of these kinds but its docs, specs and tests' directories (sysk 122).

A change to the docs, the specs or Markdown alone runs this same make docs-check at landing instead of make test (sysx 029): the facts made and the pages read against the code, then the tests that read the docs: every fact a page names is there, and docs/trusted.md's line count.

Recipes

Add a task

1. Write prg/name.sysp (a service's goes in svc/, sysk 045): one function taking the kernel, then what it needs, with a precondition that states its protocol ((tx-left out 3) or (tx-stream out), (tx-bytes out 8), (heap-budget h 10)). One task function per file, with its helpers: the build takes a file only if the manifest names its task, or a file it takes calls it (wire.rkt --uses; sysk 033: prg/files-client.sysp, for wc and follow).
2. Add a (task name …) line to system.sysk and give the channels' counts room for it.
3. make check: sysp proves it, the interface check reads it, the model checks the new system can finish.
4. Add the file to a page's covers (the docs test asks you to), write about it, make docs, review.

Add a kernel call

1. Write it in kernel/sched.sysp with its contract; it may touch kernel state only inside atomic, and every atomic block must keep the rely.
2. List it under calls in kernel/interface.sysk; it becomes a gate, numbered by its place in the list.
3. Add a negative test showing what a task still cannot do.