Using sysi · the lowering

From sysp to sysi

sysi/lower.rkt turns a verified sysp program into a sysi module. It decides how each sysp value is held in words and memory, lays out structs as C does, passes arguments by the RISC-V calling convention, and turns sysp's structured control flow into blocks and jumps. It can be simple because sysp has already proved the program safe, and it leaves hints so that its output can be checked.

What the lowering starts from

The lowering does not parse sysp itself. sysi/sysp.rkt loads sysp's own driver, AST, types and checker from the sysp checkout beside sysi (../sysp), and sysi lower first runs sysp's check on the files, verification included. It stops if sysp reports any error. What the lowering receives is the checked program: every expression with its type, every variable resolved to its binding, and each for already rewritten by sysp into a while with its own counter and bounds. The entry point is lower-program, which returns a module that sysi lower then checks for well-formedness (The IR).

Types become words

Every sysi value is a 64-bit word, so each sysp type needs a representation in words (docs/reference.md §1):

A word narrower than 64 bits is kept zero-extended. Most operations keep that by themselves, but +, -, * and << on a w8, w16 or w32 can carry bits above the width, so the lowering masks after them, and ~ is an xor with the width's mask:

There is no such mask for i64 or u8: sysp proves their arithmetic does not overflow, so the plain 64-bit result is already right. A struct is not a value in registers at all: it is the address of its bytes. Binding a struct from a place ((let g2 g)) copies it into a fresh stack slot, field by field, so the two do not share memory; a struct that new or a call just made is fresh already and is not copied. A variable whose address is passed on, as a mut argument, also lives in a slot instead of being a value.

C's memory layout

Structs are laid out exactly as a C compiler lays them out on LP64, so that sysi code, sysp's own C, and assembly written against C's headers all agree on where a field is (docs/reference.md §4). The rules are in sysi/abi.rkt, in compute-layout: each field at the next multiple of its own alignment, the struct's alignment the largest of its fields', and its size rounded up to that alignment. A struct with no fields takes one byte.

Try it. The figure computes a layout with the same rules as compute-layout. It starts from the structs in tests/programs/features.sysp, read from the file; change a field's type, reorder the fields or add one, and watch the padding move.

Reordering is the quickest way to see the rules: in a struct of a u8, an i64 and a u8, the i64 must start at 8, so the struct is 24 bytes; put both bytes first and it is 16. sysi does not reorder fields: C does not, and the layout must be C's.

The calling convention

Every function sysi produces can be called from C or assembly, and can call them, because its parameters and results follow the RISC-V LP64 convention applied to sysp's signatures (docs/reference.md §5). param-abi and ret-abi in sysi/abi.rkt decide how each travels:

This is why the tour's sum has two parameter words for one sysp parameter. A small struct passed by value is packed into its words: the lowering loads each field and shifts it into place (struct->words), and the callee unpacks the words into a slot of its own (words->struct). The figure above shows that packing for structs of up to 16 bytes. The same functions in sysi/abi.rkt are used by the lowering, by both backends and by both checks, so they agree by construction on what the convention is; sysi refine takes them as the definition of the convention rather than checking them.

Expressions, control flow and calls

The lowering walks each function body once, carrying an environment that says where each variable is: a value (or two, for a buffer), or a place in memory. An expression gives back its value as zero, one or two words. Pick a construct below to see it in the tour's run function, its sysi, and the part of sysi/lower.rkt that produced it.

