sysi docs · the checks

The lowering, checked

sysi refine checks, for each function of each build, that the sysi the lowering wrote does what the sysp function it came from does. It does not prove the lowering correct once and for all; it checks each output, which is translation validation. A bug in sysi/lower.rkt can still exist, but it cannot reach a checked build (such as the one the gate keeps) unnoticed.

The claim

For each function of a verified sysp program, its sysi refines it: started in related states, every run of the sysi function either does not return or returns in a related state, having made the same calls, with related arguments, in the same order as sysp would. "Related" means that sysp's values can be read off sysi's words and memory, by the layout and the calling convention (the relation α, below). Together with the check of the machine code and sysr's proof of its core against isa.sysr, this carries what sysp proves about a function down to the bits the core runs, with the trusted base listed at the end of this page.

Prior art, and what is different here

seL4's translation validation (Sewell, Myreen and Klein, PLDI 2013) checks the C of a verified kernel against the ARM binary gcc made of it, function by function, finding the split points of loops by search and modelling memory as SMT arrays. Alive2 (Lopes et al., PLDI 2021) checks LLVM's optimizations as refinement with undefined behaviour, unrolling loops a bounded number of times; Bansal's group checks C against x86 from several compilers, inferring the correspondence and the invariants. Their hard parts are the same two: finding how the two programs correspond, and finding loop invariants, because the compiler is a black box to them. sysi's lowering is not: it marks each loop head with a cut, and tells the checker which sysi values hold each sysp variable there. That hint is checked, never trusted: a wrong one makes the check fail. And no invariant is needed at all, for a reason the walkthrough below shows.

Regions, cut at loop heads

