Correct-by-construction Nim programs

[mratsim]

This RFC outlines a potential roadmap to have tooling that significantly address a "new" class of bugs, logic bugs, i.e. bugs in the program design.

New as in the only general purpose language that addresses it as far as I know is Ada/Sparks. And others are formal verification language. I am aware of Eiffel and the design-by-contract paradigm, you will find assume, invariant, precondition, postcondition and assert as useful.

This is a followup to my comment on the safety modes RFC: #180 (comment)

Motivating examples

You are designing software for one of the following scenarios:

• A safety system that prevent opening doors while a vehicle is moving
• A scheduler for complex urban crossroads and you want to prove that the green lights cannot lead to vehicules crossing lanes of each other.
• A scheduler for train tunnels with only one lane in the tunnel and you don't want train collision
• A microwave and you want to ensure that under no circumstances radiations are emitted before the door is closed
• An alarm system for a building or as a medical device and you want to ensure that there is no false negative.
• An aircraft autopilot and you want to ensure that at any time a human can take back control to address unforeseen events
• A critical section algorithm but you don't have any locks available on your platform
• A multithreading runtime and you want to ensure that it is free of deadlock or livelock
• A threadsafe hash-table and you want to handle properly many threads.
• A distributed database or filesystem protocol and you want to prove that any sequence of prepare-commit-rollback leaves your database in a consistent state
• A P2P messaging protocol and you want to prove that starting from a certain connectivity threshold, messages are guaranteed to arrive (and maybe their order?)
• A blockchain protocol and you want to prove the percentage of malicious actors it can accomodate before the consensus algorithm breaks.

Overview

The usual software bug detection tools:

• avoiding nil pointers
• checking bounds accesses
• sanitizing memory accesses
• borrow checking
  only addresses low-level software bug.

They do not address bugs in software design that come from an unlikely sequence of events that trigger an unhandled or undefined scenario and potentially catastrophic failures.

Caveat emptor

This is not a replacement for runtime checks, testing, fuzzing. It ensures that your design (aka blueprint) is correct but your implementation might be buggy (for example you forgot to initialize a variable before use).

Correct-by-construction mission-critical system

In Nim, this would involve a branch of formal verification called model checking.
This works by exhaustively checking all the possible state of your program (say no train in tunnel, train approaching, trains approaching, train out of the tunnel, rain, train stuck in tunnel, red light failure, ...) and asserting that the unwanted scenarios cannot happen according to the state transitions of your system and your explicit assumptions (the red light cannot fail).

This requires at minimum:

• A Domain-Specific Language to express state, the (potentially conditional) transitions to other states, the events that trigger those transitions
• A way to express constraints: asserts at least, preCondition, PostCondition, Invariants
• A model checker (prover) that can explore all those states and prove that whatever the sequence of events those constraints are respected

Paper

• Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
  Jessica Petrasch, Jan-Hendrik Oepen, Sebastian Krings, Moritz Gericke, 2018
  https://journal.ub.tu-berlin.de/eceasst/article/view/1074
  https://github.com/bmoth-mc/bmoth

This paper, which comes with an implementation, uses:

• the B formal language to express state machine, events, transition to new state, conditions and invariants (we don't need all those maths don't worry)
• ANTLR to generate a parser the language grammar
• Z3 with Temporal Logic backend for proving
• Some glue to transform the state machine into Z3 inputs.

This was created by students in a trimester so should be quite accessible.

Note that they mentioned that Z3 wasn't ideal due to not mapping perfectly to the B language. In our case, I think it's an excellent first step as:

• We don't use the B language, we can start with a restricted subset of use cases that map well with Z3.
• We don't have to implement a prover
• State to handle grows exponentially

In Nim

• The Z3 backend and accompanying assertions/preCondition/postCondition checks are WIP in DrNim
• I wrote a state machine generator that works at compile time, Synthesis, the code generated is suitable for embedded devices: no allocation at all, just if and goto and it's fast.
  • No math, a state machine is declarative

    behavior(awaitFSA):
      ini: AW_CheckTask
      event: AWE_HasChildTask
      transition:
        profile(run_task):
          execute(task)
        profile(enq_deq_task):
          localCtx.taskCache.add(task)
      fin: AW_CheckTask

  • The state machine is code first and not diagram first.
  • It can generate graphs as well (see the implementation of await that participare in work-stealing while waiting)
  • It's a very small library (<1000 lines)
• TODO: Translating transitions into Z3 AST (covered in paragraph 4 of the paper via AST rewrite)

