{"id":"125a1a25-df19-4f41-b997-d415e04ff38f","arxiv_id":"2605.26527","paper_version":2,"verdict":"UNVERDICTED","confidence":"LOW","novelty_score":6.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":0,"one_line_summary":"Defines formal semantics for C with OpenMP directives extending CompCert, with a guarantee that successful executions are race-free.","lead":"This paper defines a formal semantics for C programs using OpenMP parallel directives by extending the CompCert verified compiler's C semantics and its concurrency extension. It guarantees that any successful execution under the semantics is free of data races, providing a basis to detect errors from incorrect annotations.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.3","headline":"No significant objection identified","rationale":"The reader's weakest assumption concerns fidelity to the OpenMP standard, which is a modeling question rather than a flaw in the internal argument for the stated safety property. Because the claim is scoped to executions inside the semantics, and no counter-example to the derivation is apparent, the load-bearing step for the headline claim holds.","tokens_in":1576,"tokens_out":275,"duration_ms":18907,"concrete_test":"Extract the inductive definition of 'successful execution' and the statement of the race-freedom theorem from the paper; check that every transition rule used in the proof either forbids a data race by construction or is covered by an explicit case analysis that rules out races.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the presented semantics guarantees race freedom for any successful execution. This is a property internal to the model: the semantics is constructed by extending CompCert's concurrency model with OpenMP directives, and the race-freedom result follows from the operational rules that prevent unsynchronized accesses from completing. No internal inconsistency, missing case in the transition rules, or unstated assumption about variable state is visible that would invalidate the derivation of the safety property. The separate question of fidelity to the OpenMP standard is outside the scope of the claim as stated.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.3","summary":"The manuscript develops a formal operational semantics for C programs with OpenMP directives by extending CompCert's C semantics and its concurrency model. It claims to capture subtle interactions between OpenMP directives and variable state that prior semantics obscured, and asserts that any successful execution is guaranteed to be free of data races.","tokens_in":1664,"tokens_out":156,"duration_ms":34445,"significance":"If the central claim holds, the work supplies a rigorous, model-internal foundation for reasoning about OpenMP-annotated C code and for detecting annotation-induced errors. Extending a verified artifact such as CompCert strengthens the soundness of the resulting semantics and provides a basis for future verification tools.","major_comments":[],"minor_comments":[],"recommendation":"accept","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for their positive assessment of the manuscript and their recommendation to accept. No major comments appear in the report, so we have no specific points requiring response or revision.","responses":[],"tokens_in":1051,"tokens_out":55,"duration_ms":24240,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"The main thing to know is that this paper adds OpenMP directives to CompCert's C concurrency semantics and derives a race-freedom guarantee for any execution that completes under the new rules. The claim is internal to the model: the operational rules are written so that unsynchronized accesses do not produce a result.\n\nWhat is new is the set of transition rules for OpenMP constructs and the way they interact with shared state. The abstract notes that this captures interactions missed by earlier OpenMP semantics. Building directly on the CompCert concurrency extension is a reasonable move; it reuses an existing formal base instead of inventing a new one from scratch.\n\nThe work is clearest on the safety property itself. If the rules are set up to block data races by construction, then the guarantee follows without extra assumptions. That part looks internally consistent based on the description.\n\nThe soft spot is the missing detail. No rules, no proof sketch, and no example derivations appear in the abstract, so it is not possible to check whether the OpenMP cases are handled completely or whether the model stays close enough to the standard for the result to be useful in practice. Fidelity to the actual OpenMP specification is left as a separate question.\n\nThis paper is for people who work on formal semantics for parallel languages or who want a verified foundation for tools that check OpenMP code. A reader already familiar with CompCert would get the most out of the extension.\n\nIt is worth sending to peer review. The artifact is concrete, the claim is stated clearly, and the base is established, even if the full definitions will need careful checking.","headline":"They extend CompCert with OpenMP rules to get a semantics where successful executions are race-free, but the abstract leaves the actual definitions and proofs out of view.","tokens_in":2127,"tokens_out":405,"would_cite":false,"duration_ms":25179,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"A formal semantics extending CompCert to OpenMP directives guarantees that any successful execution of the resulting C program is free of data races.","keywords":["formal semantics","OpenMP","CompCert","data races","concurrency","C language","parallel programming","verified compilation"],"falsifier":"An execution trace that the semantics accepts yet contains a data race on a shared variable would falsify the race-freedom guarantee.","tokens_in":2471,"feed_emoji":"","tokens_out":628,"duration_ms":26132,"temperature":0.7,"pith_summary":"The paper defines a formal operational semantics for C programs that include OpenMP parallelization directives by extending the existing CompCert C semantics and its concurrency model. This semantics tracks how OpenMP constructs interact with variable states and memory accesses in ways that earlier informal or less precise models left unclear. If the model is faithful to the OpenMP standard, then any execution path that the semantics permits must be free of data races, giving a mechanical way to detect when an annotation has introduced a race. A reader would care because OpenMP is a common way to add parallelism to existing C code, yet it is easy to create subtle concurrency bugs that are hard to find by testing alone.","feed_headline":"Semantics for C with OpenMP guarantees race-free runs","feed_subtitle":"Extending CompCert's concurrency model ensures successful executions contain no data races.","key_machinery":"The extension of CompCert's concurrency semantics to OpenMP directives, which augments the memory and thread-state model to enforce race-freedom on accepted executions.","core_discovery":"We present a formal semantics for C code with OpenMP directives, building on the C semantics of the CompCert verified compiler and its extension to concurrency. Our semantics captures subtle interactions between OpenMP directives and variable state that have been obscured by previous OpenMP semantics, and provides a basis for detecting undesired behaviors introduced by incorrect annotations: in particular, any successful execution is guaranteed to be free of data races.","pith_inferences":["The same semantic extension approach could be applied to other directive-based parallel frameworks to obtain similar race-freedom guarantees.","Compiler passes that insert OpenMP annotations could be proved correct with respect to this semantics.","The model might serve as a reference when comparing the behavior of different OpenMP implementations."],"forward_implications":["Any execution permitted by the semantics contains no data races.","Incorrect OpenMP annotations that would create races can be detected because they lead to no successful executions.","The semantics supplies a foundation for building verification or analysis tools that check OpenMP-parallelized C programs.","Subtle state interactions introduced by OpenMP constructs are made explicit in the model."],"fun_headline_variants":["CompCert semantics for OpenMP in C guarantees no races","CompCert concurrency model formalizes OpenMP C no data races","Semantics extends CompCert to OpenMP for race-free C executions","OpenMP C gets formal CompCert semantics ensuring no races"],"cache_read_input_tokens":64,"weakest_assumption_plain":"The extension of CompCert's concurrency semantics to OpenMP directives accurately captures all subtle interactions with variable state as specified in the OpenMP standard.","fun_headline_variants_meta":{"raw":{"variants":["CompCert semantics for OpenMP in C guarantees no races","CompCert concurrency model formalizes OpenMP C no data races","Semantics extends CompCert to OpenMP for race-free C executions","OpenMP C gets formal CompCert semantics ensuring no races"]},"model":"grok-4.3","cost_usd":0.007621,"raw_usage":{"total_tokens":3432,"prompt_tokens":552,"num_sources_used":0,"completion_tokens":67,"cost_in_usd_ticks":76212000,"prompt_tokens_details":{"text_tokens":552,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":2813,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":552,"tokens_out":67,"duration_ms":29944,"temperature":1.0,"reasoning_tokens":2813,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-06-29T16:08:52.616517+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"An execution trace that the semantics accepts yet contains a data race on a shared variable would falsify the race-freedom guarantee.","supporting_citations":[],"review_version":1}