A Formal Semantics of C with OpenMP Parallelism
This work provides a rigorous foundation for detecting errors in parallel C programs using OpenMP, addressing a need for formal verification of parallel code.
The paper presents a formal semantics for C with OpenMP directives, building on CompCert's C semantics and its concurrency extension. The semantics captures subtle interactions between OpenMP directives and variable state, and guarantees that any successful execution is free of data races.
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.