Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Summary
The metatheory of axiomatic weak memory models covers questions like the correctness of compilation mappings from one model to another and the correctness of local program transformations according to a given modeltopics usually requiring lengthy human investigation. We show that these questions can be solved by answering a more basic question: ``Given two memory models, is one weaker than the other?'' Moreover, for a wide class of axiomatic memory models, we show that this basic question can be reduced to a language inclusion problem between regular languages, which is decidable.
Similarly, implementing an efficient check for whether an execution graph is consistent according to a given memory model has required nontrivial manual effort. Again, we show that such efficient checks can be derived automatically for a wide class of axiomatic memory models, and that incremental consistency checks can be incorporated in GenMC, a stateoftheart model checker for concurrent programs. As a result, we get the first time and spaceefficient bounded verifier taking the axiomatic memory model as an input parameter.
Paper

Kater: Automating Weak Memory Model Metatheory and Consistency Checking.
Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis.
Proc. ACM Program. Lang. 7, POPL, Article 19 (January 2023)
[Preprint (27 pages)] [@ACM] [Artifact @Zenodo]
People
 Michalis Kokologiannakis (MPISWS)
 Ori Lahav (Tel Aviv University)
 Viktor Vafeiadis (MPISWS)
Related projects
 GenMC: A generic model checker for C/C++