Pith. sign in

REVIEW 18 references

A Formal Semantics of C with OpenMP Parallelism (Extended Version)

T0 review · reviewed 2026-06-29 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A formal semantics extending CompCert to OpenMP directives guarantees that any successful execution of the resulting C program is free of data races.

desk verdict 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. read the letter →

arxiv 2605.26527 v2 pith:GTFVNJMP submitted 2026-05-26 cs.DC cs.PL

Ke Du , Anshu Sharma , Liyi Li , William Mansky This is my paper · ORCID
classification cs.DCcs.PL
keywords formalsemanticsOpenMPCompCertdataracesconcurrencyClanguageparallelprogrammingverifiedcompilation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

An execution trace that the semantics accepts yet contains a data race on a shared variable would falsify the race-freedom guarantee.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

The extension of CompCert's concurrency semantics to OpenMP directives accurately captures all subtle interactions with variable state as specified in the OpenMP standard.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 0 minor

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.

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.

Simulated Author's Rebuttal

0 responses · 0 unresolved

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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity identified

full rationale

The paper defines a formal semantics for C+OpenMP by extending the external CompCert concurrency model. The central claim (race freedom for successful executions) is a direct consequence of the operational transition rules that the authors introduce; it does not reduce to any fitted parameter, self-definition, or load-bearing self-citation. The derivation is therefore self-contained within the constructed model and independent of the inputs it is built from.

Assumptions & free parameters 0 free parameters · 1 assumptions · 0 invented entities

Only the abstract is available, so the ledger is limited to the explicit dependency stated. The central claim rests on the soundness of the base CompCert semantics and concurrency extension.

assumptions (1)
  • domain assumption CompCert C semantics and its concurrency extension provide a correct foundation for modeling C programs with OpenMP.
    The paper states it builds directly on this prior work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Formal Semantics of C with OpenMP Parallelism (Extended Version)." pith.science (2026). https://pith.science/paper/GTFVNJMP

@misc{pith2026260526527,
  author       = {Pith},
  title        = {Pith review of: A Formal Semantics of C with OpenMP Parallelism (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GTFVNJMP}},
  note         = {Machine review of arXiv:2605.26527}
}
read the original abstract

OpenMP is a popular parallelization framework that lets users transform sequential code into parallel code with a few simple annotations. Unfortunately, it is also easy to inadvertently introduce errors by adding OpenMP pragmas into otherwise correct programs, including both logic errors and race conditions. 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.

Figures

Figures reproduced from arXiv: 2605.26527 by the authors.