A function is cut at its loop heads into regions: one from the entry, and one from each loop head, each running to the returns and the loop heads it reaches. Within a region both sides run symbolically, with paths merged where they meet (an if's join on the sysp side, a block with several predecessors on the sysi side), so a function with many branches costs one set of goals per exit, not one per path. For sum, that is two regions: sum.entry (block b0, up to the loop head b1) and sum.b1 (once around the loop, and out to the return). Here is the head, with its cut:

The cut says that at this head sysp's s is v5 and i is v6. The hint the lowering hands the checker says more: every variable in scope, including the buffer xs (the pair v1, v2) and the loop's own i-end (v2 again, since sysp evaluates a for's end once). The invariants written in the cut are for people reading the sysi; refine.rkt does not use them.

A variable is related at a head only where sysp may still read it: in the loop, after it, or in a loop around it (except one declared inside that loop, which each iteration binds again before reading). sysk's drivers move a buffer into virtio-lend before a loop that polls the device; sysp never reads it again, and relating it there compared sysp's old bytes with memory the device may have written. The region that starts at the head does not have such a variable at all, so a read of it would fail the check, never pass it. mut parameters (read at the return) and shared ones (made fresh at each atomic block's entry) always stay (specs/011). A call's mut and shared arguments are read when it returns, after all of its arguments, so they are read after a loop in one of them, as in (dealloc h (buf-end ...)) (specs/051).

A sysi value that is not a variable of the cut is fresh in the region from the head, unless sysi made it by arithmetic from constants and the parameters alone: then it is the term of its definition in every region, since a value never changes. A table retyped from a parameter's bytes before a loop (as buf-end makes one) keeps its row count as len / size at the head, and so the loop's loads stay inside the parameter's bytes (specs/051).

One region, step by step

Here is sum.b1, the loop region, as the checker runs it: sysp on the left, sysi on the right, and below them the symbolic values each side holds. The names v5⁰ and v6⁰ stand for the fresh symbols the checker makes for the head's parameters; P₁ and P₂ for sum's parameter words; M[a] for the byte at address a in xs's memory. Switch to the mutant to see the same region with one add of the lowering turned into a sub.

Why no invariant: the region starts from any values the variables could have at the head, related by the hint, and not from the ones the invariant allows. It can, because the sysp side assumes every obligation sysp's verifier proved, where it proved it: the addition does not overflow, the index is in bounds. Those facts hold in every run because the program verified, and they are exactly what the invariant was needed for. So the check is of the lowering, not of the program; the program was checked by sysp.

Two evaluators

The relation α

How a sysp value is read off sysi's state, by the layout and the ABI that sysi/abi.rkt defines for the lowering too (alpha, and rel, which turns "v is α of this" into goals):

A buffer read so is a view: element i is a load from memory at the computed address, built only when something reads element i, so z3 rarely sees the whole array. A table (a buffer of structs, specs/015) is what sysp's verifier makes of it: one array for each field, a struct field's fields each an array in turn, the model Burstall and Bornat gave pointer programs. Read off memory, the array of field f is a view whose element i is at the buffer's address plus i times the row's size plus f's offset; setting one field of a row stores into that field's array alone. A bool read from a buffer's memory is its byte not zero, as sysi's branch reads it: nothing tells z3 a buffer's bytes hold only 0 or 1, though sysi's stores and the allocator's zeros keep them so. Equal buffers are a goal over every index below the length, for each of a table's arrays, which z3 refutes, if it can, with one fresh index. Where sysp makes a free choice (a callee's result, what it wrote into a mut argument, what other tasks left in shared state) that value is not a fact to prove but a definition: it is substituted by α of sysi's state at that point, so no quantified fact is ever assumed.

Memory, split by provenance

One array of bytes for all of memory was the first design, and z3 could not prove that two structs do not overlap even for 24 bytes. So memory is split: each region known to be disjoint from every other has an array of its own, indexed by address. A region is a parameter's memory, a slot, an allocation, a string literal, or a buffer read off memory. An access belongs to the region whose base is among its address's addends, and must stay inside it. So a pointer must be the same term on both sides: one read off a small struct's words (a struct of 16 bytes or less travels in registers) is the word itself, not an extract of all its bits, which z3 knows is equal but the lookup does not (specs/036: a struct of one buffer passed through a slot found no region, and the slot was not known to be apart from it; tests/programs/small-struct.sysp). Regions are of three kinds:

• Parameters (and the result's memory, for a function returning through a pointer): each an array of its own. Ownership makes two of them disjoint when either is writable, and two read-only ones are never written, so separate arrays describe them faithfully.
• Fresh: slots, data, and each sysp_alloc, which returns memory no one else has: disjoint from all.
• Others: buffers read off memory. Those read in one place form a group (the fields of a struct after a call that may write it, the call's other arguments, its result; at a loop head, the variables that own or mutably borrow their place). By sysp's ownership, distinct places hold disjoint buffers at one time, so a group's regions get fresh arrays of their own. Only ref and shared variables at a loop head may be one another; those share one array, with a same-or-disjoint fact for each pair.

What refine states of a region (it does not wrap past the top of memory; how it lies to each region it shares an array with) holds wherever the region is named when its base is a parameter, a slot, an allocation or a pointer read off memory, as every one is today. A region whose base or size uses a value chosen where paths meet may be no region on the paths that miss its block, and a fact about it there would make the goals there hold for nothing; so its facts are stated under that block's condition, and a pair's under both (specs/044). The others stay unguarded: guarding them too made z3 give up on a goal of sysk's terminal. Each goal gets the pair facts of the regions it names, found through an index by region: sysk's command has 155,000 of them and 111 goals, and scanning them all for each goal was half its check.

Where paths meet, a value that differs between them is a choice (an ite) over the incoming edges, and is usually named, a word of its own defined as that choice, so terms stay small. A choice among addresses in known regions is kept as it is: a variant built in a slot of its own on each side of a cond, read after the paths meet, is read from each slot under its own condition. Named, the address would belong to no region, and the load would read memory as a whole (specs/010). A choice among constants is kept too: fsd divides by a stride that is 128 or 1, and division by a named word is a circuit z3 cannot decide in time, while division by a choice among constants is a choice among divisions by each, shifts here. And a choice is made by each path's own condition, without the conjuncts all the paths share: where the block is reached those hold, and nothing reads the value where it is not. Otherwise a value merged deep in a large function is a choice by whole path conditions, which z3 must show alike on both sides (specs/011).

A buffer read again after a call may be a buffer known before (the callee kept it) or a new one (the callee swapped it). The earlier region then no longer describes that memory, so it is retired: an access through a pointer read before the call fails the check. The lowering reads a buffer's pointer where sysp names the field, so a correct lowering never does this, and sysk never does. Across a call, what the callee may write (the memory of its mut, shared and own arguments, and its result's) becomes fresh, and everything else stays as it was. A load from such memory at a constant offset from the same base as a fresh range is resolved before z3 sees it, to the fresh byte or the old one: the shell's ask passes one field of its namespace to a call and reads another after, which z3 otherwise had to settle among 4,684 facts (specs/011). A view passed to a callee is the window k − at < n of its buffer on both sides, a form z3 matches without a quantifier, and its bound is n ≤ len − at, which cannot wrap as at + n can.

A call given one row of a table ((net-key k (get ms 0) ...) in sysk's netd) may write that row's bytes only: the memory after it is the call's bytes in that range and the old ones elsewhere. A read of the table at index i is decided by i, the row it lands in (every index is below 2⁶³ divided by the row's size), so the rows the call did not get read as they were, with no quantifier for z3 to unfold. A row taken whole is a well-formed value: its bools, read off memory, are 0 or 1, as a struct's in memory are taken to be (specs/051).

Calls, matched by callee

Each sysp call is paired with the next unpaired sysi call to the same callee (an atomic block's entry is a "callee" too). A call either side makes that has no partner must never happen. Two pairs that the two sides list in different orders must never both happen: on any one path the calls are then the same calls, in the same order. For each pair, both must happen under the same condition, and the arguments must be related (a mut argument as its place holds it when the call is made). Then both sides share what the callee did: sysp's fresh result and the fresh values of its mut arguments are defined as α of sysi's state after the call. The runtime's functions, which sysp does not see, are trusted to keep their contracts: sysp_alloc returns fresh zeroed memory, sysp_free and the interrupt calls change nothing sysp can see.

A retype (sysp 064, specs/018) is paired the same way, with the div the lowering makes for it. sysp's verifier gives the new rows no value, only facts of zero: zero bytes are zero rows where no padding is read, and rows that are not plain bits (a bool, a struct with an invariant) come only from zeros. So the sysp side's new rows are a free choice, defined as α of sysi's memory at the div, as a callee's result is; the buffer before must be sysi's, at the same address with the same length, and the new length must be sysi's. The facts of zero are the layout's, which the verifier trusts too; refine assumes them only where the buffer before is sysi's, so that a wrong address could not make them false and every goal pass. This is the typed heap's retype of Tuch, Klein and Norrish, where bytes take a new type in place. A retype with rows ((retype (buf S) b r ...), specs/051) is the same event with no facts of zero, then each row stored, so nothing is assumed of the bytes it writes over.

The first version paired calls by position in each side's list; sysk's show_file lists a cond's arms in another order than its blocks, and a call was paired with a call to another function. Matching by callee, with the order checked where both happen, came from that (specs/005).

Within one callee, the pairs follow the order in which the lowering made the calls, which is the source's, as sysp's order is; the lowering records it as a hint. The order in which sysi's blocks are run can differ where paths part: in fsd's fsd-open it met the last call to fsd-describe before the one in a branch that returns, and every goal about the two pairs was then false and large. A hint only chooses the pairs; any choice is checked, and the order check still uses the order the blocks run in, which on one path is the order the calls happen (specs/011).

Shared state, at atomic blocks

sysp lets a task touch shared state only inside an atomic block or through a shared argument, and when it enters an outermost atomic block, it assumes other tasks may have changed anything shared (within the rely). The check mirrors that: the entry of an outermost atomic block is paired with the sysi code's sysp_irq_save (in user mode, sysp_user_atomic_begin). There, sysi's shared memory becomes fresh (what others did is now visible), its buffers form a group, and sysp's fresh shared values are defined as α of that memory. Shared values are not compared at loop heads and returns, where sysp allows any.

How z3 is asked

Each region ends in a list of obligations, each a goal under the condition of the path that reaches it (guard ⇒ goal), and a list of facts. Each query runs in a z3 process of its own, given on its input, as is everything refine asks z3, its version included: so SYSP_Z3 may name a program that runs z3 on another machine and takes no arguments (specs/016). Its limit is z3's own count of its work (:rlimit), not time: a limit given in milliseconds is the work z3 does in that time on a quiet machine (about 12,000 units a millisecond for z3 5.1.0, measured on sysk's queries), so an answer does not depend on what else the machine runs. A wall-clock limit far behind it (ten times as long, and a minute more) only stops a z3 that hangs (specs/012). validate's queries have the same limits since specs/013, and both take them from sysi/z3.rkt, which also names the z3 they were measured on: refine's report notes any other. And each z3 that runs waits for one of the slots every z3 check on the machine shares (sysp 047), so the machine runs no more checks than it has processors, whichever session started them; with limits that count work, waiting changes no answer. sysk's queries had to be made small:

1. Facts per goal. The facts about how two regions lie (disjoint, or the same or disjoint) go only to a goal that names both regions; goals that need the same such facts are asked together. A fact left out can only fail to prove, never prove more. For recv, z3 needed 7 s just to place every region in memory for the full set of facts, and the goal needed five of them.
2. A quick form first. Each load from unchanged memory, and each division, remainder and product of two unknowns, becomes a word of its own; two loads of one array, one width and one base are equal where their addresses are (congruence). A goal that holds for every value of those words holds for the loads, so unsat here is a proof; anything else proves nothing. Two tactics are raced: qfbv after simplifying, and smt. The quick form gets at most 2 seconds.
3. Halve what fails. A set that the quick form does not prove is split in two, down to single goals, each of which is asked again with nothing abstracted and the full time limit: first with the facts of how the regions it names lie, then with every fact. Most of a large function's facts are those of how its regions lie, over 10,000 of the 10,712 in fsd's session-write, and leaving facts out can only fail to prove (specs/011).
4. Terms written one way. An address is its region's base, then the other addends in a fixed order, then the constant; a constant goes last in sysp's + and * as in the lowering's; a division by a power of two is a shift with its rounding correction. Both sides' loads of one byte then are one term, and a load through a store resolves to an if on whether the addresses are equal, before z3 sees it.
5. Vacuity. Last, the facts the proofs used are checked to be satisfiable together. If they contradict each other every goal is "proven", so the check reports "the region's assumptions contradict each other" instead. This caught a real checker bug: a slot that was a region twice, disjoint from itself. The tests check every fact, not only those the proofs used, so a wrong one fails there whichever proofs needed it; that found a second (specs/010): a view passed as a mut argument became a region of its own after the call, said to be the same as its buffer or disjoint from it, though it lies inside it. A region whose address is a known base plus more is now that region. Only sat passes: until specs/011 an undecided check passed, and on sysk about a hundred functions had facts z3 could not show consistent in 2 seconds. It now has the full limit, and is first asked with every region placed at an address of its own, far from the others: facts consistent with more added are consistent, and z3 finds a model at fixed addresses far sooner than it searches for a layout (sysk's yield: 0.8 s against 12).

What is assumed

• The program verified: each obligation sysp's verifier proved holds where it proved it.
• Ownership: distinct places do not overlap. Two parameters where either is writable, an allocation and everything else, distinct allocation sites, the buffers a struct's fields (or a call's arguments and result) hold at one time, the variables in scope at a loop head except ref and shared ones.
• The caller's pointers point outside the function's frame; a buffer's bytes fit in an i64.
• The runtime's contracts (sysp_alloc, sysp_free, the interrupt and atomic calls), and the layout and ABI of abi.rkt, taken as the definition of the convention.
• The evaluator's rules agree with sysp's verifier; and z3. (The rules are tested against running code, but not proven: the checker, tested.)

A cell-swap (specs/025) is one more such event. sysp's verifier models a cells array by its lengths only, so the buffer that comes out has the cell's length and contents left open. refine pairs the swap with two of sysi's instructions. At the load of the old length, where both of the cell's old words are known: the lengths must be equal, the address must be the word before that length, and the open contents are defined as what sysi's memory holds there, a region of its own apart from the cells. At the store of the new length: the cell's two words must be sysp's new buffer, stored where the old length was loaded. The first version checked the lengths only, and refine-test's mutants found what that missed: an old address read one byte off, and a new address not stored, were accepted. With it, every sysp form is checked: sysi refine says "ok" only when every function was, and one too slow (over --budget-s) makes the result "incomplete".

Does it catch wrong lowerings?

tests/refine-test.rkt first checks that every function of the features program refines its sysp function (all 36 of them, run's cell swap included since specs/025). Then it makes mutants of the lowering's output, one change each: an operation swapped (add for sub, lt for le, …), a constant plus one, a load's or store's offset plus one, a store dropped, a branch's targets swapped, a call's or a jump's first two arguments swapped, and, for a jump out of a loop as a break makes, the jump sent to the loop's head instead, or given the head's values. It checks every third mutant of every function but run, the program's driver, whose forms the others have and each of whose mutants would check all of it (all with MUTATE=all), and every mutant of the functions that use enums, views and break (specs/009) or tables (specs/015) or retype (specs/018) or a cell swap (specs/025), and of shape_of, which makes a variant in a slot of its own on each side of a cond (specs/010). Each mutant the check accepts must be an equivalent one: the test builds it with the RV64 backend and runs it on sysr's ISS, and it must print what the original prints. The mutants run in places side by side, and a sweep that passed is not run again until what it reads changes (specs/019; Commands, build, tests).

The test's run in specs/011 (earlier ones are recorded in specs/004, 005 and 009): 1,068 made, 449 tried, 439 rejected, 10 accepted, each running as the original: a constant 0 made 1 in put_num's block b3; two or made xor (in big_total and many), of bytes that do not overlap; in many's entry block a shl made shr and two add made sub; and four jumps of the new functions: two entry jumps whose swapped arguments are both zero (total, count_to), first_zero's break, whose two arguments are equal there, and count_to's break given the head's values, taken before the loop has changed any. In specs/019, with tables and retype in the program: 1,255 made, 566 tried, 554 rejected, 12 accepted, the same ten and two in the functions with tables (row_on's entry jump with its arguments swapped, a constant 1 made 2 in row_set), each running as the original. In a sample of 22 mutants of two kernel functions (specs/005), 11 were rejected, 9 ran out of time, and the 2 accepted changed loads whose values nothing uses.

The example's mutant above is one of these kinds. On sum it is rejected as shown:

And on the whole of sysk, kernel and tasks, at the last gate (Every build checked):

A function found to refine is kept, in the store every checkout shares (tools/store refine, beside sysp's proofs), by everything its check reads: its sysp text and each definition it names (a callee by its signature and contract), found as sysp's cache finds them, in the sources and in the texts their layouts made, which sysp's store adds itself when it is opened (sysp 110), and refine reads a layout's function's own text from there too (specs/052: tests/programs/layout.sysp, a layout's functions refined twice with a store, checks it); the part of sysp it reads, which is sysp's front end (the files check-sources runs before the verifier, found by what they load) and not the verifier or its prover; and its sysi, its hint, sysi's sources, the z3 that runs and the limits. refine writes its queries' text itself. A change to sysp's proofs alone (sysp 097's write sets, 099's bound) then keeps every result (specs/045). A gate then checks again only what changed; a failure, or a function too slow, is never kept (--results, specs/013).

Through specs/008 every one of sysk's functions checked. The largest then, the shell's command, with 22 calls, took 41 s when specs/005 was written. Since specs/009 sysi lowers all of today's sysk. Until specs/010 refine ran out of memory on the shell's watching (sysk 049): terms share their parts, and an address there of 5,337 distinct nodes is 2.2 billion as a tree, which ordering addends by their printed form walked. A term now has an id, from its head and its children's ids, so ordering takes time linear in the term as it is shared, and a function too large is reported too slow, never killed. The gate then ran to the end, with 15 functions it could not check; specs/011 took them (the changes above marked so), and with it all 574 of sysk 061 checked, in under six minutes with eight side by side on a quiet machine; the shell's command, the largest, takes about two minutes alone; under heavy load they could miss their limits until specs/012 made the limits count z3's work, not time. The example's own run, with -v, which names each function as it is checked: