arxiv: 2605.13780 · v1 · submitted 2026-05-13 · 💻 cs.PL

Recognition: no theorem link

On the Complexity of Checking Soundness of Natural Reductions (Extended Version)

Constantin Enea , Azadeh Farzan , Dominik Klumpp

Authors on Pith no claims yet

Pith reviewed 2026-05-14 17:25 UTC · model grok-4.3

classification 💻 cs.PL

keywords natural reductionssoundnesscommutativity relationsconcurrent verificationcomputational complexitylockingparameterized programsinterleavings

0 comments

The pith

Deciding whether a natural reduction is sound with respect to a commutativity relation is coNP-hard even for locking synchronization.

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

The paper defines natural reductions as syntactic restrictions on interleavings in parameterized concurrent programs, obtained by inserting atomic blocks and global rendezvous points into each thread template. It asks whether a given such reduction is sound, meaning it preserves all behaviors needed for correctness with respect to an explicitly given commutativity or semi-commutativity relation. When threads have no synchronization, a polynomial-time algorithm decides soundness exactly. Once synchronization is added, the same decision problem is already coNP-hard for the simple case of locking. The result matters because reductions are a common way to simplify verification of concurrent systems, yet the step of confirming that a chosen reduction is safe becomes intractable under routine synchronization.

Core claim

The central claim is that soundness of a natural reduction relative to a given (semi-)commutativity relation is decidable in polynomial time in the absence of synchronization, while the problem is coNP-hard in general and remains coNP-hard already when the only synchronization primitive is locking.

What carries the argument

Natural reductions obtained by adding atomic blocks and global rendezvous points to the thread template of a parameterized program.

If this is right

Soundness checking can be performed efficiently when the program uses no synchronization.
Any verification technique relying on natural reductions must treat soundness checking as intractable once locking or similar mechanisms appear.
Lower bounds apply parametrically to whatever synchronization mechanism is chosen.
Proofs that use natural reductions with synchronization cannot assume that soundness is easy to establish.

Where Pith is reading between the lines

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

Tool builders may need to limit natural reductions to the no-synchronization fragment or accept that soundness must be checked by expensive methods.
The purely syntactic definition may not capture data-dependent synchronization that appears in actual code, potentially narrowing the practical scope of the hardness result.
One could test whether the hardness threshold changes when rendezvous points are allowed to carry data or when the commutativity relation is computed rather than given.

Load-bearing premise

Reductions are purely syntactic, atomic blocks and rendezvous points are inserted directly into the thread template, and the commutativity relation is supplied explicitly as input.

What would settle it

A polynomial-time algorithm that correctly decides soundness for natural reductions under locking synchronization would refute the coNP-hardness result.

Figures

Figures reproduced from arXiv: 2605.13780 by Azadeh Farzan, Constantin Enea, Dominik Klumpp.

**Figure 1.** Figure 1: Action b cannot escape to the left/right of the atomic block z1 . . . zm. escape to the right either, due to the presence of an action ⟨c : t2⟩ such that (b, c) ∈/ I. In order for ⟨b : t1⟩ to escape to the right, ⟨c : t2⟩ would also have to escape to the right, but we have (c, zj ) ∈/ I. As shown here, even if individual actions interleaved in an atomic block can escape, in general we have to reason about … view at source ↗

