Complexity of Consistency Testing for the Release-Acquire Semantics
This addresses the problem of verifying program correctness under weak memory models for software developers and verification tools, providing new algorithmic insights but is incremental relative to prior work on memory consistency.
The paper tackles the complexity of consistency testing for the release-acquire semantics in C11 memory models, showing it is polynomial-time solvable when each memory location is written by at most one thread, but NP-hard with two writers and excludes efficient algorithms under the Exponential Time Hypothesis with three writers.
In a seminal work, Gibbons and Korach 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. 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 sequential consistency. We complement this upper bound with tight hardness results: the problem is NP-hard when two threads may write to the same location, and 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.