• Operators are one instruction each: + is add, < is lt, / is div. (get xs i) is an address computation and a load; (put xs i v) a store; for elements wider than a byte the index is shifted first. (len xs) is the buffer's second word and needs no instruction.
• and, or and => branch, as in C: the right operand runs only when it must, so its effects happen only then.
• if becomes a br to two new blocks and, when an arm continues, a join block. When both continue, the join's parameters are the if's value and every variable the arms left with different values (merge!). An arm that has returned does not jump to the join.
• while becomes a loop head whose parameters are the variables the loop assigns (only those held as values; one in memory needs none), the condition with a br into the body or out, and the body jumping back with the variables' new values. A (while true ...) has no exit block.
• for is a while by the time sysi sees it: sysp rewrites (for (i lo hi) body) into a start and an end evaluated once, a counter i starting at the start, and (while (< i end) body (set i (+ i 1))) with the invariant (<= lo i hi) added to the loop's own.
• Calls pass each argument by param-abi: a scalar as its word, a buffer as two, a small struct as its packed words, a large one as the address of a fresh copy, and a mut or shared argument as the address of the caller's place. Results come back the same way; a large struct result is written to a slot the caller passes as an extra first word. A call to a function that never returns is followed by unreachable.
• The platform: buf-new and cells-new call sysp_alloc, asking for at least one element; free calls sysp_free; cells-free calls a helper the lowering adds to the module, sysi_cells_free, which frees each cell's buffer and then the cells; atomic brackets its body with sysp_irq_save and sysp_irq_restore.
• Specifications are not code. requires, ensures, assert, assume and invariants produce no instructions; invariants are only copied into the cuts. A return ends its block. Code after a terminator goes into a fresh block, and blocks that cannot be reached from the entry are dropped at the end.

What the lowering relies on

sysi's lowering adds no run-time checks. Each of these choices is correct only because sysp proved something about the program; that is why sysi lower refuses a program that does not verify (its --no-verify flag exists for experiments only).

Loop-head hints

Checking that a loop means the same on both sides cannot be done by following it around: the number of rounds is not known. sysi refine instead cuts each function at its loop heads and checks each piece between cuts on its own, from a state where all it knows about the variables is the loop's invariant. For that it must know, at each head, which sysi values correspond to which sysp variables. Finding that correspondence by search is the hard part of translation validation. The lowering knows it, because it made it, so it says so: the cut written at each loop head, and a fuller hint it hands to the check.

The cut in the module names the values that hold the loop's own variables, (vars (s v5) (i v6)), with the loop's place in the source and its invariants as written. The hint given to the check goes further: for every variable in scope at the head, where the lowering keeps it, either as a value (ssa) or at an address and offset in memory (mem) for variables that live in a slot. It also records, for each function, the sysp definition it came from and whether it is a kernel twin or runs in user mode. At a loop head, the check reads each sysp variable off sysi's state as the hint says, and at every jump back to the head it must show that the new sysi values are again the new sysp values. A wrong hint can only make that fail; it can never make a wrong lowering pass. The tour shows a failure reported at a loop head.

Kernel and user code: twins and gates

In sysk, tasks run in RISC-V user mode, and some functions are reached both from the kernel and from tasks. The lowering decides which code runs where as sysp's C backend does, from two options of sysi lower: --user-entry F names the function where user mode starts, and --gate G (repeatable) names a function user code reaches by a trap into the kernel.

• Every function F reaches, except through a gate, runs in user mode. In user code a call to a gate G becomes a call to the extern sysp_gate_G (the trap stub), and atomic becomes sysp_user_atomic_begin and _end, since user code cannot turn interrupts off.
• A function reached from both sides whose user form would differ (it has an atomic block or calls a gate, or calls such a function) is lowered twice: the user form under its own name, and a kernel twin named sysp_kernel_... with (source NAME twin), which the kernel's code calls instead.

Without these options, as in the tour, everything runs in kernel mode and no twins are made. Both checks treat a twin as one more function: sysi refine checks it against the same sysp function, in the mode it runs in.

The test program

tests/programs/features.sysp has one function for each form the lowering and the backends handle, each printing what it computes: structs of 3, 16 and 40 bytes passed by value, by reference and by mut, and returned; a struct holding a buffer, swapped with replace; more arguments than there are argument registers; every word width; a mut scalar; recursion and an early return from a loop; cells; and and and or with effects on the right. Its run calls them all.

• tests/rv64-test.rkt builds it through sysi's C and through sysi's RV64 assembly (with registers, and with every value on the stack), runs all three on sysr's simulator, and requires the same output.
• tests/refine-test.rkt requires every function of its lowering that sysi refine covers to pass it (all but run, which uses cell-swap, not checked yet), then makes mutants of the lowering, one changed instruction or terminator each (an operator swapped, a constant or offset off by one, a store dropped, call arguments or branch targets swapped), checks every third one (all of them with MUTATE=all), and requires each to be rejected, or else to run exactly as the original.