Wed 18 Jan 2023 10:45 - 11:10 at Grand Ballroom A - Automated Verification Chair(s): Michael Greenberg

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 model—topics 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 non-trivial 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 state-of-the-art model checker for concurrent programs. As a result, we get the first time- and space-efficient bounded verifier taking the axiomatic memory model as an input parameter.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:45 - 12:00
Automated VerificationPOPL at Grand Ballroom A
Chair(s): Michael Greenberg Stevens Institute of Technology
10:45
25m
Talk
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
POPL
Michalis Kokologiannakis MPI-SWS, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS
DOI
11:10
25m
Talk
Stratified Commutativity in Verification Algorithms for Concurrent ProgramsVirtual
POPL
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg
DOI
11:35
25m
Talk
A Partial Order View of Message-Passing Communication Models
POPL
Cinzia Di Giusto Université Côte d'Azur; CNRS, Davide Ferre' Université Côte d'Azur; CNRS, Laetitia Laversa Université Côte d'Azur; CNRS, Etienne Lozes Université Côte d'Azur; CNRS
DOI