Truly Stateless, Optimal Dynamic Partial Order Reduction
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 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:45
|The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson|
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 UniversityDOI Media Attached
|Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal StoresRemote|
POPLDOI Media Attached
|Truly Stateless, Optimal Dynamic Partial Order ReductionRemote|
Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWSDOI Media Attached