GenMC: A Generic Model Checker for Concurrent Programs

GenMC is a stateless model checker for concurrent programs written under the SC [Lamport 1979], TSO [Owens et al. 2009], RA [Lahav et al. 2016], RC11 [Lahav et al. 2017], and IMM [Podkopaev et al. 2019] memory models. It primarily targets C/C++ and Rust programs, verifying safety properties by analyzing their concurrency patterns (e.g., usage of C11 atomics or Rust's std::sync). It employs an effective dynamic partial order reduction technique [Kokologiannakis et al. 2019, Kokologiannakis et al. 2022] that is sound, complete, and optimal.

GenMC operates at the level of LLVM Intermediate Representation (LLVM-IR). It uses clang to translate C/C++ programs and rustc to translate Rust programs into LLVM-IR. This intermediate approach allows GenMC to be language-agnostic regarding its core verification logic, though it relies on language-specific frontends for translation.

GenMC should compile on Linux and MacOS provided that the relevant dependencies are installed (see README.md).

Table of Contents

• Basic Usage
• Tool Features
• Command-line Options
• Supported APIs
• References

Contact

For feedback, questions, and bug reports please send an e-mail to michalis.kokologiannakis@inf.ethz.ch.