Stateless Model Checking Concurrent and Distributed Programs
Materials
Summary
Stateless model checking (SMC) is a fully automated (“push-button”) technique for verifying con- current and distributed programs that is easy to use and hard to master. One writes a self-contained program — typically a test client of a concurrent library containing some assertions — and invokes the model checker. The model checker then explores all the possible executions of the program (i.e., all thread interleavings, all weak memory consistency effects) in a very clever fashion, and either reports that the program is correct or returns a concrete program execution leading to an error.
This tutorial will cover both the theory and the practice of stateless model checking using GenMC, a state-of-the-art model checker for C/C++ programs. More specifically, we will cover the following topics:
- How does SMC work?
- How can we apply SMC to our code?
- How can we estimate how much time verification will take?
- What options do we have when the time estimate is too large?
- How can we make verification more efficient?
- What else (besides correctness) can we get from a model checker?