Pith. sign in

REVIEW 3 major objections 5 minor 27 references

The complexity of verifying the release-acquire semantics over register machines

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Verification of Weak Release-Acquire consistency on register machines is polynomial-time, while RA and SRA verification are decidable in PSPACE and are NP- and coNP-hard.

desk verdict Real WRA algorithm and plausible coNP-hardness, but the RA/SRA PSPACE upper bound rests on an unproved short-circuit lemma and the NP-hardness claim is mislabeled. read the letter →

arxiv 2506.08238 v3 pith:A6GHARGA submitted 2025-06-09 cs.PL

Parosh Abdulla , Elli Anastasiadi , Mohamed Faouzi Atig , Léo Exibard , Samuel Grahn This is my paper
classification cs.PL MSC 68Q6068Q1768Q2568Q85
keywords weakmemorymodelsRelease-AcquiresemanticsregistermachinesconsistencyverificationexecutiongraphsPSPACEpolynomial-timealgorithmcoNP-hardness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Consistency models for weak memory are usually checked on one execution at a time; the harder question is whether an implementation can ever produce a run that violates the model. This paper studies that verification problem for Release-Acquire (RA), Strong Release-Acquire (SRA), and Weak Release-Acquire (WRA), with the implementation described as a register machine whose registers hold values from an unbounded domain. It establishes that WRA verification is decidable in $O(n^5)$ time, while RA and SRA verification are decidable in PSPACE and are both NP- and coNP-hard. The significance is that the verification question was poorly understood in this setting; for WRA the result gives a practical polynomial bound, and for RA and SRA it gives a concrete space-bounded search procedure.

What carries the argument

The central objects are execution graphs whose nodes are read/write events and whose edges are program order, reads-from, and coherence; each of the three memory models is a forbidden-cycles condition on these relations. For WRA-Cons the algorithm is a backward reachability fixed-point computation that maintains small summary tuples called fragile and exposed, recording which threads could reach a read through the happens-before relation; the propagation rules are monotone, so the $O(n^4)$-sized data structures bound the number of iterations. For RA-Cons and SRA-Cons the PSPACE algorithm rests on a short-circuit lemma: if a violating run's execution graph has a cycle, a shorter run with $O(|\Theta|^2)$ events can be produced by replacing, inside each thread, the stretch between the first event entering the cycle and the last event exiting it with a single program-order edge, while keeping the run realizable by the register machine.

What would settle it

Find a register machine family whose only runs violating RA or SRA force a minimal cycle to enter the same thread more than once, so the short-circuit jump cannot be made without losing realizability; such machines would falsify the PSPACE membership argument. Equivalently, exhibit a machine family whose minimal violating cycles have superquadratic length in the number of threads.

Watch

Extended reading notes

Core claim

On a register machine of size $n$, the paper's Theorem 3.1 asserts three bounds. WRA-Cons, checking whether every run satisfies Weak Release-Acquire, is solvable in $O(n^5)$ time. RA-Cons and SRA-Cons are each in PSPACE and are hard for both NP and coNP. The abstract describes the RA/SRA result as PSPACE-complete, while the formal theorem proves membership in PSPACE together with NP- and coNP-hardness, not PSPACE-hardness. The algorithmic contribution is a method for exploring only finitely many runs even though the machine's data domain and run set are infinite, with reductions from tautology and SAT supplying the lower bounds.

Load-bearing premise

The PSPACE upper bound for RA and SRA rests on the short-circuit lemma: any minimal violating cycle can be compressed to $O(|\Theta|^2)$ events by jumping within each thread from its first cycle event to its last, and the compressed run is still a realizable run of the register machine.

Editorial extensions

If this is right

  • A correct $O(n^5)$ WRA algorithm means implementations modeled as register machines can be verified automatically, not just tested on individual runs.
  • For RA and SRA, verification is decidable in polynomial space, so an exhaustive but space-bounded search over candidate violating runs is possible.
  • The coNP-hardness of RA and SRA means no simple polynomial-size witness can certify consistency for these models unless the polynomial hierarchy collapses.
  • The NP-hardness reduction means finding a violating run can encode Boolean satisfiability, so the problem has genuine computational content.
  • The reductions and algorithms move the testing-to-verification gap from an open question to concrete complexity bounds.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: if the short-circuit lemma is correct, the true complexity of RA and SRA verification may be lower than PSPACE; the authors note that reachability between register configurations might be solvable in NP, which would put the problems in coNP.
  • Editorial inference: the register-machine devices used in the hardness proofs suggest similar NP/coNP dichotomies for nearby declarative models whose acyclicity conditions are small variations, such as PSI.
  • Editorial inference: the polynomial WRA bound points to copy operations between registers as a source of hardness; extending register machines with compare-and-swap or data-dependent transitions is likely to push complexity into well-structured-system territory.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper studies the verification problem for three release-acquire memory-model variants over register machines. For a register machine of size n, it claims that WRA verification is decidable in O(n^5) time, that RA and SRA verification are in PSPACE and are both NP- and coNP-hard, and it sketches algorithms and reductions to support these claims. The main techniques are a backward-reachability algorithm for WRA, a short-circuit argument intended to bound the size of a minimal violating execution graph, and reductions from Tautology and SAT.