Figure 1
Figure 1. Left: a typical OpenMP program. Right: an incorrect OpenMP program. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Semantic rules: parallel, for, single, barrier while updating the team tree with h, where h may bind the original thread pool P and team tree T , and the new team tree is h(T , i). We omit h if the team tree is not updated. The Step-Thread rule in [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 4
Figure 4. An OpenMP program with a single construct. The Parallel Construct The main structuring construct in OpenMP is the parallel construct, which creates a team of threads to execute a parallel region. When a thread i reaches a SPar statement, the rule Step-Parallel forks a team of threads executing the region’s body s in parallel. For example, in [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figures from the paper (11 more)
Figure 5
Figure 5. Figure 5: OpenMP programs with the barrier constructs. Step-Barrier requires all threads in this team wait at the same barrier, and the idx of the barrier distinguishes syntactically distinct barriers. Consider the program in Figure 5b: omp_get_thread_num 11 returns 0 for the le…
Figure 6
Figure 6. Figure 6: Semantic rules: private, reduction. Supporting operations priv, end_priv and red are defined in [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: An OpenMP program with a private clause, adapted from [13]. the exception that variables in reduction clauses are implicitly privatized and initialized13). We then add an SPrivEnd instruction to the end of the region, with an argument leo containing the original memory…
Figure 8
Figure 8. Figure 8: An OpenMP program with a reduction clause Reduction A reduction variable is a special kind of private variable for which, instead of returning to the original value after the region ends, we apply some operation to combine all of the private copies into a new value for…
Figure 9
Figure 9. Figure 9: ClightOMP Syntax. SPriv, SPrivEnd, SRed are generated at runtime, and le stores runtime values. B Nested Parallel Region [PITH_FULL_IMAGE:figures/full_fig_p020_9.png]
Figure 10
Figure 10. Figure 10: An OpenMP program with nested parallel regions I, II and III, marked [PITH_FULL_IMAGE:figures/full_fig_p021_10.png]
Figure 11
Figure 11. Figure 11: (c), when t1 of the team {t1 , t2 } meets the parallel construct on line 4 in [PITH_FULL_IMAGE:figures/full_fig_p021_11.png]
Figure 12
Figure 12. Figure 12: Team tree operations op(T, i), leader(T , i), team_tids(T , i) and the node operations that op(T, i) is lifted from. D Supporting Privatization and Reduction Operations We first define some notations: # [t0;t1;...;tk] j fj ≜ftk ◦ · · · ◦ ft1 ◦ ft0 where ∀j ∈ [t0;t1; .…
Figure 13
Figure 13. Figure 13: Supporting functions for privatization and reduction. [PITH_FULL_IMAGE:figures/full_fig_p023_13.png]
Figure 14
Figure 14. Figure 14: An OpenMP program. 𝑟 ↦ி 0 𝑟 ↦ோ 0 𝑟 ↦ோ 0 𝑟 ↦ோ 0 𝑟ଵ ↦ி 0 𝑟 ↦ோ 0 𝑟ଶ ↦ 0 𝑟 ↦ோ 0 𝑟ଵ ↦ி 𝑛 𝑟 ↦ோ 0 𝑟ଶ ↦ி 𝑚 SPar SFor SBRB 𝑟 ↦ோ 𝑛+𝑚 𝑟ଶ ↦ி 𝑛 𝑟 ↦ோ 𝑛+𝑚 SPrivEnd 𝑡ଵ 𝑡ଶ 𝑡ଵ SFor 𝑟 ↦ோ 𝑛+𝑚 𝑟ଶ ↦ி 𝑚 SBRB SPrivEnd 𝑟 ↦ோ 𝑛+𝑚 𝑟 ↦ி 𝑛+𝑚 𝑟 ↦ி 𝑛+𝑚 SPrivEnd SPrivEnd (halts) loop iterations loop …
Figure 16
Figure 16. Figure 16: ClightOMP memory events emitted by a step. [PITH_FULL_IMAGE:figures/full_fig_p025_16.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

18 extracted references · 9 canonical work pages

  1. [1]

    In: Proceedings of the 9th International Workshop on Software Correctness for HPC Applications

    Ahmmed, J., Mahmud, Q.I., Shim, J., Li, L., Jannesari, A., Cohen, M.B.: Differ- ential testing for sequential to parallel transformations. In: Proceedings of the 9th International Workshop on Software Correctness for HPC Applications. Correct- ness ’25 (2025)

    2025

  2. [2]

    Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cam- bridge University Press (2014),http://www.cambridge.org/de/academic/ subjects/computer-science/programming-languages-and-applied-logic/ program-logics-certified-compilers?format=HB

    2014

  3. [3]

    In: 2018 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW)

    Atzeni, S., Gopalakrishnan, G.: An operational semantic basis for building an OpenMP data race checker. In: 2018 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW). pp. 395–404 (2018).https://doi. org/10.1109/IPDPSW.2018.00074

    work page doi:10.1109/ipdpsw.2018.00074 2018

  4. [4]

    In: Inter- national Conference on Interactive Theorem Proving

    Besson, F., Blazy, S., Wilke, P.: A concrete memory model for compcert. In: Inter- national Conference on Interactive Theorem Proving. pp. 67–83. Springer (2015)

    2015

  5. [5]

    openmp.org/wp-content/uploads/OpenMP-API-Specification-6-0.pdf(2024)

    Board, O.A.R.: OpenMP Application Programming Interface.https://www. openmp.org/wp-content/uploads/OpenMP-API-Specification-6-0.pdf(2024)

    2024

  6. [6]

    Cuellar, S., Giannarakis, N., Madiot, J.M., Mansky, W., Beringer, L., Cao, Q., Appel, A.: Compiler correctness for concurrency: from concurrent separation logic to shared-memory assembly language. Tech. rep., Princeton University (2020)

    2020

  7. [7]

    In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Princi- ples of Programming Languages

    Ellison, C., Rosu, G.: An Executable Formal Semantics of C with Applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Princi- ples of Programming Languages. pp. 533–544. POPL ’12, ACM, New York, NY, USA(2012).https://doi.org/10.1145/2103656.2103719,http://doi.acm.org/ 10.1145/2103656.2103719

    work page doi:10.1145/2103656.2103719 2012

  8. [8]

    Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv

    Jiang, H., Liang, H., Xiao, S., Zha, J., Feng, X.: Towards certified separate compilation for concurrent programs. In: Proceedings of the 40th ACM SIG- PLAN Conference on Programming Language Design and Implementation. p. 111–125. PLDI 2019, Association for Computing Machinery, New York, NY, USA(2019).https://doi.org/10.1145/3314221.3314595,https://doi.or...

    work page doi:10.1145/3314221.3314595 2019

Show all 18 references
  1. [9]

    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM21(7), 558–565 (Jul 1978).https://doi.org/10.1145/359545. 359563,https://doi.org/10.1145/359545.359563

    1978 doi

  2. [10]

    Communications of the ACM 52(7), 107–115 (Jul 2009).https://doi.org/10/c9sb7q,http://doi.acm.org/ 10.1145/1538788.1538814

    Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (Jul 2009).https://doi.org/10/c9sb7q,http://doi.acm.org/ 10.1145/1538788.1538814

    2009 doi

  3. [11]

    In: Proceedings of the 39th ACM International Conference on Supercomputing

    Mahmud, Q.I., TehraniJamsaz, A., Ahmed, N.K., Willke, T.L., Jannesari, A.: Con- traph: Contrastive learning for parallelization and performance optimization. In: Proceedings of the 39th ACM International Conference on Supercomputing. pp. 596–610 (2025)

    2025

  4. [12]

    In: Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers)

    Mahmud,Q.I.,TehraniJamsaz,A.,Phan,H.D.,Chen,L.,Capotă,M.,Willke,T.L., Ahmed, N.K., Jannesari, A.: Autoparllm: Gnn-guided context generation for zero- shot code parallelization using llms. In: Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Asso...

    2025

  5. [13]

    hands-on

    Mattson, T.: A “hands-on” introduction to openMP*.https://www.openmp. org/wp-content/uploads/Intro_To_OpenMP_Mattson.pdf(2013), located at https://www.openmp.org/resources/tutorials-articles/ A Formal Semantics of C with OpenMP Parallelism 29

    2013

  6. [14]

    Memarian, K., Gomes, V.B.F., Davis, B., Kell, S., Richardson, A., Watson, R.N.M., Sewell, P.: Exploring C Semantics and Pointer Provenance. Proc. ACM Program. Lang.3(POPL), 67:1–67:32 (Jan 2019).https://doi.org/10.1145/ 3290380,http://doi.acm.org/10.1145/3290380

    2019 doi

  7. [15]

    SIG- PLANNot.51(6),1–15(Jun2016).https://doi.org/10.1145/2980983.2908081, https://doi.org/10.1145/2980983.2908081

    Memarian, K., Matthiesen, J., Lingard, J., Nienhuis, K., Chisnall, D., Watson, R.N.M., Sewell, P.: Into the Depths of C: Elaborating the de Facto Standards. SIG- PLANNot.51(6),1–15(Jun2016).https://doi.org/10.1145/2980983.2908081, https://doi.org/10.1145/2980983.2908081

    doi

  8. [16]

    In: SC ’15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis

    Siegel, S.F., Zheng, M., Luo, Z., Zirkel, T.K., Marianiello, A.V., Edenhofner, J.G., Dwyer, M.B., Rogers, M.S.: Civl: the concurrency intermediate verifica- tion language. In: SC ’15: Proceedings of the International Conference for High Performance Computing, Networking, Stora...

    2015 doi

  9. [17]

    Advances in Neural Information Processing Systems37, 100965–100999 (2024)

    Tehrani, A., Bhattacharjee, A., Chen, L., Ahmed, N.K., Yazdanbakhsh, A., Jan- nesari, A.: Coderosetta: Pushing the boundaries of unsupervised code translation for parallel programming. Advances in Neural Information Processing Systems37, 100965–100999 (2024)

    2024

  10. [18]

    Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: Com- pCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM60(3), 22:1–22:50 (Jun 2013).https://doi.org/10.1145/2487241.2487248,http:// doi.acm.org/10.1145/2487241.2487248

    2013 doi

Pith tools

Reviewed June 29, 2026 · model on record in the stance chip above.