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.

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. Equal buffers are a goal over every index below the length, 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. 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.

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.

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.

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).

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, from a file, with z3's wall-clock limit and the checker's behind it, so no query can hang the next. 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 every fact and nothing abstracted, with the full time limit.
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.

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.)

Does it catch wrong lowerings?

tests/refine-test.rkt first checks that every function of the features program refines its sysp function (at least 18 of its 19; the 19th has the cell swap). 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. Of the 668 mutants it makes, it checks every third (all with MUTATE=all). 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 test's last run (also recorded in specs/004 and specs/005): 222 tried, 216 rejected, 6 accepted, each running as the original: a constant 0 made 1 in put_num's block b3; three or made xor (in tiny_make, big_total and many), of bytes that do not overlap; and in many's entry block a constant 3 made 4 and a shl made shr. 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):

Every one of sysk's functions checks. The largest, the shell's command, with 22 calls, took 41 s when specs/005 was written; before that work, 39 of the 280 were undecided or over a minute. The example's own run, with -v, which names each function as it is checked: