The checks · tested

The checker, tested

sysi refine proves that sysi's code does what a model of sysp says: a symbolic evaluator written from sysp's verifier. If the model were wrong, the proofs would be about the wrong thing. This page shows how the model itself is tested: it runs on values, and what it computes is compared with what the same program does compiled by sysi and run on sysr's simulator.

Why test a checker

A proof of refinement relates two meanings: sysi's (its reference, §1-2) and sysp's as the evaluator in sysi/refine.rkt takes it (sysp-region-eval, the lowering, checked). The second is written by hand, rule by rule, from sysp's verifier. A wrong rule (a - read as an addition, a comparison off by one) would not make refine fail: the lowering and the model could agree with each other and both be wrong. Nothing in the proof can notice that; running the program can.

So the model gets a second use. The chain below is what is compared: the model run on values at one end, the machine code run on sysr's ISS at the other. Agreement on a call says that the model, the lowering and the RV64 backend do the same thing on those inputs.

The model, run on values

sysi/concrete.rkt runs the evaluator itself, not a copy: sysp-region-eval is the function refine calls. A call runs region by region, as refine cuts it: from the function's entry, or a loop head, to the returns and loop heads it reaches. The terms a region builds have no free symbols left but the evaluator's own choices, and the events fix those: a call's result is what running the callee gives (or, for put-byte, a model that writes the byte); at an atomic block's entry, other tasks changed nothing; a retype's new rows are the old rows' bytes, read by C's layout with padding zero, and the facts of zero the verifier draws from it, its only quantifiers, are counted out row by row (specs/018). Exactly one exit must be taken; its values start the next region. Each fact the evaluator assumed on the way (the obligations sysp's verifier proved there, but for a product's range, which the evaluator leaves out) is checked on the values.

Here is the docs' example, its run function run that way (recorded by tools/docs.rkt run). A region is listed as it ends, so sum's regions come before the region of run that called it. At a loop head the values are the variables in scope; i-start and i-end are a for loop's bounds, which the evaluator keeps beside i. Step through it:

Random calls, both ways

sysi difftest FILE.sysp ... takes every function whose parameters are numbers, buffers and plain structs (of numbers, public, without variants, an invariant or a resource; specs/024). For each it draws inputs at random (small integers and the literals the contract names, a buffer's bytes from a short list of 0, 255, digits, letters and the characters a parser looks for, buffers of lengths the contract suggests) and keeps those its requires accept, evaluated on the values. A quantifier over several variables runs over the ranges its guard gives them, a bound between two variables carried to both (in i <= j and j < (len a), i is below the length too), and a draw the requires refuse is tried again with its buffers sorted, which is what a search's contract asks (specs/024: the benchmark's binary search had no inputs before). A function whose requires it still cannot evaluate gets no inputs, and is listed. Given the target's extensions (#:exts, specs/026), the code it runs has their instructions where --ext puts them, so a function proven to meet Zknh's predicate is compared, as sysp means it, with the instruction on the ISS (tests/programs/zknh.sysp: 6 functions, 72 calls, the same both ways). Private functions, and those that can reach an extern other than put-byte, are not tested.

It then writes a sysp driver: per call, a function that builds the inputs, makes the call, and prints the result and everything the callee may change (its mut parameters: a buffer's elements, or a number, passed as a variable); dt-run calls them all. The driver, with the program, runs two ways: on the model, each call alone (within 20,000 regions, so a call that does not end is that call's failure), and as sysi's RV64 code on sysr's ISS, with the test runtime's start calling dt_run. Every call must print the same, and no assumption may be false. The driver's machine code, as linked, must also pass sysi validate, so each difftest run checks the backend on code no test program contains.

What it has found

On the benchmark's programs written from a stub, sysk's libraries that do not take the kernel (with sysl's, which they call since sysk 085), arith.sysp, and sysk's kernel and tasks as the gate builds them (make sysk-difftest), every call agreed and every assumption held (counts in specs/007-checker-tested). One assumption was false on the way, and it was in difftest's own driver: it printed a w64 through (as i64 ...), which sysp allows only when the value fits. A bitset function set bit 63, the value no longer fit, and the model reported the cast's assumption false where the ISS printed a negative number. A w64 is now printed as its two 32-bit halves.

It has also found a bug in the backend (specs/008). A branch on a comparison with a constant read the constant from a register whose value had already been replaced; the test programs never compared that way, so the tests did not see it, but difftest's drivers loop to a buffer's length, which is a constant there. Its calls printed differently, and sysi validate on the driver named the block. That is why difftest now validates its driver on every run.

To see whether it would notice a wrong rule, eight rules of the model were broken one at a time, and difftest was run on the benchmark, on sysk's libraries and on tests/programs/arith.sysp. On the first try, four of the eight went unnoticed on the benchmark and the libraries: a remainder computed unsigned, a division by a power of two rounding down, an arithmetic >> on words, and a byte's range one short. On the inputs drawn, those programs never divided a negative number, never shifted a word with its top bit set, and never added bytes up to 255, so a wrong rule there changed nothing they printed. Two changes followed. The input draw now gives a negative integer in about a third of the draws (one in ten before, mostly from −3 to 0), and lets a byte be one of the contract's literals. And arith.sysp was written to reach those corners: every operator on negative operands, division and remainder by powers of two, shifts of words with the top bit set, and byte arithmetic up to 255. With both, each of the eight is noticed by at least one program:

From specs/007 (8 calls a function, seed 1). "differ": calls that printed differently; "false": assumptions of the model found false. When > reads as >=, the driver's own number printing breaks too (its loop never ends), so every call fails.

A part's host program on the machine

Each part's host tests run its host/host.sysp behind a shim that moves records between standard input and output (sysp's tools/host.rkt, built through sysp's C). sysi/host.rkt (specs/030) runs the same program built by sysi on sysr's ISS, so a part can compare the two builds' answers byte for byte, sysq's engine first. iss-host-run takes the part's directory, its sources, the record stream (each a kind byte, a 32-bit little-endian length and that many bytes), the record and answer sizes and the heap's size, and returns the answer stream. It writes a record loop in sysp, which reads the number of records and then each record, calls host-step with it (header included, as the shim does) and writes each answer to the UART. The records are linked into the executable and read in order by get_byte, so no record waits on the UART's timing and every run is the same. The executable is validated before it runs; a panic (the heap run out, say) or a program still running at the cycle limit is an error. tests/host-test.rkt runs tests/programs/echo-host.sysp, which answers each record with the count so far and the record reversed; its Host owns a buffer, so it is a resource, as a part's Host usually is (specs/033: the loop first held the Host in a var, which sysp refuses for one).

Running it

sysi difftest takes the program's files and --cases N (calls per function, 8 unless given), --seed N (1 unless given), --only F and -v (every call, with its inputs and what it printed). It needs clang, ld.lld and sysr beside this repository, as validate's tests do. It exits 0 only if no call differs, no assumption is false and nothing failed to run.