Complexity of Consistency Testing for the Release-Acquire Semantics
R. Govind, S. Krishna, Sanchari Sil, B. Srivathsan
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了最后一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
它引用的顶会 Paper8
- The Complexity of Dynamic Data Race PredictionUmang Mathur, Andreas Pavlogiannis, Mahesh ViswanathanLICS 2020 · 被引用 27 次
- C11Tester: a race detector for C/C++ atomicsWeiyu Luo, Brian DemskyASPLOS 2021 · 被引用 26 次
- Stateless Model Checking Under a Reads-Value-From EquivalencePratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis 等CAV 2021 · 被引用 25 次
- Verifying observational robustness against a c11-style memory modelRoy David Margalit, Ori LahavPOPL 2021 · 被引用 22 次
- Kater: Automating Weak Memory Model Metatheory and Consistency CheckingMichalis Kokologiannakis, Ori Lahav, Viktor VafeiadisPOPL 2023 · 被引用 15 次
相关 Paper
- How Hard Is Weak-Memory Testing?Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas PavlogiannisPOPL 2024 · 被引用 10 次
- Optimal Reads-From Consistency Checking for C11-Style Memory ModelsHünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna 等PLDI 2023 · 被引用 12 次
- Decidable verification under a causally consistent shared memoryOri Lahav, Udi BokerPLDI 2020 · 被引用 30 次
- Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsKartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh JagannathanOOPSLA 2024 · 被引用 1 次
- RGSep under Release/Acquire ConsistencyEllen Arlt, Viktor VafeiadisOOPSLA 2026 · 被引用 1 次
