POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is \emph{consistency testing}:~is the observed execution of a concurrent program in alignment with the specification of the underlying system? The problem has been studied extensively across Sequential Consistency (SC) and weak memory, and proven to be NP-complete when some aspect of the input (e.g., number of threads/memory locations) is unbounded. This unboundedness has left a natural question open: are there efficient \emph{parameterized} algorithms for testing?

The main contribution of this paper is a deep hardness result for consistency testing under many popular weak-memory models, that is significantly stronger than all known results:~the problem remains NP-complete even in its \emph{bounded} setting, where candidate executions contain a bounded number of threads, memory locations, and values. This hardness spreads across several Release-Acquire variants of C11, a common variant of its Relaxed fragment, common Causal Consistency models, and the POWER architecture. To our knowledge, this is the first result that fully exposes the hardness of weak-memory testing and proves that the problem \emph{admits no parameterization} under standard input parameters. It also yields a computational separation of these models from SC, x86-TSO, PSO, and Relaxed, for which bounded consistency testing is either known (for SC), or shown here (for the rest), to be in polynomial time.

Thu 18 Jan

Displayed time zone: London change

13:40 - 15:00
Weak Memory and Concurrent Separation LogicPOPL at Turing Lecture
Chair(s): William Mansky University of Illinois Chicago
13:40
20m
Talk
How Hard is Weak-Memory Testing?
POPL
Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
Pre-print
14:00
20m
Talk
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL
Angus Hammond University of Cambridge, Zongyuan Liu Aarhus University, Thibaut Pérami University of Cambridge, Peter Sewell University of Cambridge, Lars Birkedal Aarhus University, Jean Pichon-Pharabod Aarhus University
Pre-print
14:20
20m
Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL
Amin Timany Aarhus University, Simon Oddershede Gregersen Aarhus University, Leo Stefanesco MPI-SWS, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Léon Gondelman Aarhus University, Abel Nieto Aarhus University, Lars Birkedal Aarhus University
14:40
20m
Talk
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University Nijmegen
Pre-print