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.

翻译：在弱内存模型下对并发程序的验证正日益受到关注，原因是并发软件和硬件中弱内存的广泛采用。Release/Acquire已成为高性能并发编程的标准模型，被主流编程语言和计算机体系结构广泛采用。令人惊讶的是，Abdulla等人（PLDI'19）证明，当程序可访问原子读-修改-写（RMW）操作时，该模型下的可达性是不可判定的。此外，即使在仅包含4个上下文的执行中，这种不可判定性依然成立，因此基于有界上下文切换的欠近似方法对其无效。无RMW的经典情况被留作一个具有挑战性的问题——先通过证明非原始递归下界作为初步步骤，并在过去七年中一直悬而未决。本文通过证明即使在Release/Acquire的无RMW片段中，可达性也是不可判定的，从而解决了上述开放问题，由此刻画了导致不可判定性的最简通信原语集合。此外，我们证明同时对上下文切换次数和RMW操作次数进行有界约束可恢复可判定性，从而完整刻画了沿RMW有界性和上下文有界性两个维度的可判定性边界。