On the Decidability of Verification under Release/Acquire

TL;DR

This paper proves that reachability in Release/Acquire concurrent programs is undecidable even without RMW operations, but becomes decidable when bounding context switches and RMWs, clarifying the limits of automated verification.

Contribution

It resolves the open question by showing undecidability in the RMW-free case and identifies conditions under which verification becomes decidable.

Findings

Undecidability holds even without RMW operations.

Bounding context switches and RMWs makes verification decidable.

Characterizes the precise boundary of decidability for Release/Acquire models.

Abstract

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.