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

• GenMC on Github

Formal proofs

• TruSt formalization in Coq

Tool papers

• GenMC: A model checker for weak memory models.
  Michalis Kokologiannakis and Viktor Vafeiadis.
  In CAV 2021 (July 2021)
  [Paper (13 pages)]
  [Artifact @Zenodo]
• Enhancing GenMC's Usability and Performance.
  Michalis Kokologiannakis, Rupak Majumdar and Viktor Vafeiadis.
  In TACAS 2024 (April 2024)
  [Paper (16 pages)]
  [Artifact @Zenodo]

Papers

• Model checking for weakly consistent libraries.
  Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis.
  In PLDI 2019 (June 2019)
  [Paper (15 pages)] [@ACM] [Full paper with the technical appendix (31 pages)]
  [Artifact @ACM]
• Effective lock handling in stateless model checking.
  Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, OOPSLA, Article 173 (October 2019)
  [Paper (26 pages)] [@ACM] [Full paper with the technical appendix (40 pages)]
  [Artifact @Zenodo]
• HMC: Model checking for hardware memory models.
  Michalis Kokologiannakis and Viktor Vafeiadis.
  In ASPLOS 2020 (March 2020)
  [Paper (15 pages)] [@ACM]
  [Artifact @Zenodo]
• BAM: Efficient model checking for barriers.
  Michalis Kokologiannakis and Viktor Vafeiadis.
  In NETYS 2021 (May 2021)
  [Paper (17 pages)]
• Dynamic partial order reductions for spinloops.
  Michalis Kokologiannakis, Xiaowei Ren, and Viktor Vafeiadis.
  In FMCAD 2021 (October 2021)
  [Paper (10 pages)]
• Truly stateless, optimal dynamic partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, POPL (January 2022)
  [Paper (28 pages)]
  [Full paper with the technical appendix (58 pages)]
  [Artifact @Zenodo]
• Model Checking on Multi-execution Memory Models.
  Evgenii Moiseenko, Michalis Kokologiannakis, and Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, OOPSLA2 (October 2022)
  [Paper (28 pages)]
  [Full paper with the technical appendix (70 pages)]
  [Artifact @Zenodo]
• Reconciling Preemption Bounding with DPOR.
  Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis.
  In TACAS 2023 (April 2023)
  [Paper (19 pages)]
  [Full paper with the technical appendix (21 pages)]
  [Artifact @Zenodo]
• Unblocking Dynamic Partial Order Reduction.
  Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis.
  In CAV 2023 (July 2023)
  [Paper (19 pages)]
  [Technical appendix]
  [Artifact @Zenodo]
• SPORE: Combining Symmetry and Partial Order Reduction.
  Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis.
  In PLDI 2024 (June 2024)
  [Paper (23 pages)]
  [Full paper with the technical appendix]
  [Artifact @Zenodo]
• RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency.
  Pavel Golovin, Michalis Kokologiannakis, and Viktor Vafeiadis.
  In POPL 2025 (January 2025)
  [Paper (23 pages)]
  [Artifact @Zenodo]
• Model Checking C/C++ with Mixed-Size Accesses.
  Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis.
  In POPL 2025 (January 2025)
  [Paper (23 pages)]
  [Artifact @Zenodo]

People

• Michalis Kokologiannakis (MPI-SWS)
• Iason Marmanis (MPI-SWS)
• Azalea Raad (MPI-SWS)
• Viktor Vafeiadis (MPI-SWS)

Related projects

• RCMC: a model checker for RC11
• Repairing sequential consistency in C/C++11: defines the RC11 model.
• PerSeVerE: GenMC for model checking under Linux ext4.