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.

翻译：OpenMP是一种流行的并行化框架，它允许用户通过简单的注解将顺序代码转换为并行代码。然而，在原本正确的程序中添加OpenMP编译指示容易意外引入错误，包括逻辑错误和数据竞争。我们基于CompCert验证编译器的C语言语义及其并发扩展，提出了一种带有OpenMP指令的C语言代码的形式语义。该语义捕捉了OpenMP指令与变量状态之间微妙的交互作用——这些交互在以往的OpenMP语义中被模糊处理——并为检测因错误注解而引入的非期望行为提供了基础：特别地，任何成功的执行均可保证无数据竞争。