**Figure 2.** Figure 2: Examples for incompleteness of mover reasoning. [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗

**Figure 3.** Figure 3: Thread template for a clause C2 ≡ (x ∨ ¬y ∨ ¬z) in φ ≡ C1 ∧ C2 ∧ C3 [PITH_FULL_IMAGE:figures/full_fig_p028_3.png] view at source ↗

**Figure 4.** Figure 4: Thread template for the reduction of coverability with locks to sound [PITH_FULL_IMAGE:figures/full_fig_p030_4.png] view at source ↗

read the original abstract

The verification of reductions, representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syntactic reductions, which we call natural reductions. Natural reductions are specified by introducing atomic blocks and global rendezvous points in the parameterized program's thread template. We study the problem of deciding whether a given natural reduction is sound wrt. a given (semi-)commutativity relation. In the case that there is no synchronization between threads, we present a sound and complete polynomial-time algorithm. In the case where synchronization is considered, we provide a general lower bound for the problem (parametric in the synchronization mechanism), and show that the problem is coNP-hard already for a simple mechanism like locking.

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

The paper gives a P-time algorithm for soundness of natural reductions without synchronization and proves coNP-hardness for the locking case.

read the letter

The main takeaway is that checking whether a natural reduction is sound is polynomial-time solvable with no synchronization between threads but coNP-hard once locking enters the picture. The paper defines natural reductions syntactically by inserting atomic blocks and global rendezvous points into the thread template, then studies the decision problem relative to a given commutativity relation. For the no-sync case it supplies a sound and complete P-time algorithm. For synchronization it states a general lower bound that depends on the mechanism and specializes it to locking to obtain the hardness result. This separation is new relative to earlier work on reduction soundness and is the part that could actually guide algorithm design for reduction-based verifiers. The syntactic restriction and the assumption that the commutativity relation is supplied as input keep the problem well-defined. The hardness claim for locking is the spot that needs checking. The construction likely requires a number of distinct locks that grows with the instance size, so the mechanism is not a single fixed primitive but scales with the problem. That makes the phrasing “a simple mechanism like locking” slightly loose; the hardness may stem more from unbounded lock identifiers than from locking per se. The full proofs are not visible in the abstract, so any referee would want to inspect the reduction for gaps. This work is aimed at researchers in parameterized concurrent verification who rely on reductions to cut down interleavings. A reader who builds or analyzes reduction-based tools would find the complexity map useful. It deserves serious peer review because the claims are precise and the problem is relevant, even if the hardness details require verification.

Referee Report

2 major / 2 minor

Summary. The paper introduces an expressive class of syntactic reductions called natural reductions, defined by inserting atomic blocks and global rendezvous points into the thread template of a parameterized concurrent program. It studies the decision problem of whether a given natural reduction is sound with respect to a provided (semi-)commutativity relation. For the no-synchronization case, the paper presents a sound and complete polynomial-time algorithm. For the synchronized case, it establishes a general lower bound parametric in the synchronization mechanism and proves that the problem is coNP-hard already for locking.

Significance. If the central claims hold, the work provides useful complexity-theoretic insights into reduction verification for parameterized concurrent programs, a key technique for scalable correctness proofs. The polynomial-time algorithm for the unsynchronized case is a clear positive contribution that could be directly applicable. The coNP-hardness result for locking delineates when soundness checking becomes intractable, though its practical relevance hinges on whether the locking model remains 'simple' under the reduction construction.

major comments (2)

[Abstract] Abstract and hardness section: the claim that soundness checking is coNP-hard 'already for a simple mechanism like locking' needs explicit clarification on whether the number of distinct lock identifiers is bounded by a constant or grows with the size of the input instance (e.g., the UNSAT formula). If the latter, the hardness may derive from an unbounded family of synchronization primitives rather than a fixed simple mechanism, weakening the interpretation of the result.
[Hardness proof] Hardness proof (likely the section presenting the coNP-hardness reduction): provide the explicit construction showing how the locking-based natural reduction encodes a coNP-complete problem such as UNSAT, including how the commutativity relation is supplied as input and how the thread template is instantiated. Without this, it is difficult to verify that the reduction is polynomial and that the soundness question directly corresponds to the source problem.

minor comments (2)

Ensure the definition of 'natural reduction' (atomic blocks plus global rendezvous points) is stated formally with precise syntax before the complexity results are presented.
[Polynomial algorithm section] For the polynomial-time algorithm in the no-synchronization case, include a brief complexity analysis (e.g., O(n^k) bound) and pseudocode or high-level steps to make the procedure reproducible.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and valuable comments on the abstract claim and the hardness proof. We address each point below and will incorporate clarifications and expansions into the revised manuscript.

read point-by-point responses

Referee: [Abstract] Abstract and hardness section: the claim that soundness checking is coNP-hard 'already for a simple mechanism like locking' needs explicit clarification on whether the number of distinct lock identifiers is bounded by a constant or grows with the size of the input instance (e.g., the UNSAT formula). If the latter, the hardness may derive from an unbounded family of synchronization primitives rather than a fixed simple mechanism, weakening the interpretation of the result.

Authors: We agree that explicit clarification is warranted. In our reduction from UNSAT, the locking mechanism employs a constant number of distinct lock identifiers (specifically two locks) that remains fixed and independent of the input formula size. The hardness arises from the encoding of clause-variable interactions within the natural reduction and the supplied commutativity relation, not from scaling the number of locks. We will revise the abstract and hardness section to state this explicitly. revision: yes
Referee: [Hardness proof] Hardness proof (likely the section presenting the coNP-hardness reduction): provide the explicit construction showing how the locking-based natural reduction encodes a coNP-complete problem such as UNSAT, including how the commutativity relation is supplied as input and how the thread template is instantiated. Without this, it is difficult to verify that the reduction is polynomial and that the soundness question directly corresponds to the source problem.

Authors: The manuscript's hardness section already presents the polynomial-time reduction from UNSAT: the thread template is instantiated by creating one thread per clause with atomic blocks guarded by the fixed locks to simulate variable assignments, and the commutativity relation (provided as input) consists of all pairs of actions that do not access the same variable. Soundness of the resulting natural reduction holds if and only if the formula is unsatisfiable. To address the concern, we will expand this section with a concrete small-formula example, explicit pseudocode for the template instantiation, and a proof sketch confirming polynomial size and direct correspondence. revision: yes

Circularity Check

0 steps flagged

No circularity: standard complexity reduction for decision problem

full rationale

The paper establishes a polynomial-time algorithm for soundness checking without synchronization and a coNP-hardness lower bound for the locking case. These are proven via explicit constructions that reduce from known coNP-complete problems (such as UNSAT) to the soundness decision problem. The constructions are syntactic and parametric in the given commutativity relation and thread template; no step equates a derived quantity to its own input by definition, renames a fitted parameter as a prediction, or relies on a load-bearing self-citation whose justification is internal to the paper. The result is a self-contained complexity-theoretic statement.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on the assumption that natural reductions are defined syntactically via atomic blocks and rendezvous points and that soundness is defined with respect to an arbitrary given (semi-)commutativity relation. No free parameters or invented entities are introduced.

axioms (2)

domain assumption Natural reductions are specified solely by inserting atomic blocks and global rendezvous points into the thread template.
This syntactic restriction is used to obtain the polynomial-time algorithm and is stated in the abstract.
domain assumption Soundness is defined with respect to a given (semi-)commutativity relation.
The decision problem is parameterized by this relation; the abstract treats it as input.

invented entities (1)

natural reduction no independent evidence
purpose: A syntactic class of reductions for parameterized concurrent programs that simplifies interleaving verification.
New class introduced in the paper; no independent evidence outside the definition is provided.

pith-pipeline@v0.9.0 · 5415 in / 1422 out tokens · 53694 ms · 2026-05-14T17:25:38.251357+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages

[1]

In: ESOP

Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: ESOP. pp. 290–309. Lecture Notes in Com- puter Science, Springer (2013). https://doi.org/10.1007/978-3-642-37036-6_17

work page doi:10.1007/978-3-642-37036-6_17 2013
[2]

In: OSDI

Chajed, T., Kaashoek, M.F., Lampson, B.W., Zeldovich, N.: Verifying concurrent software using movers in CSPEC. In: OSDI. pp. 306–322. USENIX Association (2018)

work page 2018
[3]

In: PODC

Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: PODC. pp. 44–65. ACM (1988). https://doi.org/10. 1145/62546.62556

work page arXiv 1988
[4]

In: The Book of Traces, pp

Clerbout, M., Latteux, M., Roos, Y.: Semi-commutations. In: The Book of Traces, pp. 487–552. World Scientific (1995). https://doi.org/10.1142/9789814261456_ 0012

work page doi:10.1142/9789814261456_ 1995
[5]

In: CAV (2)

Damian, A., Dragoi, C., Militaru, A., Widder, J.: Communication-closed asyn- chronous protocols. In: CAV (2). pp. 344–363. Lecture Notes in Computer Science, Springer (2019). https://doi.org/10.1007/978-3-030-25543-5_20

work page doi:10.1007/978-3-030-25543-5_20 2019
[6]

Elrad,T.,Francez,N.:Decompositionofdistributedprogramsintocommunication- closed layers. Sci. Comput. Program. 2(3), 155–173 (1982). https://doi.org/10. 1016/0167-6423(83)90013-8 On the Complexity of Checking Soundness of Natural Reductions 19

work page 1982
[7]

In: STACS

Esparza, J.: Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In: STACS. pp. 1–10. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014). https://doi.org/10.4230/LIPICS.STACS.2014.1

