How sysk is proven

sysp in one paragraph

sysp is the language sysk is written in. It looks like Lisp and compiles to C. Every function states a contract: requires (what must hold when it is called), ensures (what holds when it returns) and effects (whether it may allocate or do IO). Buffers are linear: each has exactly one owner, and using one after giving it away is an error. sysp check turns every place the program could go wrong into an obligation, a logical formula, and asks the Z3 solver to prove it from what is known at that point. On the whole system that is obligations, proven in about seconds, with loop invariants sysp found by itself. sysp also keeps proofs: a function whose text, and whose callees' contracts, have not changed is not proven again, so after a small edit a check takes about a second.

An obligation, up close

Pick an example. The goal is what must hold at that point in the code; each part of it is proven from facts sysp knows there. Select a part to see where its facts come from.

When a proof fails

Here is a task that was handed a channel end for 5 lines and sends 6. It is one of the negative tests (tests/negative/send-too-many.sysp): sysp must reject it.

; A task handed a channel end for 5 lines sends a sixth.
(fn chatty ((k (shared Kernel kernel-rely)) (out Tx) (line (ref (buf u8)))) unit
  (effects io)
  (requires
    (and (running k)
      (tx-for k out)
      (tx-left out 5)
      (tx-bytes out line-bytes)
      (== (len line) line-bytes)))
  (var i 0)
  (while (< i 6)
    (send k out line)
    (set i (+ i 1)))
  (close-tx out))

tests/negative/send-too-many.sysp:14:5: error[V001]: precondition `(and (running k) (tx-for k out) (> (. out left) 0) (== (len msg) (. out bytes)))` of `send` may not hold for this call
    obligation: (and (running k) (tx-for k out) (> (. out left) 0) (== (len msg) (. out bytes)))
    counterexample: i = 5, out.left = 5, out.bytes = 64, len(line) = 64, ...
    fix: inside a loop the verifier knows only the invariants about variables the loop changes: add an invariant that implies this obligation, or rewrite the expression so the invariants suffice

sysp names the call and the contract it could not prove. The counterexample is a state it could not rule out. Here the useful invariant, "lines left = 5 − i", is not one it can keep: by the sixth round it would have to be −1. Without it, sysp knows nothing about the count inside the loop, so it cannot show one is left. The fix is in the code, never in the checker. Every rule sysk depends on has a test like this one; the table at the end of the page lists them.

Running while others run: rely and guarantee

Tasks are preempted at any instruction, and all of them share the kernel's state. A task cannot know what happened while it was paused. sysp's answer is a rely: the kernel is a shared parameter, (k (shared Kernel kernel-rely)), and between its atomic blocks a task may assume only what kernel-rely says: the kernel's invariant still holds and the task is still the current one. In return, every atomic block anywhere is proven to keep that promise (its guarantee), and so is the timer handler. Step through a stretch of the producer's run:

What is not proven

Proofs rest on things sysp takes on trust. In sysk those are kept few and named:

• Extern contracts. A function written in assembly is declared extern with a contract sysp assumes. There are of them; each is listed on The trusted base.
• The assembly itself, lines, and the C compiler that turns sysp's output into machine code. User mode with PMP catches what these get wrong in code that runs in a task; for the kernel, which runs in machine mode, nothing does.
• How tasks interleave. sysp proves each function alone. Whether two tasks can wait for each other forever is checked by a different tool, which reads each task's waits (Deadlock freedom).

The rules, and the tests that hold sysp to them