Significance. If the results were fully proven, the WRA polynomial-time algorithm and the decidability plus PSPACE upper bound for RA/SRA would be a useful contribution to verification under weak-memory models. The register-machine formulation is a natural abstraction, and the reduction to differentiated runs is a helpful step. However, the central complexity claims are not yet supported: the NP-hardness direction is proved by a reduction to the wrong language, the PSPACE upper bound depends on an unproved structural lemma, and the abstract overstates the result as PSPACE-complete. The WRA algorithm and its proof in Appendix E are the most developed part of the manuscript.

major comments (3)
  1. [Section F.2] The claimed NP-hardness reduction constructs a register machine M such that M̸|= RA iff the input 3CNF formula φ is satisfiable. This is a many-one reduction from SAT to the complement of RA-Cons, so it proves coNP-hardness of RA-Cons (equivalently, NP-hardness of the violation language), not NP-hardness of RA-Cons as stated in Theorem 3.1. Since Section F.1 already proves coNP-hardness via Tautology, the NP-hardness assertion is unsupported. Please either supply a reduction from SAT to RA-Cons itself, or weaken the theorem and abstract to claim only coNP-hardness.
  2. [Section 4.1] The PSPACE membership proof rests on the short-circuit claim that a minimal violating execution-graph cycle can be reduced to O(|Θ|^2) events, entering and exiting each thread at most once. This is presented only as an intuitive idea with Figure 8; no formal lemma or proof is given. The text says the full proofs are in Appendices C–F, but none of those appendices contains this argument. Since the polynomial event bound is the sole justification for guessing only polynomially many reserved events in the NPSPACE algorithm, the PSPACE upper bound is not established without a rigorous proof of this lemma.
  3. [Abstract and Theorem 3.1] The abstract states that verifying RA and SRA is 'PSPACE complete,' but Theorem 3.1 only claims PSPACE membership together with NP- and coNP-hardness, and no PSPACE-hardness proof appears anywhere in the body. The abstract must be corrected to match the proven statement, and the unresolved gap between the lower bounds and the PSPACE upper bound should be stated explicitly.
minor comments (5)
  1. [Section 2.2/2.3] There are several typos, e.g., 'Figrue 2' and 'repreresnt'; please proofread the text.
  2. [Section 3.1] The data-structure size is given as O(|Q|·|V|·|Regs|·|Θ∪Regs|) and then simplified to O(n^4). The definition of the machine size n should explicitly state that all of |Q|, |V|, |Regs|, and |Θ| are counted in n, otherwise the simplification is not justified.
  3. [Section 4.1] The number of reserved events is first said to be bounded by 2·|Θ|^2 but later written as 'n^2-many events'; please clarify the relationship between n and |Θ| and use a single consistent bound.
  4. [Figure 5] The rules containing 'or' are described as standing for two rules each, but this is not formalized in the figure or the surrounding text; please state this convention explicitly near the figure.
  5. [Definition 2.3] The notation in the WRA clause, e.g., '[W∧w·var]·hb·w·hb·rf^{-1}', uses relation composition over an event w without defining how an event is treated as a relation; please add a formal definition of this notation.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the PSPACE and O(n^5) results are derived from the declared memory-model semantics and external SAT/TAUT reductions; the unproved short-circuit lemma is an unproved premise, not a circular reduction.

full rationale

