How Hard Is Weak-Memory Testing?

How Hard Is Weak-Memory Testing?

Chakraborty, S.S. (TU Delft Programming Languages)
Krishna, Shankara Narayanan (Indian Institute of Technology Bombay)
Mathur, Umang (National University of Singapore)
Pavlogiannis, Andreas (Aarhus University)

2024

Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is 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 parameterized algorithms for testing? The main contribution of this paper is a deep hardness result for consistency testing under many popular weak-memory models: the problem remains NP-complete even in its 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 popular variant of its Relaxed fragment, popular 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 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.

complexity
concurrency
consistency checking
weak memory models

http://resolver.tudelft.nl/uuid:293607b7-85ff-45d0-a3e3-31fe04c2c5ed

https://doi.org/10.1145/3632908

2475-1421

Proceedings of the ACM on Programming Languages, 8

Institutional Repository

journal article

© 2024 S.S. Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas Pavlogiannis