work page doi:10.4230/lipics.stacs.2014.1 2014
[8]

In: PLDI

Farzan, A., Klumpp, D., Podelski, A.: Sound sequentialization for concurrent pro- gram verification. In: PLDI. pp. 506–521. ACM (2022). https://doi.org/10.1145/ 3519939.3523727

work page arXiv 2022
[9]

Farzan, A., Klumpp, D., Podelski, A.: Commutativity simplifies proofs of para- meterized programs. Proc. ACM Program. Lang. 8(POPL), 2485–2513 (2024). https://doi.org/10.1145/3632925

work page doi:10.1145/3632925 2024
[10]

In: TACAS

Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: TACAS. pp. 155–169. Lecture Notes in Computer Science, Springer (2009). https://doi.org/10.1007/978-3-642-00768-2_14

work page doi:10.1007/978-3-642-00768-2_14 2009
[11]

Farzan, A., Vandikas, A.: Reductions for safety proofs. Proc. ACM Program. Lang. 4(POPL), 13:1–13:28 (2020). https://doi.org/10.1145/3371081

work page doi:10.1145/3371081 2020
[12]

Flanagan, C., Freund, S.N.: The anchor verifier for blocking and non-blocking con- current software. Proc. ACM Program. Lang.4(OOPSLA), 156:1–156:29 (2020). https://doi.org/10.1145/3428224

