GenMC: A model checker for weak memory models

Summary

GenMC is an open-source state-of-the-art model checker for verifying concurrent C/C++ programs under the RC11, IMM, and LKMM memory models.

GenMC is based on a stateless model checking algorithm that is parametric in the choice of memory model. Subject to a few basic conditions about the memory model, our algorithm is sound, complete and optimal, in that it explores each consistent execution of the program according to the model exactly once, and does not explore inconsistent executions or embark on futile exploration paths.

It incorporates many optimizations, such as lock-aware and barrier-aware partial order reduction, symmetry reduction, and automatic spinloop bounding.

Source distribution

Tool paper

Papers

People

Related projects

Imprint | Data protection