The paper's central claims do not reduce to their own inputs. The WRA O(n^5) procedure (Sections 3.1-3.2) is a backward reachability algorithm whose correctness is proved in Appendix E against the execution-graph update rules of Fig. 3; Proposition 3.2 decomposes the WRA definition (acyclicity of [W∧w.var]·hb·w·hb·rf^-1) into ghost-read, mismatched-variable, and exposed-read conditions, and the soundness/completeness of the exposed-read module is argued from the semantics, not assumed. The RA/SRA PSPACE membership argument (Section 4.1, 'Idea', Fig. 8) does contain a fragile, unproved structural claim: 'if a cycle enters the same thread multiple times we are able to short-circuit the egraph cycle by jumping directly from the first entry event ... to the event where the cycle exits that thread for the final time ... and instead following po edges,' which yields the O(|Theta|^2) event bound. If this short-circuit lemma fails, the PSPACE upper bound would not follow; but this is a correctness/complexity gap, not circularity, because the lemma is not identical to the theorem's conclusion and is not derived from that conclusion. The NP- and coNP-hardness proofs (Appendix F) are many-one reductions from SAT and TAUT and are independent of the authors' prior work. Self-citations ([1], [26], [6]) are background on the testing problem and a prototype tool; none carries the verification theorems. Lemmas 2.6 and 2.7 are supported by the text's own constructions (completion of pco, appended meta-counter) and external data-independence references. The abstract's 'PSPACE complete' wording is stronger than the body's 'in PSPACE and both NP- and coNP-hard,' but that is an overclaim, not circular reasoning. No circular step can be exhibited as an equation-by-construction equality or a fitted parameter renamed as a prediction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No fitted parameters or invented entities appear; the paper is a complexity-theoretic analysis. Its assumptions are the standard declarative definitions of the memory models, the data-independence of register machines, and standard complexity theorems.

assumptions (4)
  • domain assumption The register machine model has no data-dependent transitions, so all runs are data-independent and value renaming preserves transition sequences (Lemma 2.7, Section 4.1).
    Used to reduce to differentiated runs and to justify guessing only register-value flow without tracking concrete data values.
  • standard math Savitch's theorem, NPSPACE = PSPACE, is used to convert the non-deterministic polynomial-space algorithm into a PSPACE membership proof (Section 4.1).
    The paper explicitly says the algorithm is NPSPACE and 'that is enough to prove the problem is in PSPACE'.
  • domain assumption The declarative characterizations of RA, SRA, and WRA in Definition 2.3 are taken as given from Lahav et al. [19] and Lahav and Boker [18]; the results inherit their correctness.
    The paper does not re-derive these memory model definitions; they are the external benchmarks the verification problem is defined against.
  • standard math The correctness of the execution-graph update rules in Figure 3, which determine when a run corresponds to a valid execution graph, is assumed from the axiomatic memory model literature.
    Used throughout to tie register-machine runs to execution graphs; no proof given in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The complexity of verifying the release-acquire semantics over register machines." pith.science (2026). https://pith.science/paper/A6GHARGA

@misc{pith2026250608238,
  author       = {Pith},
  title        = {Pith review of: The complexity of verifying the release-acquire semantics over register machines},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/A6GHARGA}},
  note         = {Machine review of arXiv:2506.08238}
}
read the original abstract

The Release-Acquire (RA) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed systems. Several steps have been taken in the direction of testing such semantics, where one is interested in whether a single program execution is consistent with a memory model. The more general verification problem, i.e., checking whether any allowed program run is consistent with a memory model, has still not been studied as much. The purpose of this work is to bridge this gap. We tackle the verification problem, where, given an implementation described as a register machine, we check if any of its runs violates the RA semantics or its Strong (SRA) and Weak (WRA) variants. We show that verifying WRA in this setup is in O(n5 ), while verifying the RA and SRA is PSPACE complete. This both answers some fundamental questions about the complexity of these problems, but also provides insights on the expressive power of register machines as a model.

Figures

Figures reproduced from arXiv: 2506.08238 by the authors.

Figure 16
Figure 16. For the proof of the reverse implication we assume such a cycle. We therefore get that for each clause there must have existed a variable which caused the copying of bci to aci . Consequently after performing the variable assignment phase this copying was triggered by some variable in each clause, which means that this assignment “disagreed” in some literal with each clause, and therefore invalidates the whole formu… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    Optimal stateless model checking under the release-acquire semantics

    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. , 2( OOPSLA ):135:1--135:29, 2018

    work page 2018

  2. [2]

    General decidability theorems for infinite-state systems

    Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih - Kuen Tsay. General decidability theorems for infinite-state systems. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996 , pages 313--321. IEEE Computer Society, 1996

    work page 1996

  3. [3]

    Burns, Prince Kohli, and Phillip W

    Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, and Phillip W. Hutto. Causal memory: Definitions, implementation, and programming. Distributed Comput. , 9(1):37--49, 1995

    work page 1995

  4. [4]

    Herding cats: Modelling, simulation, testing, and data mining for weak memory

    Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. , 36(2):7:1--7:74, 2014

    work page 2014

  5. [5]

    McMillan, and Doron A

    Rajeev Alur, Kenneth L. McMillan, and Doron A. Peled. Model-checking of correctness conditions for concurrent objects. Inf. Comput. , 160(1-2):167--188, 2000

    work page 2000

  6. [6]

    Ccchecker

    Anonymous. Ccchecker. Anonymized implementation

    work page

  7. [7]

    Clarifying and compiling C/C++ concurrency: from C++11 to POWER

    Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. Clarifying and compiling C/C++ concurrency: from C++11 to POWER . In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012 , pages 509--520....

    work page 2012

  8. [8]

    Mathematizing C++ concurrency

    Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++ concurrency. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011 , pages 55--66. ACM , 2011

    work page 2011

