{"id":"0b2b91b4-2bc8-4389-95db-0d93b257f925","arxiv_id":"1909.00989","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper defines the value-happens-before trace equivalence, proves it is coarser than happens-before (exponentially so in some programs), and presents the VC-DPOR algorithm that explores its classes in polynomial time per class for a bounded number of threads.","lead":"This paper introduces value-happens-before, a new way to group concurrent program executions so that more executions are treated as equivalent based on the data values they read and write. It then gives an algorithm, VC-DPOR, that explores this coarser grouping efficiently, which can speed up automated verification of concurrent software.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Closure lacks an acyclicity check; rejection of infeasible annotated partial orders is unproven, threatening Theorem 4.5 and hence Theorem 5.1.","rationale":"The paper's strongest claim is that VC-DPOR solves local-state reachability in time O(|T_max_H/VHB| * poly(n)), exploring one representative per value-happens-before class. That claim rests on the realizability machinery of Section 4: Extend and the main algorithm use Closure to decide whether annotated partial orders are realizable and to construct witnesses. The Reader's verdict flagged Lemma 4.1's acyclicity step as the weakest assumption, but on inspection that step is actually justified: in the constructed Q, every edge from a root event to a leaf event either comes from P or is added only when the leaf is not already below that root, so a cycle would force a strictly increasing sequence in the fixed total order of the root thread, which is impossible. The more serious gap is in the Closure procedure itself: the proof does not establish that infeasible inputs are always detected by termination with ⊥, and the algorithm never checks that strengthening Q preserves acyclicity. If Closure can return a cyclic 'closed' Q, then Realize cannot linearize it and the entire exploration breaks; if Closure fails to terminate on some infeasible input, the polynomial bound fails. This is a proof gap rather than a demonstrated counterexample, and the concrete brute-force test above would settle whether it is a real defect or merely a missing lemma. The verdict should remain CONDITIONAL: the paper's ideas and experiments are valuable, but this realizability gap should be closed before the central theorem is accepted as proven, and the Reader's own concern should be redirected from Lemma 4.1 to Closure's infeasible-input handling.","tokens_in":41444,"tokens_out":32366,"duration_ms":354900,"concrete_test":"Enumerate all annotated partial orders with up to 3 root events and 3 leaf events over 1–2 variables with small value domains. For each instance, compare Closure's output against a brute-force exhaustive search over all permutations of events that checks realizability (existence of a linearization in which every read observes a good write and the per-thread local traces are consistent). Verify three properties: (i) Closure always terminates; (ii) if Closure returns Q≠⊥, then Q is acyclic and the witness produced by Lemma 4.1 is a valid trace; (iii) Closure returns ⊥ exactly when brute force finds no linearization. If any infeasible instance yields a non-⊥ result or a cyclic Q, the realizability decision procedure is broken and Theorem 5.1 needs rework; if none does, the missing acyclicity invariant should be added to Lemma B.2 and the termination proof for infeasible inputs completed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim depends on Theorem 4.5, which says realizability of annotated partial orders is decidable in O(poly(n)) time. This theorem relies on Closure (Algorithm 1) either returning the unique closure or returning ⊥. Lemma B.2 proves (1) if Closure returns Q≠⊥ then Q is the closure, and (2) if it returns ⊥ then P is infeasible. It does not prove the converse needed for Theorem 4.5, namely that every infeasible input makes Closure terminate with ⊥, nor that Q remains a partial order throughout the computation. The pseudocode has no acyclicity check: each Rule1/2/3 call inserts an ordering into Q, and if that insertion creates a cycle, Q ceases to be a partial order, the predicates MinW, MaxW, and VisibleW become ill-defined, and Lemma 4.1's witness construction (which requires linearizing Q) is no longer applicable. Lemma B.1's polynomial bound assumes each rule application inserts a new ordering, but it does not rule out the possibility that a cycle is produced before a rule finds its required unique minimal/maximal witness, causing Closure to return a cyclic 'closed' structure or to fail to detect infeasibility. This is a different point from the Reader's flagged step: the acyclicity claim in Lemma 4.1's step 1 is actually defensible, since in Q any root→leaf→root transition strictly increases the fixed total order of the root thread (width(P|X1)=1), so no cycle can arise there. The vulnerable spot is Closure's handling of infeasible instances, not the witness construction for already-closed P.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":41787,"tokens_out":21231,"duration_ms":234227,"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":[{"comment":"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.","section":"§4.3, Lemma 4.3 (⇐) and §4.2, Algorithm 1"},{"comment":"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.","section":"§4.2, Lemma B.2 and Algorithms 2–4"}],"minor_comments":[{"comment":"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.","section":"§4.1, Lemma 4.1"},{"comment":"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.","section":"§3"},{"comment":"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.","section":"§6"}],"recommendation":"reject","confidential_remarks":"The counterexample in my report appears to be a genuine counterexample to Lemma 4.3 and also shows non-termination of Algorithm 1 on a realizable annotated partial order. This is not a mere proof gap: the central theorem of Section 4 is false as stated, and Theorem 5.1 inherits the problem. If the authors can repair the closure definition and the realizability decision procedure, a resubmission could be considered; in the current form the main results are not established."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version: this is the paper that gives value-aware DPOR a polynomial per-class exploration for a constant number of threads, and it backs it with real experiments. It deserves a serious referee. But the proof of the central algorithmic claim has a hole that needs to be closed before I'd take the theorem on faith.\n\nThe new thing is the value-happens-before (VHB) equivalence. It's always at least as coarse as Mazurkiewicz/HB, can be exponentially coarser, and is sound for local-state reachability. Previous value-centric methods (Huang's MCR) used NP-hard oracles; the explicit coarser equivalences (DC-DPOR, observers) ignore values. So VC-DPOR is the first explicit, value-sensitive DPOR with a polynomial per-class bound. That's a genuine advance. The appendix has real proofs, the prototype is a Nidhugg fork, and the benchmark comparison against Source, Optimal, Optimal*, and DC-DPOR is broad and honest, including cases where VC-DPOR is slower.\n\nThe soft spot is in the Closure algorithm. As printed, Algorithm 1 never returns ⊥: Rule1 can return ⊥ when the good-writes set is empty, but Closure calls Rule1 and ignores the result, so the algorithm always returns whatever Q it ends with. Lemma B.2 then discusses 'if Closure returns ⊥' — a case the pseudocode can't reach. Even if you patched that, there is no acyclicity check: the rules insert orderings, and nothing stops e1→e2 and later e2→e1, at which point Q is no longer a partial order and the minimal/maximal/visible-write sets become ill-defined. The paper says closure may fail due to cycles, but doesn't prove every infeasible input makes the algorithm stop. This threatens Theorem 4.5 and hence Theorem 5.1. It is likely fixable — return ⊥ on a rule failure and on any cycle, and argue cycles imply infeasibility — but as written it is load-bearing. The reader's concern about Lemma 4.1's step 1 is, I think, a red herring: root→leaf→root transitions strictly increase the root thread's total order, so no cycle can arise in that construction. The Closure issue is the real one.\n\nMinor things: experiments have no error bars and don't include MCR/SATCheck, and the dynamic-thread extension is asserted rather than proven. Those are secondary.\n\nBottom line: this is a paper for the DPOR/verification crowd, and it should go to peer review. The core idea is important and the gap looks patchable, but I'd want the closure correctness proof fixed before accepting.","headline":"Value-centric DPOR is a real step forward, but the closure algorithm's correctness for infeasible inputs has a hole that must be patched.","tokens_in":42309,"tokens_out":5841,"would_cite":true,"duration_ms":57306,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper introduces a coarser trace equivalence, value-happens-before, and shows it can be exponentially coarser than happens-before while remaining efficiently explorable.","keywords":["stateless model checking","dynamic partial order reduction","value-happens-before equivalence","concurrency verification","trace equivalence","local-state reachability","annotated partial orders"],"falsifier":"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.","tokens_in":41235,"feed_emoji":"🔄","tokens_out":11900,"duration_ms":99985,"temperature":0.7,"pith_summary":"This paper tries to establish that verifying concurrent programs by exploring interleavings can be made drastically cheaper if the trace space is partitioned according to the values that variables carry, not only by the order of conflicting operations. It introduces the value-happens-before equivalence ($\\mathrm{VHB}$): two traces are equivalent when they contain the same events, assign the same values to every event, agree on a side function that records for each read of a distinguished root thread whether it observed a local or remote write, agree on the causal happens-before relation restricted to reads, and agree on the happens-before relation among the remaining leaf threads. The paper proves that $\\mathrm{VHB}$ is always at least as coarse as the standard happens-before (Mazurkiewicz) equivalence, is sometimes exponentially coarser, and is sound for checking local-state properties such as assertion violations. Its algorithm VC-DPOR explores the $\\mathrm{VHB}$ partitioning in $O(|T^{\\max}_H/\\mathrm{VHB}|\\cdot \\mathrm{poly}(n))$ time for a constant number of threads, promising exponential savings in trace count without the NP-oracle bottleneck of earlier value-centric methods. Benchmarks on standard concurrency programs show that the coarser partitioning typically reduces both the number of maximal traces explored and the running time.","feed_headline":"Trace equivalence can make concurrency checking exponentially faster","feed_subtitle":"By grouping traces that read and write the same values, model checking can skip huge numbers of equivalent executions.","key_machinery":"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))$.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines trace theory and the happens-before equivalence that VHB is compared against and shown to coarsen.","marker":"[Mazurkiewicz 1987]"},{"why":"Introduces dynamic partial order reduction, the setting that VC-DPOR extends with a coarser value-aware equivalence.","marker":"[Flanagan and Godefroid 2005]"},{"why":"Provides the optimal DPOR and source-set machinery; the baseline that explores exactly one trace per happens-before class and is used as comparison.","marker":"[Abdulla et al. 2014]"},{"why":"Introduces data-centric DPOR, a coarser-than-HB explicit equivalence; VHB is positioned against it and compared experimentally.","marker":"[Chalupa et al. 2017]"},{"why":"Gives optimal DPOR with observers, another coarser equivalence; key experimental baseline.","marker":"[Aronis et al. 2018]"},{"why":"Maximal causality reduction is the prior value-centric approach that relies on NP oracles; the challenge that VHB removes.","marker":"[Huang 2015]"}],"fun_headline_variants":["Value-aware equivalence speeds up concurrency checking exponentially","New trace equivalence cuts concurrency checking time dramatically","Value-happens-before: exponential gains in stateless model checking","Smarter trace grouping makes concurrency verification exponentially faster"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Value-aware equivalence speeds up concurrency checking exponentially","New trace equivalence cuts concurrency checking time dramatically","Value-happens-before: exponential gains in stateless model checking","Smarter trace grouping makes concurrency verification exponentially faster"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000682,"raw_usage":{"total_tokens":3163,"prompt_tokens":1077,"completion_tokens":2086,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":693,"completion_tokens_details":{"reasoning_tokens":2021}},"tokens_in":693,"tokens_out":2086,"duration_ms":257103,"temperature":1.0,"reasoning_tokens":2021,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:30:47.898112+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}