arxiv: 2604.13683 · v1 · submitted 2026-04-15 · 💻 cs.PL · cs.CC

Recognition: unknown

On the Decidability of Verification under Release/Acquire

Andreas Pavlogiannis, Giovanna Kobus Conrado

Authors on Pith no claims yet

Pith reviewed 2026-05-10 12:23 UTC · model grok-4.3

classification 💻 cs.PL cs.CC

keywords Release/Acquireweak memory modelsdecidabilityreachabilityconcurrent program verificationundecidabilityRMW-free fragment

0 comments

The pith

Reachability is undecidable under Release/Acquire even without read-modify-write operations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that determining whether a concurrent program can reach a bad state remains undecidable under the Release/Acquire memory model even when atomic read-modify-write instructions are unavailable. This settles an open question that persisted after an earlier result established undecidability only in the presence of RMWs. The proof also shows that decidability is recovered precisely when both the number of context switches and the number of RMWs are bounded. The outcome identifies release and acquire as the minimal set of primitives sufficient to produce undecidability for reachability.

Core claim

We prove 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.

What carries the argument

A reduction from a known undecidable problem to reachability queries that preserves the RMW-free semantics of Release/Acquire and models finite executions under the memory model.

If this is right

Reachability remains undecidable for RMW-free programs even when the number of context switches is bounded.
Decidability holds exactly when both context switches and RMW operations are bounded simultaneously.
Release and acquire without RMWs form the minimal communication primitives that produce undecidability for verification.
Underapproximations limited to bounded context switching alone cannot decide reachability in the RMW-free model.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Verification procedures for Release/Acquire programs must therefore restrict at least one of the two dimensions to guarantee termination.
The same boundary may mark decidability thresholds in other weak-memory models that expose comparable release and acquire primitives.
Practical tools could combine bounded-context exploration with RMW counting to obtain sound and complete analyses for realistic programs.

Load-bearing premise

The reduction from a known undecidable problem preserves the RMW-free semantics of Release/Acquire and correctly models finite executions under the memory model.

What would settle it

An algorithm that correctly decides reachability for every finite RMW-free Release/Acquire program, or a specific program encoding an undecidable instance whose reachability status under the model contradicts the reduction.

Figures

Figures reproduced from arXiv: 2604.13683 by Andreas Pavlogiannis, Giovanna Kobus Conrado.

**Figure 2.** Figure 2: The high level behavior of 𝑡 𝑥 𝛼 , 𝑡 𝑦 𝛼 , 𝑡 𝑥 𝛽 , 𝑡 𝑦 𝛽 , 𝑡𝑥 , and 𝑡𝑦 on a PCP instance with the tuples ⟨𝑏𝑎, 𝑎𝑎⟩ and ⟨𝑎𝑏𝑎, 𝑎⟩ as input. The solution illustrated is the sequence 2, 1, which generates the string 𝑎𝑎𝑏𝑎. Words guessed by 𝑡 𝑥 𝛼 and 𝑡 𝑦 𝛼 are shown on the left; those guessed by 𝑡 𝑥 𝛽 and 𝑡 𝑦 𝛽 , on the right. The highlighted pairs in 𝑡𝑥 and 𝑡𝑦 mark operations that must read the same value. 𝑗 ′ 1… view at source ↗