Show all 27 references
  1. [9]

    On verifying causal consistency

    Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. On verifying causal consistency. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20...

    2017

  2. [10]

    Principles of eventual consistency

    Sebastian Burckhardt. Principles of eventual consistency. Found. Trends Program. Lang. , 1(1-2):1--150, 2014

    2014

  3. [11]

    Constraint-based verification of parameterized cache coherence protocols

    Giorgio Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst. Des. , 23(3):257--301, 2003

    2003

  4. [12]

    Scalable tree-based register automata learning

    Simon Dierl, Paul Fiterau - Brostean, Falk Howar, Bengt Jonsson, Konstantinos Sagonas, and Fredrik T quist. Scalable tree-based register automata learning. In Bernd Finkbeiner and Laura Kov \' a cs, editors, Tools and Algorithms for the Construction and Analysis of Systems - 3...

    2024

  5. [13]

    Well-structured transition systems everywhere! Theor

    Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci. , 256(1-2):63--92, 2001

    2001

  6. [14]

    Automata-based automated detection of state machine bugs in protocol implementations

    Paul Fiterau - Brostean, Bengt Jonsson, Konstantinos Sagonas, and Fredrik T quist. Automata-based automated detection of state machine bugs in protocol implementations. In 30th Annual Network and Distributed System Security Symposium, NDSS 2023, San Diego, California, USA, Feb...

    2023

  7. [15]

    Gibbons and Ephraim Korach

    Phillip B. Gibbons and Ephraim Korach. Testing shared memories. SIAM J. Comput. , 26(4):1208--1244, 1997

    1997

  8. [16]

    Effective stateless model checking for C/C++ concurrency

    Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. , 2( POPL ):17:1--17:32, 2018

    2018

  9. [17]

    Kater: Automating weak memory model metatheory and consistency checking

    Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis. Kater: Automating weak memory model metatheory and consistency checking. Proc. ACM Program. Lang. , 7( POPL ):544--572, 2023

    2023

  10. [18]

    What's decidable about causally consistent shared memory? ACM Trans

    Ori Lahav and Udi Boker. What's decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. , 44(2):8:1--8:55, 2022

    2022

  11. [19]

    Taming release-acquire consistency

    Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. Taming release-acquire consistency. In Rastislav Bod \' k and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 , pages 649--662, St. Petersb...

    2016

  12. [20]

    C11tester: a race detector for C/C++ atomics

    Weiyu Luo and Brian Demsky. C11tester: a race detector for C/C++ atomics. In Tim Sherwood, Emery D. Berger, and Christos Kozyrakis, editors, ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Virtual Event, U...

    2021

  13. [21]

    Causal consistency: beyond memory

    Matthieu Perrin, Achour Most \' e faoui, and Claude Jard. Causal consistency: beyond memory. In Rafael Asenjo and Tim Harris, editors, Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16, 2...

    2016

  14. [22]

    On parallel snapshot isolation and release/acquire consistency

    Azalea Raad, Ori Lahav, and Viktor Vafeiadis. On parallel snapshot isolation and release/acquire consistency. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory ...

    2018

  15. [23]

    Synchronising C/C++ and POWER

    Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. Synchronising C/C++ and POWER . In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLD...

    2012

  16. [24]

    Efficient and correct execution of parallel programs that share memory

    Dennis Shasha and Marc Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. , 10(2):282–312, April 1988

    1988

  17. [25]

    Aguilera, and Jinyang Li

    Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. Transactional storage for geo-replicated systems. In Ted Wobber and Peter Druschel, editors, Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, SOSP 2011, Cascais, Portugal, October 23-26,...

    2011

  18. [26]

    Optimal reads-from consistency checking for c11-style memory models

    H \" u nkar Can Tun c , Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, and Andreas Pavlogiannis. Optimal reads-from consistency checking for c11-style memory models. Proc. ACM Program. Lang. , 7( PLDI ):761--785, 2023

    2023

  19. [27]

    Expressing interesting properties of programs in propositional temporal logic

    Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986 , pages 184--193. ACM Press, 1986

    1986

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.