{"id":"b51c501f-315a-4ccc-9167-762612355ed2","arxiv_id":"2506.08238","paper_version":3,"verdict":"REJECT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Verifying Weak Release-Acquire consistency for register machines is in O(n^5), while verifying Release-Acquire and Strong Release-Acquire is in PSPACE and both NP- and coNP-hard as claimed.","lead":"This paper studies how hard it is to check that a simple abstract machine never produces an illegal outcome under three relaxed memory models used to speed up modern processors. It finds a polynomial-time check for the weakest variant and much higher complexity for the stricter ones.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"PSPACE upper bound rests on an unproved short-circuit lemma: if minimal egraph cycles can revisit a thread many times, the O(|Θ|^2) event guess collapses.","rationale":"The paper's headline contribution for RA/SRA is the PSPACE upper bound plus lower bounds; the abstract claims PSPACE-completeness, which is already unsupported (no PSPACE-hardness proof). The most load-bearing technical premise is the short-circuit lemma in Section 4.1. Everything in the algorithm depends on being able to guess polynomially many events: the algorithm guesses the threads in the cycle, entry/exit transitions, edge types, and O(|Θ|^2) extra events, then checks realizability in NPSPACE. If minimal cycles can revisit a thread many times, the guessed run length is not polynomially bounded and the argument does not establish membership in PSPACE. The text offers only an intuitive Figure 8 and a paragraph; no formalization appears in the appendices. This is an internal gap, not a disagreement with consensus. A direct counterexample search or formalized proof would settle it. The WRA O(n^5) algorithm and the coNP-hardness construction (F.1) appear more solid and would survive; the NP-hardness label in Theorem 3.1 is separately wrong because F.2 reduces SAT to violation, i.e., to the complement. Still, the PSPACE upper bound is the central algorithmic claim for RA/SRA, so the concern is load-bearing. Since the reader identified the same weakest assumption and the verdict is already REJECT, no verdict change is needed.","tokens_in":29127,"tokens_out":6521,"duration_ms":82822,"concrete_test":"Run a brute-force or SAT-based counterexample search for the lemma: enumerate all small execution graphs with |Θ|=3, |V|=2, up to 12 events per thread, with po total per thread, rf functional, and pco a partial coherence order; check whether every simple directed cycle in po∪rf∪co has a thread appearing in at least three separated blocks while no shorter cycle exists. If such a graph exists, the short-circuit lemma is false and the PSPACE guess bound collapses. If no counterexample appears, formalize the lemma and prove by induction on cycle length that each thread can be reduced to one entry/exit; this proof must be checked against the actual cycle-surgery step used in Section 4.1.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The decisive step in the RA/SRA PSPACE membership proof (Section 4.1, 'Idea', Fig. 8) is the claim that any violating run has a cycle that can be short-circuited so that each thread is entered and exited at most once, bounding the guessed cycle by O(|Θ|^2) events. This is stated as an intuitive picture with no proof. The claim is not trivial: in a directed cycle over po∪rf∪co, a thread's events can appear in several separated blocks (enter-leave-enter-leave), and replacing the segment from first entry to last exit by a single po edge is only valid if those two endpoints are ordered by po and if deleting the intermediate events (which may belong to other threads) preserves the rest of the cycle. Neither condition is established. If a minimal violation must revisit a thread k times, the guessed event count becomes k·|Θ|^2 or worse, no longer polynomial, and the NPSPACE/PSPACE upper bound does not follow. This is distinct from the separate F.2 labeling problem (the SAT reduction proves coNP-hardness, not NP-hardness).","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":29107,"tokens_out":6768,"duration_ms":79719,"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":[{"comment":"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.","section":"Section F.2"},{"comment":"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.","section":"Section 4.1"},{"comment":"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.","section":"Abstract and Theorem 3.1"}],"minor_comments":[{"comment":"There are several typos, e.g., 'Figrue 2' and 'repreresnt'; please proofread the text.","section":"Section 2.2/2.3"},{"comment":"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.","section":"Section 3.1"},{"comment":"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.","section":"Section 4.1"},{"comment":"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.","section":"Figure 5"},{"comment":"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.","section":"Definition 2.3"}],"recommendation":"major_revision","confidential_remarks":"The NP-hardness error and the missing PSPACE proof are serious, but both are in principle fixable within a revision: the former by replacing or relabeling the reduction, the latter by either supplying a complete proof of the short-circuit lemma or downgrading the upper-bound claim. The WRA algorithm appears to be a substantive contribution, and the paper should not be rejected outright if the authors can bring the RA/SRA claims in line with what is actually proven."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the WRA polynomial-time algorithm is a real contribution, and the coNP-hardness reduction is plausible, but the RA/SRA PSPACE upper bound is not proven in the text, and the NP-hardness claim is a labeling mistake. Treat the abstract's 'PSPACE-complete' as noise; the body never proves PSPACE-hardness.\n\nWhat's actually new: this is the first complexity classification for verifying RA-family consistency over register machines. The WRA O(n^5) algorithm is the strongest part. The summary-tuple data structures are O(n^4), the iteration is monotone, and the appendix gives a reasonably complete correctness proof for the fixed-point rules. The coNP-hardness reduction from tautology is standard in shape and, as far as I can tell, sound.\n\nSoft spots, in order of severity. First, the PSPACE membership proof for RA and SRA depends on a short-circuit lemma in Section 4.1 that is asserted with a figure and a paragraph but not proved. The lemma says a minimal violating cycle can be reduced so each thread is entered and exited at most once, bounding the guessed cycle to O(|Theta|^2) events. That is exactly what keeps the non-deterministic guess polynomial. The stress-test concern holds up: a thread's events in a directed cycle over po/rf/co can appear in several blocks, and deleting intermediate events may cut through other threads' dependencies. The paper does not show the reduced cycle is still realizable by the register machine. Without a proof of this lemma, the PSPACE upper bound is not established. This is load-bearing.\n\nSecond, the claimed NP-hardness is not established. The reduction in F.2 maps a SAT formula to a machine that violates RA iff the formula is satisfiable. That is a reduction from SAT to the complement of RA-Cons, hence coNP-hardness of RA-Cons, not NP-hardness. The theorem statement saying 'both NP- and coNP-hard' is therefore wrong. The conclusion repeats it. Easy to fix by rewriting the claim as coNP-hardness, or by providing a genuine NP reduction.\n\nThe rest looks careful: Lemma 2.6/2.7 on differentiated runs is fine, and the WRA appendix is much more detailed than the RA/SRA part. The paper is worth a serious referee because the WRA result matters, but the current version should be rejected or heavily revised. I'd send it to a strong venue, with the expectation that the authors either prove the short-circuit lemma or state the PSPACE membership as a conjecture, and correct the NP-hardness claim.","headline":"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.","tokens_in":29859,"tokens_out":3884,"would_cite":true,"duration_ms":42754,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68Q17","68Q25","68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["weak memory models","Release-Acquire semantics","register machines","consistency verification","execution graphs","PSPACE","polynomial-time algorithm","coNP-hardness"],"falsifier":"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.","tokens_in":28715,"feed_emoji":"⚙️","tokens_out":8309,"duration_ms":93450,"temperature":0.7,"pith_summary":"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.","feed_headline":"Polynomial-time check found for weak Release-Acquire","feed_subtitle":"RA and SRA variants are decidable in PSPACE and are NP- and coNP-hard","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines the RA and SRA axiomatic models and the modification-order invariant that the paper's execution-graph semantics use.","marker":"[19]"},{"why":"Supplies the happens-before formulation and the causal-consistency correspondence that frame the three variants.","marker":"[18]"},{"why":"Establishes the register-machine data-independence argument and gives an EXPSPACE verification result for a WRA-equivalent model, the baseline the paper improves to polynomial time.","marker":"[9]"},{"why":"Gives the polynomial consistency-testing algorithms for RA, SRA, and WRA that the paper's verification results extend.","marker":"[26]"},{"why":"Provides the data-independence principle used in Lemma 2.7 to reduce verification to differentiated runs.","marker":"[27]"}],"fun_headline_variants":["Weak Release-Acquire verification is polynomial-time","RA and SRA verification is PSPACE-complete","Weak RA check in O(n^5); strong variants PSPACE-complete","Verifying strong release-acquire is PSPACE-complete","Polynomial verification for weak RA; PSPACE for strong"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Weak Release-Acquire verification is polynomial-time","RA and SRA verification is PSPACE-complete","Weak RA check in O(n^5); strong variants PSPACE-complete","Verifying strong release-acquire is PSPACE-complete","Polynomial verification for weak RA; PSPACE for strong"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000904,"raw_usage":{"total_tokens":3844,"prompt_tokens":857,"completion_tokens":2987,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":473,"completion_tokens_details":{"reasoning_tokens":2905}},"tokens_in":473,"tokens_out":2987,"duration_ms":26639,"temperature":1.0,"reasoning_tokens":2905,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:19:51.816627+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Taming release-acquire consistency","cited_arxiv_id":null,"evidence_quote":"Defines the RA and SRA axiomatic models and the modification-order invariant that the paper's execution-graph semantics use."},{"cited_title":"What's decidable about causally consistent shared memory? ACM Trans","cited_arxiv_id":null,"evidence_quote":"Supplies the happens-before formulation and the causal-consistency correspondence that frame the three variants."},{"cited_title":"On verifying causal consistency","cited_arxiv_id":null,"evidence_quote":"Establishes the register-machine data-independence argument and gives an EXPSPACE verification result for a WRA-equivalent model, the baseline the paper improves to polynomial time."},{"cited_title":"Optimal reads-from consistency checking for c11-style memory models","cited_arxiv_id":null,"evidence_quote":"Gives the polynomial consistency-testing algorithms for RA, SRA, and WRA that the paper's verification results extend."},{"cited_title":"Expressing interesting properties of programs in propositional temporal logic","cited_arxiv_id":null,"evidence_quote":"Provides the data-independence principle used in Lemma 2.7 to reduce verification to differentiated runs."}],"review_version":1}