2024-11-09 22:45:00
plv.mpi-sws.org
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
-
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, 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, 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, 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, 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, Viktor Vafeiadis.
In PLDI 2024 (June 2024)
[Paper (23 pages)]
[Artifact @Zenodo]
People
Related projects
Support Techcratic
If you find value in Techcratic’s insights and articles, consider supporting us with Bitcoin. Your support helps me, as a solo operator, continue delivering high-quality content while managing all the technical aspects, from server maintenance to blog writing, future updates, and improvements. Support Innovation! Thank you.
Bitcoin Address:
bc1qlszw7elx2qahjwvaryh0tkgg8y68enw30gpvge
Please verify this address before sending funds.
Bitcoin QR Code
Simply scan the QR code below to support Techcratic.
Please read the Privacy and Security Disclaimer on how Techcratic handles your support.
Disclaimer: As an Amazon Associate, Techcratic may earn from qualifying purchases.