Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper resolves a long-standing open problem by proving that reachability in the RMW-free fragment of the Release/Acquire memory model is undecidable. The result demonstrates that even without atomic Read-Modify-Write operations, verifying concurrent programs under Release/Acquire remains undecidable, establishing the simplest set of communication primitives leading to undecidability. Furthermore, the authors show that bounding both context switches and RMW operations leads to decidability, delineating the boundary between decidable and undecidable verification problems.
Even without complex atomic operations, verifying concurrent programs under the Release/Acquire memory model is fundamentally undecidable.
The verification of concurrent programs under weak-memory models is a burgeoning effort, owing to the increasing adoption of weak memory in concurrent software and hardware. Release/Acquire has become the standard model for high-performance concurrent programming, adopted by common mainstream languages and computer architectures. In a surprising result, Abdulla et al. (PLDI'19) proved that reachability in this model is undecidable when programs have access to atomic Read-Modify-Write (RMW) operations. Moreover, undecidability holds even for executions with just 4 contexts, and is thus immune to underapproximations based on bounded context switching. The canonical, RMW-free case was left as a challenging question, proving a non-primitive recursive lower bound as a first step, and has remained open for the past seven years. In this paper, we settle the above open question by proving that reachability is undecidable even in the RMW-free fragment of Release/Acquire, thereby characterizing the simplest set of communication primitives that gives rise to undecidability. Moreover, we prove that bounding both the number of context switches and the number of RMWs recovers decidability, thus fully characterizing the boundary of decidability along the dimensions of RMW-bounding and context-bounding.