Correct-by-construction thread synchronization

This is something I critically need in Weave / Project Picasso (#160).
I did use model checking via TLA+ to debug and remove deadlocks in my backoff algorithm (that put idle threads to sleep) and ultimately uncover a wakeup bug in Glibc condition variables (mratsim/weave#56).
However, that requires learning a new language (which is worth it if implementing a lot of distributed protocols) and does not address implementation bugs due to misunderstanding the C11/C++11 memory model for atomics synchronization.

Examples

Verifying the implementation of a concurrent channel.

In Nim

The goal is to verify that the implemented Nim code does not lead to an inconsistent state by unanticipated interleaving of thread execution.
The way to do that is by overloading createThread, and synchronization primitives like Atomic, Lock and CondVar.

To model check a concurrent data structure instead of creating a thread, createThread will create two states, and then you create a graph of all possible threads (and resulting states) interleaving. When encountering a synchronization primtives, the model checker might have 1 state make progress (or not) if the memory model allows it (locked or not, acquire/release, ...).

This create a (potentially huge graph) of thread interleaving and what happens at each synchronization and exhaustively explore all possible state proving whether or not there is a synchronization bug (via asserts in the code).

References:

• CDSChecker
  • http://plrg.ics.uci.edu/software_page/42-2/
  • git clone git://demsky.eecs.uci.edu/model-checker.git
  • http://plrg.eecs.uci.edu/publications/c11modelcheck.pdf
• Relacy Race Detector:
  • http://www.1024cores.net/home/relacy-race-detector
  • Code: https://github.com/dvyukov/relacy
  • Note: Dmitry Vyukov is behind LLVM ThreadSanitizer, the Go and Tensorflow async and multithreaded scheduler and the Go thread sanitizer.

And a lot more at mratsim/weave#18 but most only model sequentially consistent execution (i.e. synchronization via locks and condition variables) but not C11/C++11 relaxed memory model and synchroniation via acquire/release atomics).

Note: it's probably possible to use Z3 here as well.

[Araq]

This RFC is not very action-able so far.

What features does DrNim need in order to support multi-threading?

[mratsim]

This RFC covers 2 parts:

• 1. Model checking state machines to ensure that they properly handle events and don't deadlock and respect some specified invariant
• 2. Model checking concurrent data structure including Lock, Condition Variables and Atomics usage to ensure that there is no deadlock, livelock, data races and respect some specified invariants.

Part 2: multithreading

2. is better tackled independently, which I started here: [WIP] Thread Collider: Race detection / Formal Verification of Nim concurrent programs mratsim/weave#127

Part 1: State machines

DrNim can be expanded to support 1. As mentioned, this would be very helpful for embedded devices, protocol design, mission-critical systems to prove the absence of flaws in the design.

For that DrNim would need to implement some AST -> Z3 translation similar to https://github.com/bmoth-mc/bmoth/tree/develop/src/main/java/de/bmoth/backend/z3 and described in the paper https://journal.ub.tu-berlin.de/eceasst/article/view/1074, Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation from Petrash et al

The AST ideally is similar to Synthesis DSL and you can feed it:

• initial state (StateEnum)
• event/trigger (EventEnum)
• final state (StateEnum)
• precondition, postcondition, invariant
• transition: this would set/unset some symbols that we are interested in verifying or call another nested state-machine.

This way you can ask Z3 if your state machine doesn't have a corner case with an event that is not handled.

The level beyond is then composing state machines to implement a protocol.

Then we need to find (non-trivial but not too complex) examples to showcase.

1. We can pick a 2-phase commit protocol to update a database while leaving it consistent
2. We can pick my event notifier protocol that augments a message channel to put a thread to sleep/wakeup without deadlock (i.e. you send a wakeup, then the thread wakes up and goes to sleep again because message didn't arrive yet and then you send a message and it's never received): https://github.com/mratsim/weave/blob/46cf3232d6b05e225dce81f4d92facf85cfd6293/weave/cross_thread_com/event_notifiers.nim
3. We can pick a messaging protocol for example from nanomsg:
   
4. We can pick an authentication protocol that requires handshakes and acknowledgements and prove that your transitions are bug free. For example TCP
   
   or SOCKS5
   
5. For mission-critical systems, pick an elevator example and prove that while going up from 0 to 10 and someone at floor 5 presses 3, it doesn't go down but continue to floor 10
6. I'm sure ADA/Sparks has relevant examples we can borrow from.