**Figure 3.** Figure 3: The communication topology between the threads of [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

**Figure 4.** Figure 4: An illustration of the synchronization between threads in [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗

**Figure 5.** Figure 5: An illustration of the interaction between threads in [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗

**Figure 6.** Figure 6: The program P corresponding to a PCP instance I. iterations. The purpose of using 𝑡 𝑦 𝛼 instead of 𝑡 𝑦 𝛼 is to distinguish the first write, and not allow the first read on 𝑦𝛼 on 𝑡𝑦 to skip reading from it. These writes on 𝑦𝛼 are also interleaved with other writes and reads on 𝑧 ′ 𝛼 𝑦 and 𝑧 𝑦 𝛼 , which create a pattern of interaction with 𝑡 ′ 𝛼 𝑦 following [PITH_FULL_IMAGE:figures/full_fig_p012_6.png] view at source ↗

**Figure 7.** Figure 7: A graph𝐺 with Sum(𝑒𝑖) = Sum(𝑒𝑗) and the corresponding𝐺 ′ (a). (b) illustrates the recovery of missing rf edges, and (c) illustrates how mo is adapted to restore read-coherence for the recovered rf. on each location reaches the same set of events in other threads via hb. We call T reducible if it contains a collapsible pair of events, and irreducible otherwise. The following lemma gives a bound on the size … view at source ↗

**Figure 8.** Figure 8: The graph 𝐺 ∈ ⟦P⟧ can be reduced to 𝐺 ′ while still reaching the final state of P. This is done without increasing the number of contexts of 𝐺, by simply removing events in 𝐺 and changing 𝐺.mo and 𝐺.rf. SumT (𝑒𝑖).Erf, we set 𝐺 ′ .mo𝑥 = 𝐺.mo𝑥 ∩ (𝐺 ′ .𝐸 × 𝐺 ′ .𝐸). Otherwise, let w𝑖 = LwT (𝑒𝑖 , 𝑥) and w𝑗 = LwT (𝑒𝑗 , 𝑥). We set 𝐺 ′ .mo𝑥 = mo𝑥 ∩ (𝐺 ′ .𝐸 × 𝐺 ′ .𝐸), where mo𝑥 is identical to 𝐺.mo𝑥 , with w𝑖 and w… view at source ↗

**Figure 9.** Figure 9: The two cases in the proof of 𝐺f 𝐺 ′ f \ 𝐺f [PITH_FULL_IMAGE:figures/full_fig_p023_9.png] view at source ↗

**Figure 10.** Figure 10: RMWs prevent the collapsibility of segments between repeating summaries. [PITH_FULL_IMAGE:figures/full_fig_p024_10.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper closes the seven-year open question by proving undecidability of reachability under Release/Acquire even without RMW operations.

read the letter

The main point is that reachability stays undecidable for Release/Acquire programs that use only plain loads, stores, and release/acquire annotations—no RMW instructions at all. The authors settle the question left open by Abdulla et al. in 2019 and add a matching positive result: the problem becomes decidable when both context switches and RMWs are bounded at the same time. This gives a clean characterization along those two dimensions. The undecidability side comes from a reduction that encodes a known undecidable problem into RA programs while staying strictly RMW-free and respecting finite executions under the model. The decidability side uses bounding to recover a terminating procedure, probably via automata or saturation techniques. What the paper does well is tightening the earlier non-primitive-recursive lower bound into full undecidability and then completing the picture with the joint bound. The claims line up with the standard RA semantics, and the reduction construction looks deliberate about avoiding extra power. One minor soft spot is that the reduction details will need close checking to confirm no hidden RMW sneaks in and that the encoding preserves the exact memory ordering; if the construction is long, that verification could take time. No other gaps stand out. This is for people working on weak-memory verification, concurrent program analysis, and tool design for languages or hardware that rely on Release/Acquire. It deserves a serious referee because it resolves a foundational open problem with a direct reduction and a complementary decidability result.

Referee Report

0 major / 2 minor

Summary. The paper proves that reachability is undecidable for concurrent programs under the Release/Acquire memory model even in the RMW-free fragment, resolving an open question from Abdulla et al. (PLDI'19). It establishes this via a reduction and shows that decidability is recovered when both the number of context switches and RMW operations are bounded, thereby characterizing the decidability boundary along these two dimensions.

Significance. This result fully settles the decidability status of reachability under RA, identifying the minimal set of primitives (release/acquire without RMW) that already yields undecidability. The accompanying positive result on joint context/RMW bounding supplies a concrete, practical frontier for verification algorithms. The manuscript delivers a reduction-based proof from a known undecidable source problem together with a matching decidability theorem; these are clear strengths.

minor comments (2)

[Abstract] Abstract: the source undecidable problem used in the reduction is not named; adding one sentence identifying it would help readers situate the result without lengthening the abstract.
[Introduction] The high-level description of the reduction construction is clear, but a short paragraph in the introduction summarizing the key invariants preserved by the encoding (e.g., that only release/acquire accesses are used) would improve accessibility.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the paper and for recommending acceptance. We appreciate the recognition that the results settle the decidability status of reachability under Release/Acquire by establishing undecidability in the RMW-free fragment and recovering decidability under joint bounds on context switches and RMWs.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper proves undecidability of reachability for RMW-free Release/Acquire via reduction from an external undecidable problem (standard in concurrency theory, e.g., from prior results on other weak-memory models). This reduction is described as preserving RMW-free semantics and finite executions, with no self-referential definitions, parameter fitting, or load-bearing self-citations in the derivation chain. The central claim relies on an independent encoding rather than any internal construction that reduces to the paper's own inputs by definition. The positive decidability result under joint bounds is likewise a separate characterization and does not create circularity. This is the expected non-finding for a reduction-based theoretical proof.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the correctness of a reduction from a known undecidable problem (such as halting) to RMW-free RA reachability and on the standard formalization of the Release/Acquire memory model; neither is detailed in the abstract.

axioms (2)

domain assumption The semantics of Release/Acquire as defined in prior literature (Abdulla et al.)
The paper extends the model from the cited 2019 work.
standard math Reachability problems in concurrent models can be reduced from undecidable problems like the halting problem
Standard technique for proving undecidability in verification.

pith-pipeline@v0.9.0 · 5523 in / 1314 out tokens · 48129 ms · 2026-05-10T12:23:02.678851+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

24 extracted references · 23 canonical work pages

[1]

InProceedings of 8th Annual IEEE Symposium on Logic in Computer Science

Verifying programs with unreliable channels . InProceedings of 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, Los Alamitos, CA, USA, 160,161,162,163,164,165,166,167,168,169,170. doi:10.1109/LICS.1993.287591 Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna

work page doi:10.1109/lics.1993.287591 1993
[2]

In: PLDI

Verification of programs under the release-acquire semantics. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language 26 Giovanna Kobus Conrado and Andreas Pavlogiannis Design and Implementation(Phoenix, AZ, USA)(PLDI 2019). Association for Computing Machinery, New York, NY, USA, 1117–1132. doi:10.1145/3314221.3314649 Parosh Aziz Abdulla,...

work page doi:10.1145/3314221.3314649 2019
[3]

InProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 10206

Context-Bounded Analysis for POWER. InProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 10206. Springer-Verlag, Berlin, Heidelberg, 56–74. doi:10.1007/978-3-662-54580-5_4 Jade Alglave

work page doi:10.1007/978-3-662-54580-5_4
[4]

2012), 178–210

A Formal Hierarchy of Weak Memory Models.Formal Methods in System Design41, 2 (Oct. 2012), 178–210. doi:10.1007/s10703-012-0161-5 Mohamed Faouzi Atig

work page doi:10.1007/s10703-012-0161-5 2012
[5]

doi:10.1145/3458593.3458595 Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi

What is decidable under the TSO memory model?ACM SIGLOG News7, 4 (March 2021), 4–19. doi:10.1145/3458593.3458595 Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi

work page doi:10.1145/3458593.3458595 2021
[6]

In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp

On the Verification Problem for Weak Memory Models. InProceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10). Association for Computing Machinery, New York, NY, USA, 7–18. doi:10.1145/ 1706299.1706303 Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi

work page arXiv
[7]

In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11)

Mathematizing C++ Concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA, 55–66. doi:10.1145/1926385.1926394 Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche

work page doi:10.1145/1926385.1926394
[8]

168), Artur Czumaj, Anuj Dawar, and Emanuela Merelli (Eds.)

(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 168), Artur Czumaj, Anuj Dawar, and Emanuela Merelli (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 111:1–111:16. doi:10.4230/LIPIcs.ICALP.2020.111 Armando Castañeda, Gregory Chockler, Brijesh Dongol, and Ori Lahav

work page doi:10.4230/lipics.icalp.2020.111 2020
[9]

319), Dan Alistarh (Ed.)

(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 319), Dan Alistarh (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 11:1–11:22. doi:10.4230/LIPIcs.DISC.2024.11 Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan

work page doi:10.4230/lipics.disc.2024.11 2024
[10]

25th Annual European Symposium on Algorithms (ESA 2017) , pages =

On the Complexity of Bounded Context Switching.LIPIcs, Volume 87, ESA 201787 (2017), 27:1–27:15. doi:10.4230/LIPICS.ESA.2017.27 Edsger W. Dijkstra

work page doi:10.4230/lipics.esa.2017.27 2017
[11]

Pattern-Based Verification for Multithreaded Programs.ACM Trans. Program. Lang. Syst.36, 3 (Sept. 2014), 9:1–9:29. doi:10.1145/2629644 Dexter Kozen

work page doi:10.1145/2629644 2014
[12]

In18th Annual Symposium on Foundations of Computer Science (sfcs 1977)

Lower bounds for natural proof systems. In18th Annual Symposium on Foundations of Computer Science (sfcs 1977). 254–266. doi:10.1109/SFCS.1977.16 Ori Lahav and Udi Boker

work page doi:10.1109/sfcs.1977.16 1977
[13]

2022 , url =

What’s Decidable About Causally Consistent Shared Memory?ACM Transactions on Programming Languages and Systems44, 2 (June 2022), 1–55. doi:10.1145/3505273 Lamport

work page doi:10.1145/3505273 2022
[14]

Comput.C-28, 9 (Sept

How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs.IEEE Trans. Comput.C-28, 9 (Sept. 1979), 690–691. doi:10.1109/TC.1979.1675439 Madanlal Musuvathi and Shaz Qadeer

work page doi:10.1109/tc.1979.1675439 1979
[15]

SIGPLAN Not.42, 6 (June 2007), 446–455

Iterative context bounding for systematic testing of multithreaded programs. SIGPLAN Not.42, 6 (June 2007), 446–455. doi:10.1145/1273442.1250785 G.L. Peterson

work page doi:10.1145/1273442.1250785 2007
[16]

Myths about the mutual exclusion problem.Inform. Process. Lett.12, 3 (1981), 115–116. doi:10.1016/0020- 0190(81)90106-X Emil L. Post

work page doi:10.1016/0020- 1981
[17]

A variant of a recursively unsolvable problem.Bull. Amer. Math. Soc.52 (1946), 264–268. https: //api.semanticscholar.org/CorpusID:122948861 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell

1946
[18]

ACM Program

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8.Proc. ACM Program. Lang.2, POPL, Article 19 (Dec. 2018), 29 pages. doi:10.1145/3158107 On the Decidability of Verification under Release/Acquire 27 Shaz Qadeer and Jakob Rehof

work page doi:10.1145/3158107 2018
[19]

InProceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09)

The Semantics of X86-CC Multiprocessor Machine Code. InProceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09). Association for Computing Machinery, New York, NY, USA, 379–391. doi:10.1145/1480881.1480929 Ph. Schnoebelen

work page doi:10.1145/1480881.1480929
[20]

Verifying Lossy Channel Systems Has Nonprimitive Recursive Complexity.Inform. Process. Lett.83, 5 (Sept. 2002), 251–261. doi:10.1016/S0020-0190(01)00337-4 Abhishek Kr Singh and Ori Lahav

work page doi:10.1016/s0020-0190(01)00337-4 2002
[21]

Decidable Verification under Localized Release-Acquire Concurrency. InTools and Algorithms for the Construction and Analysis of Systems: 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part III(Luxembourg Ci...

work page doi:10.1007/978- 2024
[22]

ACM32, 3 (July 1985), 733–749

The complexity of propositional linear temporal logics.J. ACM32, 3 (July 1985), 733–749. doi:10.1145/3828.3837 Salvatore Torre, P. Madhusudan, and Gennaro Parlato

work page doi:10.1145/3828.3837 1985
[23]

InProceedings of the 21st International Conference on Computer Aided Verification(Grenoble, France)(CA V ’09)

Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. InProceedings of the 21st International Conference on Computer Aided Verification(Grenoble, France)(CA V ’09). Springer-Verlag, Berlin, Heidelberg, 477–492. doi:10.1007/978-3-642-02658-4_36 Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zap...

work page doi:10.1007/978-3-642-02658-4_36
[24]

InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Common Compiler Optimisations Are Invalid in the C11 Memory Model and What We Can Do about It. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, Mumbai India, 209–220. doi:10.1145/2676726.2676995 28 Giovanna Kobus Conrado and Andreas Pavlogiannis A Proofs of Section 3 A.1 Proofs of Section 3.3 Lemma...

work page doi:10.1145/2676726.2676995