work page doi:10.1145/3428224 2020
[13]

von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend syn- chrony:synchronousverificationofasynchronousdistributedprograms.Proc.ACM Program. Lang. 3(POPL), 59:1–59:30 (2019). https://doi.org/10.1145/3290372

work page doi:10.1145/3290372 2019
[14]

In: CAV (2)

Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modu- lar refinement reasoning for concurrent programs. In: CAV (2). pp. 449–465. Lecture Notes in Computer Science, Springer (2015). https://doi.org/10.1007/ 978-3-319-21668-3_26

work page 2015
[15]

In: PLDI

Kragl, B., Enea, C., Henzinger, T.A., Mutluergil, S.O., Qadeer, S.: Inductive se- quentialization of asynchronous programs. In: PLDI. pp. 227–242. ACM (2020). https://doi.org/10.1145/3385412.3385980

work page doi:10.1145/3385412.3385980 2020
[16]

Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975). https://doi.org/10.1145/361227.361234

work page doi:10.1145/361227.361234 1975
[17]

In: PLDI

Lorch, J.R., Chen, Y., Kapritsos, M., Parno, B., Qadeer, S., Sharma, U., Wil- cox, J.R., Zhao, X.: Armada: low-effort verification of high-performance concurrent programs. In: PLDI. pp. 197–210. ACM (2020). https://doi.org/10.1145/3385412. 3385971

work page doi:10.1145/3385412 2020
[18]

In: Advances in Petri Nets

Mazurkiewicz, A.W.: Trace theory. In: Advances in Petri Nets. pp. 279–324. Lecture Notes in Computer Science, Springer (1986). https://doi.org/10.1007/ 3-540-17906-2_30

work page 1986
[19]

Computing101(1), 59–74 (2019)

Mutluergil, S.O., Tasiran, S.: A mechanized refinement proof of the Chase-Lev deque using a proof system. Computing101(1), 59–74 (2019). https://doi.org/10. 1007/S00607-018-0635-4 20 C. Enea, A. Farzan, D. Klumpp A Proofs for Section 4 (Deciding the Soundness Problem) Theorem 4.2. For every synchronization alphabet, the coverability problem over programs ...

work page 2019
[20]

normal actions

As thej-th edge is clearly reachable from thei-th edge, we know thatS1 ≺ S2 or S1 = S2 is non-trivial (due to i < j , it cannot be trivial). Furthermore, by definition, the graph (Σ(G), ↣) has an edge froma to b. Thus, Algorithm 4.4 does not conclude thatF is sound, and instead declares it unsound. Lemma A.2. If Algorithm 4.4 claims thatF is unsound, then...

work page