Wed 19 Jan 2022 14:20 - 14:45 at Salon III - Weak Memory Models Chair(s): Mae Milano

Dynamic partial order reduction (DPOR) verifies concurrent programs by exploring all their interleavings up to some equivalence relation, such as Mazurkiewicz trace equivalence. Doing so involves a complex trade-off between space and time. Existing DPOR algorithms are either exploration-optimal (i.e., explore exactly only interleaving per equivalence class) but may use exponential memory in the size of the program, or maintain polynomial memory consumption but potentially explore exponentially many redundant interleavings.

In this paper, we show that it is possible to have the best of both worlds: exploring exactly one interleaving per equivalence class with linear memory consumption. Our algorithm, TruSt, is applicable not only to sequential consistency, but also to any weak memory model that satisfies a few basic assumptions, including TSO, PSO, and RC11. In addition, TruSt is embarrassingly parallelizable: its different exploration options have no shared state, and can therefore be explored completely in parallel. Consequently, TruSt outperforms the state-of-the-art in terms of memory and/or time.

Wed 19 Jan

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

13:30 - 14:45
Weak Memory ModelsPOPL at Salon III
Chair(s): Mae Milano University of California, Berkeley
13:30
25m
Research paper
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson
POPL
Alan Jeffrey Roblox, James Riely DePaul University, Mark Batty University of Kent, Simon Cooksey University of Kent, Ilya Kaysin JetBrains Research; University of Cambridge, Anton Podkopaev HSE University
DOI Media Attached
13:55
25m
Research paper
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal StoresRemote
POPL
Azalea Raad Imperial College London, Luc Maranget Inria, Viktor Vafeiadis MPI-SWS
DOI Media Attached
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI Media Attached