REVIEW 2 major objections 3 minor 6 references
Value-centric Dynamic Partial Order Reduction
T0 review · 2 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read This paper introduces a coarser trace equivalence, value-happens-before, and shows it can be exponentially coarser than happens-before while remaining efficiently explorable.
desk verdict Value-centric DPOR is a real step forward, but the closure algorithm's correctness for infeasible inputs has a hole that must be patched. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the annotated partial order (APO), a partial order $P$ over the event set $X_1\cup X_2$ (root-thread events $X_1$, leaf-thread events $X_2$) enriched with a value function $\mathrm{val}$, a side function $S$ for root reads, and a good-writes function $\mathrm{GoodW}$ assigning to each read the set of write events a realizing trace may let it observe. Two structural constraints make the machinery work: $\mathrm{width}(P|_{X_1})=1$, so root events are totally ordered, and $\mathrm{Mwidth}(P|_{X_2})=1$, bounding the largest set of pairwise-conflicting leaf events with no order between them. The argument runs through closure: three rules (Rule1, Rule2, Rule3) add orderings that every realizing trace must satisfy; if the closure exists the APO is realizable, and if no closure exists it is not. The witness construction (Lemma 4.1) linearizes the closure by ordering all root events before all leaf events unless the opposite order is already forced, and this is where the paper asserts—without a complete proof—that the resulting order is acyclic. The closure computation gives the polynomial-time per-class bound, and the $\mathrm{VHB}$ class count gives the overall complexity $O(|T^{\max}_H/\mathrm{VHB}|\cdot \mathrm{poly}(n))$.
What would settle it
Construct a closed annotated partial order $(X_1,X_2,P,\mathrm{val},S,\mathrm{GoodW})$ with $\mathrm{width}(P|_{X_1})=1$ and $\mathrm{Mwidth}(P|_{X_2})=1$ for which the order $Q$ defined by $Q=P\cup\{(e_1,e_2): e_1\in X_1, e_2\in X_2, e_2\not<_P e_1\}$ contains a cycle. Such an object would refute Lemma 4.1 and invalidate the witness construction; in its absence, exhaustively checking small random APOs for cyclic $Q$ would either produce such a counterexample or add evidence for the lemma.
Extended reading notes
Core claim
The central claim is that a value-aware equivalence can be both much coarser than happens-before and efficiently explorable. Formally, $\mathrm{VHB}$ identifies traces $t_1,t_2$ when they have the same event set, the same value function $\mathrm{val}_{t_1}=\mathrm{val}_{t_2}$, the same side function $S_{t_1}=S_{t_2}$ on reads of the root thread, the same causal happens-before relation restricted to read events, and the same happens-before relation restricted to leaf-thread events. The paper proves this equivalence is sound for local-state reachability—if two traces are equivalent, both reach the same local states—and that it is at least as coarse as the happens-before partition, with explicit programs where the $\mathrm{HB}$ partition is exponential ($\Omega(4^n/\sqrt{n})$ or $\Omega(2^n)$ classes) while the $\mathrm{VHB}$ partition has only $O(n^2)$ classes. The algorithmic result is that VC-DPOR visits a representative of every $\mathrm{VHB}$ class, spends only polynomial time per class when the thread count is constant, and never visits a second trace from the same class.
Load-bearing premise
The whole method assumes, without proof, that the witness trace for a closed annotated partial order can always be built by putting every root-thread event before every leaf-thread event unless the opposite order is already forced, and that this construction never creates a cycle.
Editorial extensions
If this is right
- For any concurrent program with a constant number of threads, the total verification effort becomes the size of the $\mathrm{VHB}$ partition times a polynomial; whenever $\mathrm{VHB}$ is exponentially coarser than happens-before, the trace-exploration cost drops by the same exponential factor.
- Soundness for local-state properties means assertion violations, races, and local reachability checks can be reported without exploring the remaining traces in a class; global-state properties can be reduced to local ones with a monitor thread.
- The $\mathrm{VHB}$ partition is never larger than the $\mathrm{HB}$ partition, so VC-DPOR never explores more maximal traces than optimal happens-before DPOR, and in the benchmarks it often explores orders of magnitude fewer.
- The closure-based realizability test gives a polynomial-time way to move between classes, so the coarser equivalence does not reintroduce exponential per-class cost, which was the bottleneck of earlier value-centric methods that relied on NP oracles.
Reading between the lines
- The unproven acyclicity step in Lemma 4.1 is the one point where the completeness proof could fail; if it is repaired, the same annotated-partial-order closure framework could support other coarse equivalences, such as ones tracking only the last writer per value or per variable.
- The choice of which thread is the root is arbitrary, so a symmetric or multi-root variant might yield an even coarser equivalence or reduce the per-class overhead; the paper's experiments suggest the asymmetry matters in practice.
- When $\mathrm{VHB}$ gives no reduction (as in a few benchmarks), VC-DPOR is slower than lighter DPOR methods because closure computation is heavy; reducing that overhead, or dynamically switching equivalences, is a natural engineering follow-up.
- Since the side function only distinguishes local versus remote writes for root reads, an extension that partitions by the actual observation value of each read could make the equivalence coarser still, though it would require new closure rules and a new realizability argument.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper introduces a value-sensitive trace equivalence called value-happens-before (VHB), proves that it is at least as coarse as the Mazurkiewicz/happens-before equivalence and can be exponentially coarser, and presents an algorithm VC-DPOR that is claimed to explore exactly one representative per VHB class in time O(|T_max_H/VHB| * poly(n)) for a constant number of threads. The technical machinery consists of annotated partial orders, a notion of closed annotated partial orders, a closure algorithm (Algorithm 1), and a decision procedure Realize for realizability. The paper also reports an implementation in Nidhugg and compares it with Source-DPOR, Optimal-DPOR, Optimal-DPOR with observers, and DC-DPOR on SV-COMP, dynamic-programming, mutual-exclusion, and individual benchmarks.
Significance. If the main theorem were correct, this would be a substantial advance: it would give an explicit value-centric equivalence that is provably coarser than happens-before, is explorable in polynomial time per equivalence class without NP oracles, and is accompanied by a prototype implementation and broad experiments. The exponential-separation examples in Section 3 are clear and the experimental evaluation is extensive, with code available. However, the central realizability theorem (Theorem 4.5) is false as stated, and the closure algorithm can diverge on a realizable input. Because Theorem 5.1 rests directly on Theorem 4.5, the main claims of the paper are not established in the current form.
major comments (2)
- [§4.3, Lemma 4.3 (⇐) and §4.2, Algorithm 1] Lemma 4.3 is false as stated. Let X1 = {r}, X2 = {w1, w2}, let P be the total order w1 <P w2 <P r, and set GoodW(r) = {w2}, val(w1) = 1, val(w2) = val(r) = 2, and S(r) = 2. This annotated partial order is consistent, satisfies width(P|X1) = Mwidth(P|X2) = 1, and is realizable by the trace w1, w2, r, in which r observes w2. However, P is not closed: MinW_P(r) = {w1}, so GoodW(r) ∩ MinW_P(r) is empty, violating Item 1 of the closedness definition. Moreover, no partial order Q with P ⊆ Q (in the paper's refinement notation, Q ⊑ P) can be closed, because any such Q must contain w1 <Q w2 <Q r, so w2 can never become a minimal visible write for r. Thus P is realizable but infeasible, contradicting Lemma 4.3. The same phenomenon makes Algorithm 1 diverge: starting from the variant in which r is unordered with w1 and w2, Rule1(r) inserts w2 → r, but Item 1 remains violated because w1 is still the unique minimal visible write, so Rule1 is called again and re-inserts the already-present ordering w2 → r forever. This falsifies the assertion in Lemma B.1 that every rule application inserts a new ordering, and it invalidates the 'if and only if' in Theorem 4.5 on which Theorem 5.1 depends.
- [§4.2, Lemma B.2 and Algorithms 2–4] Independently of the counterexample above, the correctness proof of Closure is incomplete. Algorithm 1 never checks whether a rule application creates a cycle, and Lemma B.2 does not prove that Q remains a partial order between rule applications or that every infeasible input makes Closure return ⊥. The uniqueness assertions in Rule2 (Algorithm 3, line 3) and Rule3 (Algorithm 4, lines 1–2) are asserted rather than derived; Mwidth(P|X2) = 1 only orders conflicting pairs, so two maximal remote writes for a read need not be comparable. If a cycle is created, VisibleW_Q, MinW_Q, and MaxW_Q become ill-defined, and the polynomial bound of Lemma B.1 and the invariant argument of Lemma B.2 no longer apply. This is a second load-bearing gap in the proof of Theorem 4.5.
minor comments (3)
- [§4.1, Lemma 4.1] The sentence 'It is easy to see that since width(P|X1) = 1, Q is indeed a partial order' should be expanded into a real proof; the acyclicity argument is not immediate and is load-bearing for the witness construction.
- [§3] The text contains an unresolved cross-reference: 'We also refer to ?? for a comparison of VHB and our algorithm VC-DPOR' should name the specific appendix or table.
- [§6] The experimental tables report single runs without variance or confidence information; this is acceptable given the large differences in most benchmarks, but the cases where VC-DPOR is slower (e.g., X2Tv9 in Table 3) would benefit from a brief discussion of implementation overhead versus partitioning size.
Circularity Check
No circular derivation found: VC-DPOR and VHB are derived from explicit definitions and proved against independent baselines, with no fitted input renamed as prediction.
full rationale
The paper's central results are self-contained derivations from its own definitions. VHB soundness and coarseness relative to HB are proved directly (Theorem 3.1, Appendix A), and the equivalence is not defined as 'the classes explored by VC-DPOR'; rather, the algorithm's completeness and pairwise-distinct class visits are argued via Lemmas C.1-C.4. Closure uniqueness and realizability (Lemmas 4.1-4.3, 4.4) are proved in the appendix with explicit constructions, not imported from prior work by the same authors. The only self-overlap is citation of the authors' DC-DPOR as a comparison baseline in the experiments and related work, which is not load-bearing for any theorem. No parameter is fitted to data and then reported as a prediction; the experiments report trace counts and timings against external implementations (Nidhugg Source/Optimal, optimal with observers) and public SV-COMP benchmarks. The manuscript does contain a genuine proof gap that is not circular: the acyclicity of the strengthened partial order Q in Lemma 4.1 and the invariant of Lemma B.2 are asserted ('It is easy to see that since width(P|X1)=1, Q is indeed a partial order') without a complete argument that Closure's rule applications can never create a cycle before detecting infeasibility. That is a correctness risk in Theorem 4.5, and hence in Theorem 5.1, but it is not a reduction of the conclusion to the hypotheses. Accordingly, the circularity score is 0.
Assumptions & free parameters
assumptions (6)
- domain assumption The program has a fixed, constant number of threads, no dynamic thread creation, and a sequentially consistent memory model.
- domain assumption The state space is acyclic (bounded model checking), so every trace is finite and maximal traces exist.
- domain assumption Each thread is deterministic, so local states are determined by the sequence of values read and written.
- domain assumption Events are identified by thread id and program index, requiring the program control flow to be unrolled into a tree.
- ad hoc to paper For a consistent annotated partial order, each thread's projected events form a valid local trace when forced to read/write the annotated values.
- standard math The Mazurkiewicz/happens-before equivalence and its optimal exploration (Source/optimal DPOR, Abdulla et al. 2014) are correct external baselines.
Cite this review
Pith. "Pith review of Value-centric Dynamic Partial Order Reduction." pith.science (2026). https://pith.science/paper/YJAGG7BC
@misc{pith2026190900989,
author = {Pith},
title = {Pith review of: Value-centric Dynamic Partial Order Reduction},
year = {2026},
howpublished = {\url{https://pith.science/paper/YJAGG7BC}},
note = {Machine review of arXiv:1909.00989}
}
read the original abstract
The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.
Figures
Figures from the paper (5 more)
Reference graph
Works this paper leans on
-
[1]
=E(t′ 2), and observe that t′ 1∼VHB t′
-
[2]
Since we have constantly many threads, it follows that given a maximal tracet, there exist O(poly(n)) different sets X⊆E( t) for which there exists a tracet′ such that (i)E(t′) = X and (ii)t is a maximal extension oft′. It follows that|TH/VHB| = O |T max H /VHB|· poly(n) , and thus it suffices to argue that VC-DPOR runs in time O(|TH/VHB|· poly(n)). By Le...
work page 2018
-
[3]
Reduction in the number of annotated partial orders returned by Extend. In our presentation of Extend(P, X′, val′, S′, GoodW′), given X′\ X ={e} such that e belongs to a leaf thread, we consider all possible orderings of e with conflicting events from all leaf threads. However, in our implementation, we relax this in two ways. Given a write eventew , we s...
work page 2018
-
[4]
Choosing the order of reads to extend the annotated partial order. In VC-DPOR Algorithm 5, given an extensionQ, we first call ExtendRoot, and then for each leaf thread we call its corresponding ExtendLeaf. However, the order in which we callExtendRoot and different ExtendLeaf can have an effect on the shape of the induced recursion tree. In our experiment...
-
[5]
Extensions yielding maximal traces. Consider a call of VC-DPOR Algorithm 5 on a node u of the induced recursion tree, In this call, an annotated partial orderQ will be (attempted to) be extended with a read event r to observe a valuev. If this extension is successful and results in a maximal trace, we do not attempt to extend annotated partial orders that...
-
[2015]
Stateless Model Checking for TSO and PSO. In TACAS. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2017. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. J. ACM 64, 4 (2017), 25:1–25:49. https://doi.org/10.1145/3073408 Elvira Albert, Puri Arenas, María García de la Banda, Miguel Gómez-Zamalloa, and Pete...
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.