FM2026Top-tier venue
Complexity of Consistency Testing for the Release-Acquire Semantics
R. Govind, S. Krishna, Sanchari Sil, B. Srivathsan
Abstract
Abstract In a seminal work, Gibbons and Korach [9] studied the complexity of deciding whether an observed sequence of reads and writes of a multi-threaded program admits a sequentially consistent interleaving. They showed the problem to be NP -hard even under strong syntactic restrictions. More recently, Chakraborty et al. [6] considered the problem for weak memory models and proved that NP -hardness remains even when the number of threads, the number of memory locations, and the value domain are all bounded. In this paper we revisit the problem for the release-acquire variants of the C11 memory model. Our main positive result is that consistency testing can be done in polynomial-time when each memory location is written by at most one thread (multiple readers are allowed). Notably, this restriction is already NP -hard for the model of sequential consistency. We complement our upper bound with tight hardness results: we show the problem to be NP -hard when two threads may write to the same location; furthermore, allowing three writers per location rules out 2 o ( k ) · n O ( 1 ) algorithms under the Exponential Time Hypothesis, where k denotes the number of threads, and n the number of memory operations.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext c9b39c3d-8c19-40f5-8be4-1cbe2b76bc8bBuilds on8
- The Complexity of Dynamic Data Race PredictionUmang Mathur, Andreas Pavlogiannis, Mahesh ViswanathanLICS 2020 · 27 citations
- C11Tester: a race detector for C/C++ atomicsWeiyu Luo, Brian DemskyASPLOS 2021 · 26 citations
- Stateless Model Checking Under a Reads-Value-From EquivalencePratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis et al.CAV 2021 · 25 citations
- Verifying observational robustness against a c11-style memory modelRoy David Margalit, Ori LahavPOPL 2021 · 22 citations
- Kater: Automating Weak Memory Model Metatheory and Consistency CheckingMichalis Kokologiannakis, Ori Lahav, Viktor VafeiadisPOPL 2023 · 15 citations
Related papers
- How Hard Is Weak-Memory Testing?Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas PavlogiannisPOPL 2024 · 10 citations
- Optimal Reads-From Consistency Checking for C11-Style Memory ModelsHünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna et al.PLDI 2023 · 12 citations
- Decidable verification under a causally consistent shared memoryOri Lahav, Udi BokerPLDI 2020 · 30 citations
- Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsKartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh JagannathanOOPSLA 2024 · 1 citation
- RGSep under Release/Acquire ConsistencyEllen Arlt, Viktor VafeiadisOOPSLA 2026 · 1 citation
