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语义中常被模糊处理——并为检测由错误注释导致的不良行为提供了基础：特别地，任何成功执行的程序都保证无数据竞争。