{"id":"e79a9985-8f55-4db0-a3a6-e3463e3a193f","arxiv_id":"2411.16612","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper introduces a ghost-variable witness format for concurrent programs and claims witness validity coincides under interleaving and thread-modular semantics, with an evaluation where a model checker confirmed most Goblint-generated witnesses.","lead":"This paper proposes a format for correctness witnesses of concurrent programs that uses ghost variables, so a proof produced by one verifier can be checked by a verifier using a different concurrency semantics. It reports that a model checker confirmed most ghost witnesses generated by an abstract interpreter on SV-COMP benchmarks, though the central equivalence proof is incomplete.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem C.2, the unproved converse of the split encoding, is load-bearing: Theorem 5's claim that interleaving validity implies local-trace validity collapses if this direction fails.","rationale":"The reader's weakest_assumption identifies exactly the load-bearing gap: Theorem C.2 is stated without proof, and the proof of Theorem 5 requires that exact direction. My reading of the appendix confirms the omission: Corollary 3, which would also supply the needed direction, is unproved, and the prose around it claims the opposite implication. Since Theorem 5 is the paper's central theoretical contribution, the absence of a proof for one of its two implications means the main claim is not currently supported. No formal verification is claimed, and the empirical results, while suggestive and valuable, only cover the specific Goblint/GemCutter tool pair and do not establish the general equivalence. The reader's REJECT verdict is therefore justified; no change to that verdict is needed. I would add that the concern is about the argument, not about the authors' integrity: the paper itself flags the missing proof, which is honest but does not fill the gap.","tokens_in":29827,"tokens_out":8483,"duration_ms":86634,"concrete_test":"Build an exhaustive small-model check: enumerate all LangAtomic programs up to, say, 3 thread templates, 2 mutexes, 2 globals, and 4 nodes per template; for each, compute exact interleaving safety of P and of split P by brute-force state-space exploration. If any pair differs in safety, Theorem C.2 is refuted; if all agree, the theorem is supported but still unproved. Separately, attempt a formal proof of Theorem C.2 in Isabelle/HOL or Coq from the stated definitions; a successful formalization would close the gap, while a failed attempt would pinpoint a missing hypothesis or reveal a counterexample.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 5 asserts that ghost-witness validity coincides under interleaving and local-trace semantics. Its proof reduces to Theorem 4, which states that a program P is safe iff its atomic-block encoding split P is safe. The direction 'split P safe implies P safe' — equivalently, every violation of split P yields a violation of P — is Theorem C.2, whose proof in Appendix C.1 is literally 'Without proof.' This is not a cosmetic omission: without this direction, an interleaving-valid witness (P^W safe) could still yield an unsafe split P^W, so a thread-modular validator using Definition 7 could reject a witness that is valid under interleaving semantics. The surrounding appendix text weakens rather than supports the point: Corollary 3 states the needed converse but is unproved, and the paragraph following it asserts the opposite direction. The empirical confirmation rates from Table 1 do not cover this theoretical gap; they only show that the two implemented tools agreed on the tested subset. Thus, the central 'coincides' claim is not yet established as a theorem.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a witness format for correctness witnesses of concurrent programs, using ghost variables and ghost updates to encode a tool's reasoning into an instrumented program. The central theoretical claim is Theorem 5, which states that the validity of a ghost witness with respect to the interleaving semantics coincides with its validity with respect to the local trace (thread-modular) semantics. The paper also defines a YAML-based concrete format, shows how thread-modular invariants from Goblint can be expressed as ghost witnesses, and reports an evaluation in which witnesses generated by Goblint are validated by the model checker Ultimate GemCutter.","tokens_in":30016,"tokens_out":13255,"duration_ms":115175,"significance":"If established, the equivalence in Theorem 5 would be a valuable contribution: it would allow the exchange of correctness witnesses between verifiers based on different concurrency semantics, with validation soundly performed by either kind of tool. The paper's concrete YAML format, the artifact, and the detailed bug reports from both Goblint and Ultimate GemCutter are significant practical contributions, and the paper is transparent about limitations and threats to validity. However, the central theoretical claim is not actually proved in the submitted manuscript, and the empirical summary contains a numerical inconsistency, so the contribution is currently not fully supported.","major_comments":[{"comment":"Theorem 5 depends on both directions of Theorem 4. The direction P safe implies split P safe — equivalently, the contrapositive that any violation of split P yields a violation of P — is stated as Theorem C.2 in Appendix C.1 with the proof literally marked 'Without proof.' Corollary 3, which asserts the same implication, is also given without a derivation, and the paragraph following Corollary 3 states the converse of the corollary. Since Theorem 5 is the paper's central 'coincides' claim, this is a load-bearing gap: the manuscript does not establish that an interleaving-valid witness is also valid under the local trace semantics, even assuming all other results. A complete proof of Theorem C.2 (or a fully worked proof of the missing direction of Theorem 4) is required before the main claim can be accepted.","section":"Section 4, Appendix C.1"},{"comment":"The abstract states that the model checker can confirm 75% of the generated witnesses, but this percentage is not derivable from Table 1. The table yields 653/787 ≈ 83% confirmed for witnesses of correct programs, 710/1165 ≈ 61% for witnesses of incorrect programs, and 1363/1952 ≈ 70% overall. Please reconcile the abstract's number with the reported data, or explicitly state the denominator and the subset of witnesses used for the 75% figure.","section":"Abstract, Table 1"}],"minor_comments":[{"comment":"The formal definition of local trace semantics is deferred to Schwarz et al. [71]; for a self-contained extended version, it would be helpful to include the key definitions and consistency requirements directly, since Theorem 1 and Theorem 5 both rely on this semantics.","section":"Section 2.3"},{"comment":"The claim that the critical-section encoding may introduce deadlocks that 'do not unduly restrict the set of reachable states' is made without argument. Since this is exactly the point that the unproved Theorem C.2 must justify, the statement should either be proved or explicitly identified as part of the missing proof.","section":"Section 4"},{"comment":"In Table 1, the 'rejected' rows are all zero, while the text separately reports 12 crashes due to ghost updates at unsupported locations and 58 cases of unsupported C features. It would be clearer to account for these cases explicitly in the table or in a footnote, so that the reader can see how they relate to the 'out of resources' counts.","section":"Section 7.2"},{"comment":"The C-level witness semantics is justified via sequence points and the assumption of data-race freedom, but the connection between these C-specific notions and the abstract Lang/Split semantics is only informal. A precise statement of the intended correspondence would strengthen the paper's claim that the abstract equivalence transfers to the implemented format.","section":"Section 6"}],"recommendation":"major_revision","confidential_remarks":"The manuscript has a strong practical component, and the artifact and bug reports are valuable. However, the theoretical centerpiece — the equivalence in Theorem 5 — is not proved because the needed direction of Theorem 4 is explicitly marked 'Without proof.' The 75% figure in the abstract also needs correction. If the authors can supply the missing proof and fix the numerical inconsistency, the paper could become a solid contribution; as it stands, the central claim is not yet established."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, the engineering is real: a YAML-based ghost-witness format for concurrent programs, implemented in Goblint and Ultimate GemCutter, with an artifact and 29 pre-existing bugs found across the two tools. That is a solid, useful contribution. Second, the central theoretical claim—Theorem 5, that witness validity coincides between interleaving and local-trace semantics—is not actually established. The proof reduces to Theorem 4, whose direction “split P safe implies P safe” is Theorem C.2, and the proof of that theorem in Appendix C.1 is literally the words “Without proof.” This is load-bearing, not cosmetic. If that direction fails, an interleaving-valid witness could produce an unsafe split program, and a thread-modular validator would reject a witness that is valid under interleaving semantics. The paper is candid about the omission, but the coincidence theorem is the headline and it is currently a conjecture, not a theorem.\n\nWhat the paper does well: the format itself is a natural extension of the sequential witness format, the ghost-variable encoding is explained clearly, and the evaluation is honest about threats to validity. Finding 29 bugs, including soundness-critical ones, is a meaningful empirical result and a good argument for adoption even without the full theory. The abstract's 75% confirmation rate does not match Table 1 exactly—the overall confirmed rate is closer to 70%, with 83% on correct programs and 61% on incorrect ones—but that is a minor precision issue in the abstract, not a fatal flaw.\n\nThe soft spot is the unproved theorem. The rest of the formal development, including the ghost-instrumentation preservation lemmas, is sketched or proved in the appendix and looks plausible. The missing direction is the only part I would call a genuine gap, and the authors clearly know it exists.\n\nWho is this for? Tool developers in concurrency verification, especially those working on SV-COMP witnesses. They will get practical value from the format and the bug list. The theoretical claim should not be cited as a proven theorem until the proof appears.\n\nMy recommendation: send it to peer review, but with the explicit expectation that the authors either provide a full proof of Theorem C.2 or re-scope Theorem 5 as a conjecture with empirical support. The engineering and the bug findings deserve publication; the theorem needs to be fixed or downgraded.","headline":"Genuinely useful witness format and a 29-bug payoff, but the headline equivalence theorem rests on a direction the paper leaves unproved.","tokens_in":30567,"tokens_out":1945,"would_cite":true,"duration_ms":19542,"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 establishes that correctness witnesses for concurrent programs can be defined so that their validity is the same under both interleaving semantics and thread-modular semantics, by attaching ghost-variable updates and invariants…","keywords":["concurrent programs","correctness witnesses","ghost variables","thread-modular semantics","interleaving semantics","abstract interpretation","model checking","software verification"],"falsifier":"Take a ghost-instrumented program whose atomic-block semantics is safe, encode its atomic blocks as critical sections with per-global mutexes, and search the encoded program for an assertion violation; a single such case would directly contradict the unproved direction of Theorem C.2 and, through it, Theorem 5.","tokens_in":116,"feed_emoji":"👻","tokens_out":9269,"duration_ms":146354,"temperature":0.7,"pith_summary":"This paper proposes a format for correctness witnesses of concurrent programs—evidence that a program satisfies an assertion—that works equally well for analyzers that reason by interleaving all thread actions and analyzers that reason thread-by-thread with a local trace semantics. The key idea is to let a witness add ghost variables: auxiliary variables that do not affect program behavior, updated atomically with real statements, plus location invariants over both real and ghost variables. Instrumenting the program with these ghosts turns witness validity into ordinary safety of the instrumented program, and the paper argues that safety under the two semantics coincides for such programs. If the central result holds, a correctness proof produced by a thread-modular analyzer can be checked by an interleaving model checker, and vice versa, without the validator needing to know which semantics produced the witness. In the evaluation, an independent model checker confirmed 75% of the witnesses generated this way, and the exchange exposed 29 pre-existing bugs in the two tools.","feed_headline":"Ghost variables bridge two semantics for concurrent proofs","feed_subtitle":"Validity is the same under both semantics, so different verifiers can check each other's proofs.","key_machinery":"The load-bearing object is the ghost witness $(D,X,U,I)$: ghost global declarations $D$, ghost local variables $X$, a partial function $U$ attaching ghost updates to program edges, and location invariants $I$. It operates through the witness-instrumented program $P^W$, in which each original action is executed atomically together with its ghost update and invariant checks are inserted as atomic assertions. To move between semantics, the split transformation rewrites every atomic block as a critical section guarded by the per-global mutexes of the variables it accesses. The chain of equivalences—Theorem 4 ($P$ safe iff $\\mathrm{split}\\,P$ safe) and Theorem 1 (safe under interleaving iff safe under local traces for guarded programs)—is what lifts the two semantics to agreement on witness validity in Theorem 5.","core_discovery":"On the paper's own terms, the central discovery is Theorem 5: a witness $W$ for a program $P$ is valid with respect to the interleaving semantics if and only if it is valid with respect to the local trace semantics. Validity is not defined by a bespoke witness checker; it is defined by building the witness-instrumented program $P^W$, which adds ghost declarations and updates plus location invariants, and asking whether $P^W$ is safe. Ghost updates are folded with original statements into atomic blocks, and the split transformation encodes those atomic blocks as critical sections protected by per-global mutexes. The equivalence chains two earlier results: the mutex encoding preserves safety of atomic-block programs (Theorem 4), and for programs in the guarded language, interleaving and local-trace semantics agree on safety (Theorem 1). The paper further shows how thread-modular invariants—mutex invariants and protected invariants—are naturally expressed in the format by ghost booleans that track whether each mutex is locked and whether the program has become multithreaded.","pith_inferences":["An implicit consequence is that the same ghost mechanism could be reused for violation witnesses: ghost history variables could record enough of an interleaving for a consumer to reconstruct why an assertion fails, giving concurrent violation witnesses a comparable exchange format.","The missing proof for Theorem C.2 is the place to look first: a counterexample would not necessarily destroy the practical format, but it would force validators to treat atomicity as a first-class semantic notion instead of relying on the mutex encoding.","Because the format attaches invariant evaluation to C sequence points, it sidesteps data-race granularity; extending ghost witnesses to weak-memory models would require redefining when an invariant is allowed to observe a partially written shared value.","The approach also suggests a division of labor in tool chains: a lightweight thread-modular analyzer can emit ghost witnesses that a more expensive interleaving model checker then confirms, effectively using witnesses to focus the model checker on the reasoning it needs to re-verify."],"forward_implications":["Witness validity becomes a property of the witness-instrumented program rather than of any particular analyzer, so an independent validator can confirm a concurrent correctness proof without adopting the generator's semantics.","Thread-modular invariants that track lock ownership, including relational mutex invariants, can be packed into the witness format, lowering the adoption barrier for existing verifiers.","Validity under both semantics means that a witness rejected by one kind of validator is rejected by the other, so disagreements between tools can be traced to a bad witness or a buggy validator rather than to a semantic mismatch.","The safety-preservation results guarantee both trust directions: a valid witness forces the original program to be safe, and an unsafe original program can never have a valid correctness witness."],"supporting_citations":[{"why":"Defines the witness format 2.0 with location invariants that the proposed ghost format extends.","marker":"[3]"},{"why":"Provides the thread-modular local trace semantics and its fixed-point formulation used to prove the safety equivalence and to derive thread-modular invariants.","marker":"[71]"},{"why":"Introduces the mutex-meet analysis whose relational invariants are encoded using ghost boolean lock-trackers.","marker":"[72]"},{"why":"Supplies the classical observation that atomic blocks can be encoded as critical sections, which the split transformation relies on.","marker":"[50]"},{"why":"Shows a practical implementation of atomic sections via synchronization inference, supporting the atomic-block-to-critical-section encoding.","marker":"[53]"},{"why":"Presents the sequentialization-based interleaving model checker used as the independent validator of the generated witnesses.","marker":"[28]"},{"why":"Describes the thread-modular abstract interpreter used to generate the ghost witnesses in the evaluation.","marker":"[67]"}],"fun_headline_variants":["Ghosts bridge the gap between two concurrent semantics","Ghost witnesses make concurrency proofs interchangeable","One witness format for interleaving and thread-modular checks","Correctness witnesses for concurrency via ghost instrumentation"],"cache_read_input_tokens":32640,"weakest_assumption_plain":"The unproved direction of Theorem C.2 is the load-bearing assumption: an assertion violation in the critical-section-encoded program must always correspond to a violation in the original atomic-block program.","fun_headline_variants_meta":{"raw":{"variants":["Ghosts bridge the gap between two concurrent semantics","Ghost witnesses make concurrency proofs interchangeable","One witness format for interleaving and thread-modular checks","Correctness witnesses for concurrency via ghost instrumentation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00065,"raw_usage":{"total_tokens":3003,"prompt_tokens":987,"completion_tokens":2016,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":603,"completion_tokens_details":{"reasoning_tokens":1956}},"tokens_in":603,"tokens_out":2016,"duration_ms":14534,"temperature":1.0,"reasoning_tokens":1956,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T12:55:33.521536+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a ghost-instrumented program whose atomic-block semantics is safe, encode its atomic blocks as critical sections with per-global mutexes, and search the encoded program for an assertion violation; a single such case would directly contradict the unproved direction of Theorem C.2 and, through it, Theorem 5.","supporting_citations":[{"cited_title":", Vojdani, V.: Im- proving thread-modular abstract interpretation","cited_arxiv_id":null,"evidence_quote":"Provides the thread-modular local trace semantics and its fixed-point formulation used to prove the safety equivalence and to derive thread-modular invariants."},{"cited_title":"In: Wies, T","cited_arxiv_id":null,"evidence_quote":"Introduces the mutex-meet analysis whose relational invariants are encoded using ghost boolean lock-trackers."},{"cited_title":"In: Wortman, D.B","cited_arxiv_id":null,"evidence_quote":"Supplies the classical observation that atomic blocks can be encoded as critical sections, which the split transformation relies on."},{"cited_title":"In: Tools and Algorithms for the Construction an d Anal- ysis of Systems, pp","cited_arxiv_id":null,"evidence_quote":"Describes the thread-modular abstract interpreter used to generate the ghost witnesses in the evaluation."}],"review_version":1}