A Formal Semantics of C with OpenMP Parallelism (Extended Version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911722568155136 |
|---|---|
| author | Du, Ke Sharma, Anshu Li, Liyi Mansky, William |
| author_facet | Du, Ke Sharma, Anshu Li, Liyi Mansky, William |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_26527 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Formal Semantics of C with OpenMP Parallelism (Extended Version) Du, Ke Sharma, Anshu Li, Liyi Mansky, William Distributed, Parallel, and Cluster Computing Programming Languages D.3.1 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. |
| title | A Formal Semantics of C with OpenMP Parallelism (Extended Version) |
| topic | Distributed, Parallel, and Cluster Computing Programming Languages D.3.1 |
| url | https://arxiv.org/abs/2605.26527 |