SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 08:10 - 08:25 at Zurich D - Shared Memory - mirror Chair(s): Sebastian Burckhardt
Wed 20 Oct 2021 16:10 - 16:25 at Zurich D - Shared Memory Chair(s): Doug Lea

The verification of concurrent programs remains an open challenge due to the non-determinism in inter-process communication. One recurring algorithmic problem in this challenge is the consistency verification of concurrent executions. In particular, consistency verification under a reads-from map allows to compute the \emph{reads-from (RF) equivalence} between concurrent traces, with direct applications to areas such as Stateless Model Checking (SMC). Importantly, the RF equivalence was recently shown to be coarser than the standard Mazurkiewicz equivalence, leading to impressive scalability improvements for SMC under SC (sequential consistency). However, for the \emph{relaxed memory} models of TSO and PSO (total/partial store order), the algorithmic problem of deciding the RF equivalence, as well as its impact on SMC, has been elusive.

In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted \operatorname{VTSO-rf} and \operatorname{VPSO-rf}, respectively. For an execution of $n$ events over $k$ threads and $d$ variables, we establish novel bounds that scale as $n^{k+1}$ for TSO and as $n^{k+1}\cdot \min(n^{k^2}, 2^{k\cdot d})$ for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is \emph{exploration-optimal}, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when $k$ is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for \operatorname{VTSO-rf} and \operatorname{VPSO-rf} provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.

Wed 20 Oct

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

07:40 - 09:00
Shared Memory - mirrorOOPSLA at Zurich D
Chair(s): Sebastian Burckhardt Microsoft Research
07:40
15m
Talk
The Semantics of Shared Memory in Intel CPU/FPGA SystemsVirtual
OOPSLA
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
DOI
07:55
15m
Talk
SecRSL: Security Separation Logic for C11 Release-Acquire ConcurrencyVirtual
OOPSLA
Pengbo Yan University of Melbourne, Toby Murray University of Melbourne
DOI
08:10
15m
Talk
The Reads-From Equivalence for the TSO and PSO Memory ModelsVirtual
OOPSLA
Truc Lam Bui Comenius University Bratislava, Krishnendu Chatterjee IST Austria, Tushar Gautam IIT Bombay, Andreas Pavlogiannis Aarhus University, Viktor Toman IST Austria
DOI
08:25
15m
Talk
Making Weak Memory Models FairDistinguished PaperVirtual
OOPSLA
Ori Lahav Tel Aviv University, Egor Namakonov St. Petersburg University; JetBrains Research, Jonas Oberhauser Huawei, Anton Podkopaev HSE University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI
08:40
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

15:40 - 17:00
Shared MemoryOOPSLA at Zurich D -8h
Chair(s): Doug Lea State University of New York (SUNY) Oswego
15:40
15m
Talk
The Semantics of Shared Memory in Intel CPU/FPGA SystemsVirtual
OOPSLA
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
DOI
15:55
15m
Talk
SecRSL: Security Separation Logic for C11 Release-Acquire ConcurrencyVirtual
OOPSLA
Pengbo Yan University of Melbourne, Toby Murray University of Melbourne
DOI
16:10
15m
Talk
The Reads-From Equivalence for the TSO and PSO Memory ModelsVirtual
OOPSLA
Truc Lam Bui Comenius University Bratislava, Krishnendu Chatterjee IST Austria, Tushar Gautam IIT Bombay, Andreas Pavlogiannis Aarhus University, Viktor Toman IST Austria
DOI
16:25
15m
Talk
Making Weak Memory Models FairDistinguished PaperVirtual
OOPSLA
Ori Lahav Tel Aviv University, Egor Namakonov St. Petersburg University; JetBrains Research, Jonas Oberhauser Huawei, Anton Podkopaev HSE University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA