Wed 21 Jun 2023 09:40 - 10:00 at Cypress 1 - PLDI: Memory Models & Program Logics Chair(s): Matthew J. Parkinson

Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++. One of the most fundamental problems associated with a memory model M is consistency checking:~given an execution X, is X consistent with M? This problem lies at the heart of numerous applications, including specification testing and litmus tests, stateless model checking, and dynamic analyses. As such, it has been explored extensively and its complexity is well-understood for traditional models like SC and TSO. However, less is known for the numerous model variants of C/C++, for which the problem becomes challenging due to the intricacies of their concurrency primitives. In this work we study the problem of consistency checking for popular variants of the C11 memory model, in particular, the $\mathtt{RC20}$ model, its release-acquire (RA) fragment, the strong and weak variants of RA (SRA and WRA), as well as the Relaxed fragment of RC20.

Motivated by applications in testing and model checking, we focus on reads-from consistency checking. The input is an execution X specifying a set of events, their program order and their reads-from relation, and the task is to decide the existence of a modification order on the writes of X that makes X consistent in a memory model. We draw a rich complexity landscape for this problem; our results include (i) nearly-linear-time algorithms for certain variants, which improve over prior results, (ii) fine-grained optimality results, as well as (iii) matching upper and lower bounds (NP-hardness) for other variants. To our knowledge, this is the first work to characterize the complexity of consistency checking for C11 memory models. We have implemented our algorithms inside the TruSt model checker and the C11Tester testing tool. Experiments on standard benchmarks show that our new algorithms improve consistency checking, often by a significant margin.

Wed 21 Jun

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

09:00 - 11:00
PLDI: Memory Models & Program LogicsPLDI Research Papers at Cypress 1
Chair(s): Matthew J. Parkinson Azure Research, Microsoft, UK

#pldi-wed-0900-memory-cypress Discord icon small YouTube icon small

09:00
20m
Talk
Compound Memory Models
PLDI Research Papers
Andrés Goens the University of Edinburgh, Soham Chakraborty TU Delft, Susmit Sarkar University of St. Andrews, Sukarn Agarwal University of Edinburgh, Nicolai Oswald NVIDIA, Vijay Nagarajan University of Edinburgh, UK
DOI
09:20
20m
Talk
Putting Weak Memory in Order via a Promising Intermediate Representation
PLDI Research Papers
Sung-Hwan Lee Seoul National University, Minki Cho Seoul National University, Roy Margalit Tel Aviv University, Israel, Chung-Kil Hur Seoul National University, Ori Lahav Tel Aviv University
DOI
09:40
20m
Talk
Optimal Reads-From Consistency Checking for C11-Style Memory Models
PLDI Research Papers
Hünkar Can Tunç Aarhus University, Parosh Aziz Abdulla Uppsala University, Sweden, Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
DOI Pre-print
10:00
20m
Talk
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
PLDI Research Papers
Zongyuan Liu Aarhus University, Sergei Stepanenko Aarhus University, Jean Pichon-Pharabod Aarhus University, Amin Timany Aarhus University, Aslan Askarov Aarhus University, Lars Birkedal Aarhus University
DOI
10:20
20m
Talk
Embedding Hindsight Reasoning in Separation Logic
PLDI Research Papers
Roland Meyer TU Braunschweig, Thomas Wies New York University, Sebastian Wolff New York University
DOI
10:40
20m
Talk
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
PLDI Research Papers
Ike Mulder Radboud University Nijmegen, Lukasz Czajka Heliax AG, Robbert Krebbers Radboud University Nijmegen
DOI Pre-print