{"id":"05767393-7340-481c-8aae-de4015b250b6","arxiv_id":"2411.16921","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Stateful partial-order reduction with blocking cannot be approximated within polynomial factors unless P=NP, and a new 'includes first set' heuristic outperforms persistent sets in experiments.","lead":"This paper studies partial-order reduction for concurrent systems with locks and other blocking operations, offering a new algorithm and a hardness result. It proves that no efficient algorithm can build a near-minimal reduced model unless P=NP, and its heuristic implementation outperforms standard persistent-set methods on several benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 26's lower bound relies on an unjustified step in Lemma 29: distinct global states reached after different satisfying valuations are asserted to force distinct states in any sound and complete reduced transition system, but Definition 5 allows arbitrary state merging.","rationale":"The central claim is Theorem 26, and its proof hinges on Lemma 29: the lower bound needs the number of states in any sound and complete reduced transition system for P_φ to be at least the number of satisfying valuations of φ. The proof currently only shows that the global states s1, s2 reached after e on different valuation runs are distinct; it then jumps to 'any sound and complete transition system must have at least as many states.' Because Definition 5 allows arbitrary abstract states, the jump is invalid without an extra argument that merging s1 and s2 would sacrifice soundness or completeness. This is exactly the reader's weakest assumption. The proposed brute-force test on a 2-valuation formula would either falsify the lemma or provide evidence that the missing intersection condition is the right repair. The other issues (Lemma 17(i) contradiction, absent code/data) are real but do not affect the lower bound as directly. If the authors supply the missing argument, the theorem likely survives; hence the reader's CONDITIONAL verdict is appropriate and my read does not move it.","tokens_in":28177,"tokens_out":6971,"duration_ms":65509,"concrete_test":"For the smallest satisfiable formula with two satisfying valuations, e.g. φ = (x1∨x2) ∧ (¬x1∨¬x2), construct Pφ as in §8 and brute-force search over all reduced transition systems with at most 2 states (directly using Definition 5) for a sound and complete system whose state count is 1 after the e-transition. If such a system exists, Lemma 29 is false; if the minimum is 2, the state-counting step survives this instance and the missing intersection argument is the likely correct repair.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of Lemma 29 claims that because the global states s1 and s2 reached after e on runs wv1 and wv2 are distinct for distinct satisfying valuations v1 and v2, every sound and complete reduced transition system must have at least as many states as satisfying valuations. This step is not justified by Definition 5: a reduced transition system is only required to preserve full runs up to trace equivalence (soundness and completeness), and its states are arbitrary abstract states, not necessarily global states of TS(P). It is in principle allowed to merge s1 and s2 into one abstract state, provided the outgoing transitions of that state are enabled in every global state that maps to it (the intersection condition). The proof neither states nor proves that such a merge is impossible for the runs wv1 and wv2, e.g. that no action enabled in the intersection can lead to a trace-equivalent representative of the remaining suffix. Since Lemma 29 underpins Corollary 30 and hence the exponential-state lower bound in Theorem 26, the main inapproximability result currently rests on an unproven state-distinguishability assumption. The fix is to show that two different valuations force non-trace-equivalent maximal continuations, so no single abstract state can represent both without violating soundness or completeness.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a stateful partial-order reduction framework for client/server systems with blocking, centered on an \"includes first set\" (IFS) oracle. It presents an idealized lex-first exploration algorithm with sleep sets and an IFS oracle (Listings 1 and 2), proves NP-hardness of the IFS test, and states a strong lower bound (Theorem 26) claiming that no polynomial-time algorithm can construct a reduced transition system whose size is polynomially close to the minimum unless P=NP. It then introduces one-sided heuristics PIFS and rPIFS, a closure-based covering source set construction, and a practical algorithm (Listing 6), with an implementation and experiments on several benchmarks.","tokens_in":28359,"tokens_out":23538,"duration_ms":235635,"significance":"If the lower bound can be made rigorous, it would be the first inapproximability result for stateful partial-order reduction in the presence of blocking, and the IFS/PIFS viewpoint is a genuinely useful conceptual reframing of the \"when to stop exploring\" question. The constructive side is promising: the PIFS characterization (Lemma 32), the closure construction (Lemma 37), and the experimental validation against independently computed complete transition systems via Proposition 7 are concrete strengths. The paper does not ship machine-checked proofs or code, but the completeness checks on random and literature models give useful evidence for the implementation. However, two load-bearing technical points -- the state-counting step in Lemma 29 and the internal contradiction around Lemma 17(i) -- need to be resolved before the main claims can be accepted.","major_comments":[{"comment":"The proof of Lemma 29 infers that, because the global states s1 and s2 reached after e on w_v1 and w_v2 are distinct for distinct satisfying valuations, every sound and complete reduced transition system for P_phi must have at least as many states as satisfying valuations. This inference is not licensed by Definition 5, which only requires every full run of TSr to be a full run of TS and does not require the states of TSr to be states of TS(P). A small acyclic action-deterministic transition system can contain exponentially many full runs (for example, a chain q0 -> q1 -> ... -> qm with two differently labeled transitions at each level), so distinct global states may be merged in TSr. Since Corollary 30 and Theorem 26 rely on this state-counting step, the main inapproximability result is not established as written. The authors should either provide a genuine lower bound on the number of states needed by any TSr whose full-run language contains all runs w_v while remaining a subset of the full runs of TS(P), or explicitly restrict Definition 5 and Definition 25 to reduced transition systems whose states are states of TS(P) (or nodes of the exploration graph) and restate the theorem for that setting.","section":"§8, Lemma 29 and Definition 5"},{"comment":"Lemma 17(i) states that every full run in the graph built by Listing 2 is a full lex-run of TS(P), but the paragraph immediately before the lemma says that edges added by the subsumption rule may create paths that are not lex-runs. The proof of (i) is only \"direct from the algorithm,\" which is inconsistent with the preceding remark. This matters because the correctness argument for Listing 6 in §10.3 invokes Lemma 17 as the correctness statement for Listing 2. Please remove or repair (i), prove the soundness and completeness parts separately, and prove the lex-usefulness of states without relying on (i).","section":"§6, Lemma 17"}],"minor_comments":[{"comment":"The comment on line 6 of both listings, \"Sl = sleep(n) union {labels of transitions outgoing from n},\" is misleading; it should say \"labels of transitions already explored from n,\" since Sl is built incrementally in the while loop.","section":"§6, Listings 1 and 2"},{"comment":"The claim that Listing 1 remains optimal when line 9 chooses actions arbitrarily rather than in the fixed linear order is plausible but not proved; the proof of Lemma 15 uses the fixed order in an essential way, so a separate argument should be supplied if the remark is retained.","section":"§6, Remark 21"},{"comment":"The two client processes for each variable are hard to distinguish in Figure 7, and the text \"Similarly, for client Ci but now we have theta_i, lambda_i, and x_i actions\" is difficult to parse; please clarify the notation and the figure labels.","section":"§8, Figure 7"},{"comment":"Several rows of Table 1 are difficult to read in the current formatting, with missing or misplaced entries (for example, the fs rows); please reformat the table so that each column is clearly aligned.","section":"§11, Table 1"},{"comment":"The sentence \"Even if we verified the abstract algorithm from Listing 6 in Coq, that we are not capable of\" is confusing and could be misread as claiming a Coq verification was performed; rephrase to state clearly that no such formal verification was done.","section":"§11, implementation paragraph"},{"comment":"References [3] and [15] are incomplete (missing publication venue/year), and reference [32] lacks the journal name; please complete the bibliographic data.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The main risk is the lower bound. If Lemma 29 cannot be proved under the current Definition 5, the authors should restrict the theorem to the standard subgraph notion of reduced transition system; without such a repair, the headline negative result is unsupported. The constructive algorithm and experimental evaluation are potentially solid, but the paper's novelty depends heavily on Theorem 26, so the revision should address the state-counting gap directly and not merely add a caveat."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I read the Herbreteau et al. paper. My take: the IFS/PIFS/rPIFS framework is a real conceptual contribution, but the marquee inapproximability theorem is not proven as written. Two concrete problems stand out.\n\nFirst, Lemma 17(i) says every full run in the graph built by Listing 2 is a lex-run, and the paragraph immediately above says the opposite: subsumption edges can create paths that are not lex-runs. The proof hand-waves this as 'direct from the algorithm,' which does not resolve the contradiction. This is probably fixable by weakening the lemma to soundness and completeness, but as stated it is simply wrong.\n\nSecond, and more serious, Lemma 29. The proof asserts that because the global states reached after e on runs for distinct satisfying valuations are distinct, any sound and complete reduced transition system must have at least that many states. Definition 5 does not require reduced TS states to be global states, nor does it forbid merging. To rule out a merge you need to show that the outgoing transitions from a merged state would have to be enabled in both concrete states, and that no single abstract state can represent both without losing trace equivalence for some maximal continuation. That argument is absent. Since Lemma 29 feeds Corollary 30 and then Theorem 26, the main lower bound has a hole. I suspect the result is true, but the proof needs real work.\n\nWhat is genuinely new and good: the IFS oracle cleanly separates 'which action to take' from 'when to stop,' and recasting persistent sets, sleep sets, and race reversal as heuristics for one decision problem is useful. The PIFS/rPIFS heuristics and the rPIFS-based closure operation go beyond standard stubborn/persistent sets, and the experiments show large gains on several public benchmarks. The independent completeness check using Proposition 7 is good practice; no code or data are shipped, but the validation method is honest.\n\nOverall: this deserves a serious referee, but not in current form. My recommendation is to engage with it, ask the authors to fix Lemma 17 and supply the missing state-distinguishability argument for Lemma 29, and then reassess. If you work on partial-order reduction, the IFS material is worth citing and worth discussing in a reading group.","headline":"A genuinely useful reformulation of stateful POR with a plausible but currently unproven lower bound; Lemma 29 needs a missing argument and Lemma 17 needs a correction.","tokens_in":28961,"tokens_out":5768,"would_cite":true,"duration_ms":57193,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68Q85","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that stateful partial-order reduction cannot be approximated within any polynomial factor unless P=NP, and it backs the claim with a 3-SAT reduction plus a practical heuristic algorithm.","keywords":["stateful partial-order reduction","Mazurkiewicz traces","sleep sets","covering source sets","IFS oracle","NP-hardness","model checking","concurrent systems"],"falsifier":"Run the Section 8 construction on a 3-CNF formula with exponentially many satisfying assignments: if any algorithm, in polynomial time, outputs a sound and complete reduced transition system for the resulting client/server system with fewer states than the number of satisfying valuations, then Theorem 26 is refuted.","tokens_in":27939,"feed_emoji":"🔀","tokens_out":6358,"duration_ms":55913,"temperature":0.7,"pith_summary":"This paper tackles stateful partial-order reduction, where the goal is to build a reduced transition system containing one representative run from each equivalence class of a concurrent system's runs. Its central result is negative: assuming P is not equal to NP, no algorithm can construct a sound and complete reduced transition system whose size is bounded by any polynomial in the size of the smallest possible such system while running in polynomial time in input plus output. The positive contribution is to isolate a simple oracle, IFS, which asks whether exploration from a state is already covered, and to show that this oracle is NP-hard. The paper then develops polynomial-time heuristic approximations of IFS, packaged into a sound and complete reduction algorithm that uses sleep sets and covering source sets, and reports experiments where it outperforms persistent-set-based reduction by orders of magnitude.","feed_headline":"Stateful partial-order reduction can't be near-optimal unless P=NP","feed_subtitle":"A proof rules out polynomial-time construction of state graphs within any polynomial factor of the minimum.","key_machinery":"The central objects are first sets and covering source sets. For a por-equivalence on runs, first(u) is the set of actions that can start a run equivalent to u, and a covering source set in a state intersects the first set of every maximal run from that state; following only actions in covering source sets preserves all equivalence classes. The IFS oracle asks whether a given set B includes the first set of some maximal run from state s. Sleep sets record which actions need not be explored because equivalent runs were already seen, and lexicographic ordering selects representative runs. The heuristic PIFS replaces the global run-existence question by local runs of individual processes and a sticking closure between actions, while closure(s,b) builds a covering source set from a chosen action. The carrying mechanism is the pattern of Lemma 32, a staircase of actions whose domains successively wrap all enabled actions, which characterizes exactly when IFS holds.","core_discovery":"The paper's main claim is Theorem 26: if P is not equal to NP, then no excellent partial-order reduction algorithm exists, meaning no algorithm that, in time polynomial in the size of the input system plus the minimal reduced transition system, outputs a sound and complete reduced transition system of size at most polynomial in that minimum. In other words, the smallest sound and complete reduced state graph cannot be efficiently approximated within any polynomial factor. The paper also proves that the IFS oracle, which asks whether a given set of actions contains the first set of some maximal run from a state, is NP-complete. In response to these hardness results, it proposes an idealized trace-optimal algorithm based on lexicographic order and sleep sets, and then a practical algorithm replacing IFS with the PIFS and rPIFS heuristics, with a proof that the resulting reduced transition system is sound and complete.","pith_inferences":["The lower bound likely extends to stateless partial-order reduction in the presence of blocking, since the proof does not rely on stored states; if so, the recent trace-optimal polynomial-memory stateless algorithms for non-blocking systems cannot be adapted to locks without losing polynomial-time near-optimality.","The IFS heuristic framework suggests a concrete research line: approximate IFS with SAT solvers or with k-Cartesian abstractions, both of which the paper mentions as possibilities but does not evaluate.","Combining race-reversal heuristics with PIFS is a natural next step, since the paper shows race reversal is another approximation of IFS but leaves its integration with the new algorithm open.","The implementation claims rest on an empirical completeness check rather than a machine-checked proof of the code, so a formally verified implementation of Listing 6 would be a natural follow-up."],"forward_implications":["Any future stateful partial-order method aimed at guaranteed near-optimal reduced graphs must overcome the P versus NP barrier, so heuristic or approximate methods are the only viable route.","The IFS viewpoint reframes partial-order reduction from deciding which actions to explore into deciding when to stop; any correct heuristic must answer 'yes' whenever IFS holds, giving a one-sided error condition.","For non-blocking read/write systems without synchronization primitives, the IFS test becomes linear-time, yielding a simple trace-optimal stateless exploration algorithm for that class.","The closure-based covering source sets are always covering and are no larger than the persistent sets used as the baseline, which explains the reported gains of the new algorithm across the benchmark models.","Because the lower-bound construction uses only binary synchronizations with blocking, the inapproximability transfers to any model that can encode this client/server pattern."],"supporting_citations":[{"why":"Introduces trace-optimality and source sets, the foundation for the optimality notion the paper builds on.","marker":"[1]"},{"why":"Supplies sleep sets and persistent sets, the two classical mechanisms the algorithms combine.","marker":"[15]"},{"why":"Defines Mazurkiewicz trace equivalence, the por-equivalence relation used throughout the paper.","marker":"[29]"},{"why":"Starts stateless dynamic partial-order reduction and provides two benchmark models, filesystem and lastzero.","marker":"[14]"},{"why":"Contributes the quasi-optimal partial-order reduction hardness result and benchmark models disp, mpat, and qo used for comparison.","marker":"[9]"},{"why":"Shows a truly stateless trace-optimal algorithm with polynomial memory, the main reference point for the stateless/stateful contrast.","marker":"[24]"},{"why":"Gives the persistent-set computation called p-closure that serves as the baseline algorithm in the experiments.","marker":"[12]"},{"why":"Uses lexicographic ordering to select representative runs, an ingredient of the idealized IFS-based algorithm.","marker":"[21]"}],"fun_headline_variants":["Near-optimal stateful reduction impossible unless P=NP","P≠NP blocks near-optimal stateful partial-order reduction","Hardness proof: no polynomial near-optimal stateful reduction","NP-hard optimality spurs practical heuristics for stateful reduction","Beyond stubborn sets: practical stateful reduction heuristics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The lower-bound argument relies on treating a state in a reduced transition system as a genuine global state: if several histories reach the same node, any outgoing transition must be executable after every one of those histories, and merging states cannot create transitions that are valid for only some of them.","fun_headline_variants_meta":{"raw":{"variants":["Near-optimal stateful reduction impossible unless P=NP","P≠NP blocks near-optimal stateful partial-order reduction","Hardness proof: no polynomial near-optimal stateful reduction","NP-hard optimality spurs practical heuristics for stateful reduction","Beyond stubborn sets: practical stateful reduction heuristics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001292,"raw_usage":{"total_tokens":5254,"prompt_tokens":902,"completion_tokens":4352,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":518,"completion_tokens_details":{"reasoning_tokens":4268}},"tokens_in":518,"tokens_out":4352,"duration_ms":29048,"temperature":1.0,"reasoning_tokens":4268,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T12:53:15.100582+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the Section 8 construction on a 3-CNF formula with exponentially many satisfying assignments: if any algorithm, in polynomial time, outputs a sound and complete reduced transition system for the resulting client/server system with fewer states than the number of satisfying valuations, then Theorem 26 is refuted.","supporting_citations":[{"cited_title":"Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction","cited_arxiv_id":null,"evidence_quote":"Introduces trace-optimality and source sets, the foundation for the optimality notion the paper builds on."},{"cited_title":"Partial-Order Methods for the Verification of Concurrent Systems An Approach to the State-Explosion Problem","cited_arxiv_id":null,"evidence_quote":"Supplies sleep sets and persistent sets, the two classical mechanisms the algorithms combine."},{"cited_title":"Mazurkiewicz","cited_arxiv_id":null,"evidence_quote":"Defines Mazurkiewicz trace equivalence, the por-equivalence relation used throughout the paper."},{"cited_title":"Dynamic Partial-Order Reduction for Model Checking Software","cited_arxiv_id":null,"evidence_quote":"Starts stateless dynamic partial-order reduction and provides two benchmark models, filesystem and lastzero."},{"cited_title":"Quasi-optimal partial order reduction","cited_arxiv_id":null,"evidence_quote":"Contributes the quasi-optimal partial-order reduction hardness result and benchmark models disp, mpat, and qo used for comparison."},{"cited_title":"Truly stateless, optimal dynamic partial order reduction","cited_arxiv_id":null,"evidence_quote":"Shows a truly stateless trace-optimal algorithm with polynomial memory, the main reference point for the stateless/stateful contrast."},{"cited_title":"Sound sequentialization for concurrent program verification","cited_arxiv_id":null,"evidence_quote":"Gives the persistent-set computation called p-closure that serves as the baseline algorithm in the experiments."},{"cited_title":"Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique","cited_arxiv_id":null,"evidence_quote":"Uses lexicographic ordering to select representative runs, an ingredient of the idealized IFS-based algorithm."}],"review_version":1}