arXiv CSopen access

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

A Formal Semantics of C with OpenMP Parallelism Ke Du1[0009−0008−2465−1082] , Anshu Sharma2[0000−0002−8686−5835] , Liyi Li3[0000−0001−8184−0244] , and William Mansky1[0000−0002−5351−895X] University of Illinois Chicago The College of William and Mary 3 Iowa State University

arXiv:2605.26527v2 [cs.DC] 27 May 2026

1

2

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. Keywords: OpenMP · Formal Semantics · Concurrency.

1

Introduction

The OpenMP framework [5] provides a straightforward entry point for sharedmemory parallel programming. Instead of explicitly creating and managing threads and locks, a programmer can write a sequential program and then use the OpenMP API to instruct the compiler to automatically parallelize the code, e.g., by distributing the iterations of a loop across multiple threads. The core of the API is a set of compiler directives (#pragmas in C and C++) that can be added before the code segments to be parallelized, supported by common compilers including GCC and Clang. However, the simplicity of this interface can be deceptive—OpenMP still suffers from all the complexity of shared-memory concurrency, and choosing the wrong directives can easily introduce race conditions or logic errors. Prior work [3] defined formal semantics for OpenMP for the purpose of race detection, modeling the synchronization effects of key directives and the memory accesses they produce. This is useful for detecting concurrency bugs, but does not fully address the question “what is this OpenMP program allowed to do?” In this work, we aim to answer that question with a formal semantics for OpenMP at the language level, specifically for C programs with OpenMP annotations.

2

K. Du et al.

Our semantics builds on CompCert’s C semantics [10] and its extension to concurrency [6], giving us high confidence in our base language semantics; our task is then to accurately capture the allowed behavior of OpenMP directives. There are three main challenges to giving formal semantics for OpenMP at the language level: 1. The OpenMP API is not a library of functions but a set of compiler directives that modify the behavior of the code they apply to. These directives cannot be modeled as special function calls executed in a single step, as is standard in concurrent extensions of CompCert, since, at a minimum, they may have effects at both the beginning and the end of the affected block. 2. Unlike standard fork-join concurrency, in which an unstructured collection of threads interacts peer-to-peer via shared memory or message passing, OpenMP describes the behavior of dynamically created teams of threads, and the validity and effects of directives depend on the team to which the executing thread currently belongs. Any formal model of OpenMP must track the team structure of the executing threads in addition to more usual forms of state. 3. OpenMP directives have subtle effects on local variables: depending on the position of its declaration and the details of the directive, a variable may be treated as shared memory across multiple threads or split into private copies that may be reconciled at the end of a parallel section—and mistakes in variable-handling directives are a major source of OpenMP-induced bugs. By carefully modeling the scope of OpenMP directives and their effects on team structure and local variables, in addition to their concurrency and memory behavior, our semantics provide a basis for determining the allowed behavior of an OpenMP-annotated program, and thus ultimately for determining whether a given parallelization preserves the intended behavior of the code. Our semantics is stuck in the presence of memory errors or data races, making it useful for bug-finding. The semantics can also serve as a basis for analysis tools that prove the safety and functional correctness of OpenMP C programs. 1.1

A Motivating Example

We illustrate the uses and challenges of our semantics with a typical OpenMP program (shown on the left of Figure 1) and a typical OpenMP mistake (shown on the right). The core mechanism of OpenMP is a set of directives, compiler annotations to parallelize a sequential program, implemented as #pragmas in C. Some directives are associated with the following code block, binding to them to form a construct. Other directives, such as barrier, do not associate with a statement and form a construct by themselves. In the left program, parallel num_threads(2) is an OpenMP directive that specifies that a team of two threads should execute the associated code in parallel, with all threads executing the same code block. The omp for directive on line 5 is always associated with a for-loop, and divides the workload of the associated forloop among the threads of the executing team. When this program executes, it

A Formal Semantics of C with OpenMP Parallelism 1 2 3 4 5 6 7 8 9 10

// program starts with one thread t1 #pragma omp parallel num_threads(2) {// a team of 2 threads {t1, t2} is created f () ; #pragma omp for for ( i=0; i<6; i+=1) { // each thread only works a loop partition loop_body } }// end of parallel region , only thread is t1

1 2 3 4 5 6 7

3

int k = 0, s = 0; #pragma omp parallel for reduction(+ : k, s) for (int i = 0; i < 128; i++) { k = k + 3; s = s + k; }

Fig. 1: Left: a typical OpenMP program. Right: an incorrect OpenMP program.

begins with a single thread of execution; at line 2, the parallel directive creates a team with two threads; and the iterations of the for-loop on line 6 are partitioned across the threads, e.g., each thread may execute three steps of the loop. This illustrates several challenges in defining the semantics of OpenMP: 1. The for directive is team-sensitive, i.e., the partitioning of the loop at line 5 depends on the number of threads set up in line 2. 2. OpenMP does not check for race-freedom: if loop_body is not safe to run in parallel, the program will not execute correctly. 3. At the end of the parallel block at line 10, there is an implicit barrier: every thread in the team must wait until all threads finish their tasks. Our semantics must track the team structure throughout the program, detect race conditions among threads, and capture the effects of both the start and end of a construct. Another difficulty arises from the complex interaction between OpenMP directives and local variables, as shown in the right program in Figure 1 (adapted from Ahmed et al. [1]). When run sequentially, this program sums the multiples of 3 from 3 to 3 * 128. The reduction clause aims to divide the work across threads; each thread receives its own copies of k and s, and the copies are summed at the end of the loop. For k, this will indeed produce the right result (3 * 128 = 384). However, depending on the distribution of loop iterations among threads, some per-thread values of k will be reused in computing s, while other values will never be reached, producing an incorrect final value of s. This program does not contain a data race—it is not buggy in and of itself—but it does not have the same semantics as the corresponding sequential program, and we can only determine this by modeling the values of k and s in each thread. Notably, the main prior work on the semantics of OpenMP [3] works at the level of memory operations, obscuring the effects of OpenMP directives on variables and control flow. In contrast, our OpenMP semantics directly models the effects of directives on the C program state, allowing us to detect errors like that on the right of Figure 1.

4

K. Du et al.

1.2

Contributions and Roadmap

The main contribution of this paper is, to our knowledge, the first formalization of OpenMP semantics in C at the language level. We formalize 5 constructs and 3 clauses representing commonly used OpenMP directives. In particular, we give the first formal semantics for the for and single clauses, which control worksharing within teams, and the private and reduction clauses, which control the interaction between threads and local variables. Our novel team tree construction captures the essence of OpenMP’s execution model and could be reused to define OpenMP semantics in other languages, such as C++ or FORTRAN. Our semantics is based on per-thread permissions to memory, and we prove that any execution in our semantics is data-race-free. The paper is structured as follows. In Sections 3.1 and 3.2, we describe the syntax of ClightOMP and the team tree model that plays a key role in ClightOMP program states. In Section 3.3, we formally present our operational semantic rules for OpenMP and describe in detail the semantics of the major constructs and clauses of OpenMP: parallel and worksharing constructs, barriers, and privatization and reduction clauses. The ClightOMP semantics is formalized in the Rocq proof assistant4 . Section 4 describes the properties of the semantics, including a proof of data-race freedom for any execution. Finally, in section 5 we compare with related work, and in section 6 we summarize our results and discuss future work.

2

Background: The Concurrent Permission Machine

Since our goal is to give precise semantics for C programs with OpenMP directives, we begin with the authoritative formal semantics of ordinary C, the Clight semantics of the CompCert verified compiler [10]. However, CompCert’s model of C does not include concurrency—it is strictly a sequential semantics. Several more recent works, including CASCompCert [8] and the Concurrent Permission Machine (CPM) [6], lift Clight to concurrency by defining a multithreaded machine where each step is either a sequential Clight step or a concurrency operation; our semantics builds on the CPM approach. In this section, we explain the parts of the CPM’s program states and step rules that will be necessary to understand our semantics. A CPM program state has the form ⟨0, P, m⟩, consisting of a schedule 0, a thread pool P, and a shared memory m. The schedule 0 is a list of thread IDs that determines the order in which threads interleave; the possible behaviors of a program are its behaviors under all schedules. The thread pool P maps each thread ID i to its local state P (i) = ⟨σi , πi ⟩, where σi = ⟨s, le, k⟩ is a Clight state containing the statement s to be executed, the local variable environment le that maps variable names to their addresses in the memory m, and the continuation k; πi is the permission map of thread i, describing the thread’s access level to each memory location (None, Nonempty, Readable, Writable, or Freeable). These 4

Available in https://github.com/dkxb/ClightOMP.

A Formal Semantics of C with OpenMP Parallelism

5

access levels allow the CPM to detect data races: at each step of execution, the permissions held by all threads must be compatible with each other, so that e.g. if one thread holds Writable access to a location, no other thread can hold Readable access. Finally, m is a CompCert memory [4]. For this paper, it can be viewed as a pair ⟨mv , πm ⟩ where mv maps addresses to values, and πm is a placeholder for the executing thread’s permission map. We define a few shorthands: m(l) ≜ m.1(l) for loading a value from address l, perm(m) ≜ m.2 for getting the permission map, m|π ≜ ⟨m.1, π⟩ for replacing the permission in m with π. The operational semantics of the CPM includes two kinds of steps. First, an individual thread may take a step according to the sequential Clight semantics →sq : Step-Clight

P(i) = ⟨σi , πi ⟩

⟨σi , m|πi ⟩ →sq ⟨σi′ , m′ ⟩ P[i ::= ⟨σi′ , perm(m′ )⟩] = P ′ ⟨i · 0, P, m⟩ → ⟨0, P ′ , m′ ⟩

If i is the next thread scheduled to execute, and its current state is ⟨σi , πi ⟩ where σi can execute a sequential C statement, then it executes as follows. First, it combines its permissions πi with the shared memory m to obtain a thread-local “view” of memory m|πi , which has all the same values as m but allows only operations that the thread has permission for (e.g., if πi only has Readable access to a location ℓ, then a write to ℓ in m|πi will fail). The local state σi and local memory m|πi combine to make an ordinary Clight state, which may step according to Clight’s sequential semantics to a new state ⟨σi′ , m′ ⟩. The new memory m′ then becomes the new shared memory, and the thread pool records the new local state σi′ and permissions perm(m′ ) for thread i. The Step-Clight rule applies when the next operation in the scheduled thread is a sequential statement. When it is a concurrency operation, we instead look for a specific rule for that operation in the CPM. For instance, the rule for thread creation is: Step-Spawn

j ̸∈ P πi = πi′ ⊕ πj′ D h i E i · 0, P i ::= ⟨spawn(f, a), le, k⟩, πi , m →

D h i E 0, P i ::= ⟨SSkip, le, k⟩, πi′ , j ::= ⟨f (a), ∅, KStop⟩, πj′ , m The in-place update notation P[i ::= (σ, π)] is the thread pool P but thread i has state (σ, π). If thread i wants to spawn a new thread executing function f with argument a, it can do so by creating a new thread whose code is f (a) with a fresh index j not yet in P. The parent thread’s statement is replaced by the no-op statement SSkip, so its next step will be decided by its continuation k. The new thread has an empty local variable environment ∅ and a continuation KStop, meaning that the thread halts after f (a). The permissions πi of i must be split into two parts, one retained by the parent thread (πi′ ) and one given to the child thread (πj′ ).

6

K. Du et al.

The CPM includes rules for thread creation and lock operations (allocation, deallocation, acquire, and release). Taken together, these implement a concurrent extension of Clight with an SC-DRF (Sequential Consistency for Data-Race-Free programs) memory model: programs with data races are stuck (due to permission conflicts), while programs without data races have sequentially consistent behavior, interleaving the steps of individual threads. We develop our OpenMP semantics by extending the CPM with rules for OpenMP directives like parallel regions and work-sharing constructs, extending the state model as necessary. OpenMP’s memory model is also SC-DRF as long as programs do not use weakmemory atomic constructs (which we do not support), so the CPM provides a reasonable basis for capturing the concurrency behavior of C programs with OpenMP directives.

3

Syntax and Semantics of ClightOMP

ClightOMP extends the syntax of Clight [10], the subset of C formalized in CompCert, with OpenMP directives as new statements. The full syntax is defined in Figure 9. In this section, we introduce the syntax and give an operational semantics to these statements, building on Clight and the CPM semantics. 3.1

Syntax: Extending Clight

The extended statements for constructs, such as the one for the parallel con→ − s, have 4 parts in general: SPar specifies the kind of struct, SParidx nc pc rcs → − directive; nc, pc and rcs are construct-specific clauses that specify additional behaviors; s is the statement affected by the directive; lastly, the subscript idx is an index that uniquely identifies the construct. Concretely, line 2-10 in Figure 1 is encoded as SParidx 2 [] [] s, where idx is some unique index and s is the statement for line 3-10. We explain them in detail. In addition to SPar for the parallel directive, we define 4 core statements for directives in total: SFor for the for directive, SSingle for the single directive, and SBarrier for the barrier directive. The parallel, for, and single directives are lexically associated with the following statement (or block) and semantically affect that statement, and we encode the affected statement as the last argument s of SPar, SFor and SSingle. These directives and their associated statements form a construct. The barrier directive does not associate with a statement and forms a barrier construct on its own. A construct statement can have 0 or more clauses. The nc clause specifies the number of threads in the parallel construct5 . A privatization clause pc gives a list of variable names to privatize. Constructs that support reduction have a → − and a reduction clause rc is a pair of a reduction list of reduction clauses rcs, 5

In the OpenMP standard, the actual number of threads is determined by a number of factors at runtime; currently, we assume that the number is determined statically, but our semantics could be modified to follow the standard more closely.

A Formal Semantics of C with OpenMP Parallelism

7

identifier rid that specifies the operation for combining the reduction contributions, and a list of variables to be reduced—for example, at the end of a for loop that computes a sum in variable sum, we may sum every thread’s contribution to compute the final result using a reduction clause (+:sum). Both SPar and SFor support a privatization clause and a list of reduction clauses; SSingle supports privatization but not reduction. When directives with these clauses are executed, we generate runtime-only instructions SPriv, SPrivEnd, SRed that carry a mix of statically and dynamically recorded information about how to perform privatization and reduction; we discuss these further in Section 3.5. There are several places in the semantics of OpenMP where we need to know that statements executed by different threads are not merely equal but in fact the same syntactic occurrence of the statement: for instance, threads in a team synchronize at a barrier only if they have all reached the same barrier. For this purpose, we give every construct statement (SPar, SFor, SSingle, SBarrier) a unique integer index n. We also generate SBarriers at runtime to make implicit barriers explicit, and they need to be further distinguished with an optional statement s and a boolean b; we discuss these details in Section 3.4. 3.2

Synchronization with the Team Tree

As described in Section 2, the CPM models the execution of concurrent programs by tracking a collection of per-thread states and a single shared memory. For OpenMP, we need to track an additional kind of information: the hierarchical structure of spawned threads, which are organized into teams, and the states of their in-progress OpenMP operations. Since the team hierarchy in the program forms a tree (each team is spawned by a single parent thread, which may itself be part of a team), we organize OpenMP-specific state information into a tree that we call the team tree, denoted by T , which we include in program states alongside the thread pool P and memory m. The execution of sequential C code (rule Step-Clight) is not affected by the addition of the team tree, as regular per-thread execution is independent of OpenMP states. We define the team tree by defining its Nodes. Each node corresponds to a thread of execution. When a thread spawns a team, its node adds child nodes for the team’s threads, along with some team contexts that record OpenMP state common to the entire team. Formally: Definition 1 (Node and Team) A Node of a team tree is a tuple (t, tm) where t is a thread ID and tm is either some Team or ⊥. A Team is a tuple −−−→ (leader , pctx , ectx , mates) where leader stores the thread ID for the leader of the team (which is always the thread that spawns the team), pctx is the parallel context of the team, ectx is a team-executed context representing the currently −−−→ active team-executed construct6 or ⊥, and mates is a list of Nodes for the members of the team. 6

One team-executed context suffices because all threads in a team can be in at most one team-executed construct at a time: the OpenMP standard effectively requires that, inside a parallel region, team-executed contexts cannot be nested. From the

8

K. Du et al.

The program starts with the initial team tree (t1 , ⊥), containing a single Node for the initial thread t1 and no team. The parallel context ParCtxidx of a Team records the index idx of the parallel construct that spawned it; ectx exists if some member of the team is inside a team-executed construct, and records information specific to that construct. It has the form ForCtxidx w for a for construct, or SinCtxidx j for a single construct. We will explain the definition and the usage of the contexts when we introduce the semantics in the following sections. The thread that spawns a team becomes the leader of this team; it participates in this team as a new node with the same thread ID (therefore this new node is also a child of the original node). Spawned threads can also spawn teams themselves, resulting in nested teams. 7 Only the leaf node of i in a team tree T is immediately relevant to its execution, and we call this node the active node of i, denoted as T (i). T (i) is only defined if the active node for i is unique. In this section, we will describe the operations on team trees informally; formal definitions are in Figure 12. 3.3

Overview of the Semantics

Our semantic rules for the OpenMP constructs are shown in Figures 2 and 6. As described in the previous section, our step relation is on configurations of the form ⟨0, P, T , m⟩, where 0 is a thread schedule, P is a collection of per-thread states including control state (for example, the current Clight statement and continuation), local variables, and permissions, T is a team tree, and m is the shared memory. Each rule begins with a schedule of the form i·0, indicating that i is the next thread to execute, and then explains the effect on the configuration if i is executing one of the OpenMP directives (regular program steps do not affect the team tree, and so use the Step-Clight rule from Section 2 as is). In the rest of this section, we describe each of these rules in detail. Judgement and Notation Although OpenMP constructs are essentially concurrent, some can be described as local transitions of a single thread, together with synchronizations via the team tree T . This is expressed with the judgement h s || le || m 7−−−→ s′ || le ′ || m′ : it says a thread i updates its statement s and i,P,T

variable environment le (along with the global memory m) to s′ , le ′ (and m′ ), standard: “a team-executed region (for, single, barrier) may not be closely nested (nested in the same parallel region) inside a partitioned worksharing region (for or single)”. We implement the barrier construct as a single atomic operation, and all of our team-executed constructs have an implicit barrier at the end of the construct, so no thread can enter a new team-executed construct while some of its teammates are still executing the old one. 7 In this work, we only model programs that are executed by one device, and all synchronization is due to the OpenMP pragmas that we define. We do not model the teams construct, or the notion of a league of teams, and all threads are descendants of the initial thread.

A Formal Semantics of C with OpenMP Parallelism

9

SBRBidx ,s,r ≜ let sr := if r.1 = [] then SSkip else SBarrieridx ,false,s ; SRed r in sr ; SBarrieridx ,true,s Step-Parallel

→ − ∀j ∈ t .j ∈ /P M ′ ′ ′ → − − − r ≜ ( rc, le|→ s ≜ SPriv → x (s; SBRBidx ,SPar,r ) π i = πi ⊕ ( → − πj ) x ) j∈t D h i E − − i · 0, P i ::= ⟨SParidx nc → x → rc s, le, k⟩, πi , T , m → D h i E → − → − ′ ′ ′ ′ 0, P i ::= ⟨s , le, k⟩, πi , ∀j ∈ t . j ::= ⟨s , le, KStop⟩, πj , spawn_team(ParCtxidx , t )(T , i), m → − | t | = nc − 1

Step-Barrier

M M → − ′ t ≜ team_tids(T , i) T (i). ectx ̸= ⊥ ⇐⇒ s = SFor ∨ s = SSingle → − πj = → − πj j∈t j∈t D h i E → − i · 0, P ∀j ∈ t , j ::= ⟨SBarrieridx ,b,s , le j , kj ⟩, πj , T , m → D h i E → − ′ 0, P ∀j ∈ t , j ::= ⟨SSkip, le j , kj ⟩, πj , if b then end_ctx(s)(T , i) else T , m⟩

Step-Thread

h

′

′

′

s || le || m|πi 7−−−−→ s || le || m i,P,T h i h i ′ ′ ′ ′ ⟨i · 0, P i ::= ⟨s, le, k⟩, πi , T , m⟩ → ⟨0, P i ::= ⟨s , le , k⟩, perm(m ) , h(T , i), m ⟩

Step-For w ≜ partition (s) ′ ′′ ′ − − s ≜ set_stmt_to_partition(s, w(i)) r ≜ ⟨→ rc, le⟩ s ≜ SPriv → x (s ; SBRBidx ,SFor,r ) sync_ectx (ForCtxidx w) ′ − − SForidx → x → rc s || le || m 7−−−−−−−−−−−−−−−−→ s || le || m i

Step-Single

′ − s ≜ SPriv (if i = j then → x else []) ((if i = j then s else SSkip); SBarrieridx ,true,SSingle ) sync_ectx(SinCtxidx j) ′ → − SSingleidx x s || le || m 7−−−−−−−−−−−−−−−−→ s || le || m i

Fig. 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 Figure 2 lifts a single-thread step by thread i to the full configuration, writing back the updated s′ and le ′ to the thread pool P, updates T to h(T , i), and m to m′ . Thread i’s continuation k stays the same. Like Step-Clight, thread i can only step with m|πi , i.e. m equipped with thread i’s initial permission πi ; we then save perm(m′ ), the permission in the new memory m′ , as thread i’s new permission. Step-Parallel and Step-Barrier change the state of multiple threads and are not expressed − in this style. We abuse the le|→ x notation to mean the map le with the domain − restricted to → x. We explain the basic semantics of the constructs that enable parallelism and worksharing in Section 3.4. Privatization and reduction clauses can be attached to these constructs to fine-tune their behavior; their semantics are explained in Section 3.5.

10

K. Du et al.

3.4

1 2 3 4 5 6 7

Parallelism and Work-Sharing

#pragma omp parallel num_threads(5) { #pragma omp for for(int i = 0; i < 100; i++) { printf("%d\n", i); } }

Fig. 3: An OpenMP program with parallel and for constructs.

1 2 3 4 5 6

#pragma omp parallel num_threads(2) { #pragma omp single { printf("Before\n"); } printf("After\n"); }

7

Fig. 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 Figure 3, a team of 5 threads executes lines 2–6 in parallel. Thread i also participates in the team and becomes the primary thread of the team, so we only need to add nc −1 new threads. We add these threads both to the team tree T via the spawn_team operation and to the thread pool P, where we record each thread’s code, local environment, and permissions. At a first pass, the code executed by the spawned threads is (s; SBarriertrue,SPar ): each thread executes the body s of the parallel region, and then a barrier synchronizes all the threads in the team and ends the parallel region. For the permissions, all teammates split thread i’s original permissions arbitrarily— a given memory location may be written by a single thread in the team or read by all of them (but not both). In this case, the original permission πi is redistributed → − among the team (πi′ and πj′ for j ∈ t ). Two points further complicate this picture: privatization and reduction. Each thread wraps its code in a SPriv command that creates private copies of variables as specified in the SPar directive’s private clause. Furthermore, if the directive’s reduction clause is non-empty, the threads must execute additional commands (denoted by SBRB) to perform reduction at the end of the region. We discuss privatization and reduction in Section 3.5. The For Construct The for construct is the most common form of worksharing in OpenMP, distributing the iterations of a for loop across the threads in a team. For example, the program in Figure 3 distributes its loop to a team of 5 threads, each of which executes some portion of the loop in parallel. The program will still print each of 0 to 99 once, but in an arbitrary order8 determined by the partition of iterations and the order of parallel execution. 8

This loop body is safe to execute in parallel because the iteration variable i is made private; we explain this in more detail in the following sections.

A Formal Semantics of C with OpenMP Parallelism

11

The rule Step-For applies when a thread reaches a SFor pragma applied to the loop statement s. The OpenMP standard requires that s be in canonical loop nest form 9 , essentially restricting the syntax of the loop so that it is possible to compute the logical iterations at runtime by just looking at the initializer, increment, and condition statements of the associated loop. We then choose a partition w that maps thread ID to a list of iterations, so w(i) is the iterations for thread i. The partition w is arbitrary as long as these iterations combine to a permutation of the original iterations. The team must agree on a context ForCtx for the loop that includes w, guaranteeing that each thread uses the same partition. This is accomplished using the sync_ectx(ForCtxidx w) operation: if there is no ectx for its team in T , it is set to be ForCtxidx w; otherwise, if there is already some ectx set, sync_ectx is only defined if ectx = ForCtxidx w, essentially enforcing the team to agree on the same w. The thread then executes a modified version s′ of the loop, where the iterations have been restricted to its piece w(i) by modifying the initialization and test expressions, followed by a closing barrier. As with parallel, any privatization and reduction clauses in the for pragma are handled by SPriv and SBRB respectively. The Single Construct We also model the simpler work-sharing construct single, which says that only one thread in the team executes the associated code. For example, in Figure 4, exactly one thread prints “Before”, and 2 threads print “After”, and “Before” is always printed before any “After”. As with for, the threads must agree on a SinCtx by sync_ectx, but this time its only contents are the id j of the thread that will execute the code. Threads that are not chosen execute no instructions (SSkip) and privatize no variables ([]) in the region. The SSingle construct does not support reduction clauses, since only one thread performs computation in the region. Barriers The barrier construct creates an explicit barrier that blocks a thread until all threads in its team reach the barrier. For example, in Figure 5a, all 5 threads have to reach the barrier before any of them can proceed, so all “before”s will be printed before any “after”. When thread i takes a Step-Barrier, it first identifies its team members: Definition 2 The team of a thread i in a team tree T is the set of thread IDs of all the siblings of T (i) (including i), denoted as team_tids(T , i). 10 Our semantics formalizes requirements about the initializer, the condition, and the increment statements in the loop. The OpenMP specification imposes further requirements on the loop body: there must be no break or continue statements, and the iteration variable must not be modified during execution of the loop body, preventing partial or skipped execution of some iterations. Since this is a syntactic constraint, we assume that a parser has already implemented this check when it generates the ClightOMP language. 10 Notice a sibling node of T (i) is not necessarily active since it may spawn another team, but only the thread of the sibling node is in team_tids(T , i). 9

12 1 2 3 4 5 6

K. Du et al.

#pragma omp parallel num_threads(5) { printf("before\n"); #pragma omp barrier printf("after\n"); } (a) threads wait at a barrier

1 2 3 4 5 6

#pragma omp parallel num_threads(2) { int i = omp_get_thread_num(); if (i==0) { bar1(); } else { bar2(); } } (b) Threads in a team should enter barriers in the same order

Fig. 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 leader and 1 for the other thread, so two threads in a team arrive at different barriers and should be stuck according to the OpenMP specification. 12 Our semantics gives uniform treatment to both explicit barrier directives and the implicit barriers at the ends of regions (i.e., the barriers in SBRB generated by rules like Step-Parallel), and we index SBarrieridx,b,s with not just idx but an additional boolean b and an optional statement s (the directive that generates the implicit barrier, or ⊥ for an explicit barrier) to handle the subtle differences in their semantics. As shown in the rule Step-Barrier, a barrier can only execute when a full team of threads are all at the same barrier (i.e., a barrier with the same indices idx,b,s). Explicit barriers must not be placed inside team-executed regions, which we check via the team’s ectx; this requirement comes from the OpenMP specification and serves to rule out, e.g., the case where a barrier in the body of a shared loop is encountered a different number of times by threads executing a different number of iterations of the loop body. Further, if the barrier is the closing operation (b = true) for some construct s, it removes related context from T accordingly with end_ctx: for a for construct (s = SFor) or a single construct (s = SSingle), it removes the ectx; for a parallel construct (s = SPar), it removes the team (i.e. undo the effects of spawn_team). Finally, all threads in the team simultaneously move to the next statement, and may also freely exchange permissions within the team: for instance, a barrier may be used to separate a code segment in which a thread has exclusive Writable access to a variable from one in which Readable permission is shared across the whole team. An OpenMP thread number uniquely identifies a thread in a team. For thread i, the function omp_get_thread_num returns the index of node T (i) relative to its siblings. Note that this is different from a thread ID, which uniquely identifies a thread in the thread pool. 12 This program terminates for OpenMP implementations in GCC or Clang, and to the best of our knowledge, there are currently no tools that catch this issue. 11

A Formal Semantics of C with OpenMP Parallelism

3.5

13

Privatization and Reduction

As described in Section 1.1, OpenMP directives can have subtle effects on the semantics of variables within the affected regions. In particular, both parallel and for constructs can trigger privatization and reduction, according to the private clause pc and the reduction clauses rcs included in their directives. We model the semantics of these clauses as additional helper statements emitted at the start of each region, with arguments derived from both the syntactic clauses and the program’s runtime state. The rules are defined in Figure 6. Step-Priv

′ ′ − priv→ x ,i (le, m) = ⟨le , m ⟩

′ ′ → − SPriv − x s || le || m 7− → s; SPrivEnd le|→ x || le || m i

Step-Red

→ r = ⟨− rc , le o ⟩

Step-Priv-End end_privi,le o (le, m) = ⟨le ′ , m′ ⟩ SPrivEnd le o || le || m 7− → SSkip || le ′ || m′ i

− → t ≜ team_tid(T , i)

− → SRed r || le || m 7− −−− → SSkip || le || if leader(T , i) = i then red→ t ,− rc ,le o ,P (m) else m i,P,T

Fig. 6: Semantic rules: private, reduction. Supporting operations priv, end_priv and red are defined in Figure 13 in the appendix

Privatization By default, variables declared before a parallel region are shared among the threads in the region’s team: they are treated as memory locations that can be accessed by all threads (and access must be synchronized accordingly). However, sometimes it is useful for each thread in the team to have its own private copy of a shared variable. In the example in Figure 7, if x were a shared variable, the threads’ accesses to it would race; the intended behavior is instead that each thread uses its own copy of x, as indicated by the private clause in the parallel directive. Both parallel and for constructs can include private clauses; the iteration variable of a for construct is also implicitly privatized as mentioned in Section 3.4 (we assume that the parser has already added any implicitly privatized variables to the relevant private clauses). In Figure 7, if there were no private clause, variable x would be shared in the team in the parallel region, and updates to x on line 5 would race. With the private clause, a private copy of x is allocated for each thread in the team, so it is safe to update x on line 5, and on line 6 each thread’s x holds its own OpenMP thread number. After the parallel region, these private copies of x are deallocated, and the original x is again in scope. The execution of a region with a private clause is prefixed with a statement − − SPriv → x , where → x is the list of variables to be privatized. The rule Step-Priv − describes the semantics of privatization. For each private variable xk ∈ → x , we allocate a new location lk in the shared memory m which will hold the value of thread i’s private copy of xk , and set xk to refer to lk in i’s local environment. The initial value at lk is undefined, as if it were a newly declared variable (with

14

1 2 3 4 5 6

K. Du et al.

int x = 3; #pragma omp parallel private(x) num_threads(2) { // x uninitialized x = omp_get_thread_num(); printf("my thread number is %d\n", x); } // x=3

Fig. 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 le o containing the original memory locations of the variables − in → x . When we reach the SPrivEnd statement, we reverse the process, freeing each location allocated for a private variable and restoring the local environment − to the original locations of → x . Note that each thread in a team will separately − execute the SPriv instruction, allocating its own copies of the variables in → x; after all threads end privatization, each xk will once again refer to the same memory location in each thread. 1 2 3 4 5 6 7

int sum=0; #pragma omp parallel num_threads(2) { #pragma omp for reduction(+:sum) for(int i=1; i≤ 100; i++) { sum += i; } } printf("sum of the first hundred numbers is %d\n", sum);

Fig. 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 the shared variable. For example, in Figure 8, the loop iterations are divided between two threads, each summing a part of the 100 numbers. Each thread saves its running sum in an implicitly privatized sum variable during the for construct. When both threads are at the end of the for construct, the reduction clause says that the private copies of sum are combined with the original one with the operator +, producing the total sum. We assume that all reduction variables are declared to be private (the parser can add all reduction variables to the private clause of the same construct), so they are already processed by the SPriv statement for their region. The additional work of reduction occurs at the end of the region: if the region’s 13

OpenMP has rather detailed rules for determining the initial values of reduction variables, which we do not discuss here but are reflected in our semantics.

A Formal Semantics of C with OpenMP Parallelism

15

reduction clause is non-empty, then instead of a single barrier, SBRB emits a barrier, a reduction statement SRed, and another barrier14 . The first barrier synchronizes all threads in the team, ensuring that they have all finished the region, and transfers permissions for all their reduction variables to the leader. The SRed statement is executed only by the leader and performs reduction on all private copies of each reduction variable, folding the specified operation over their values and storing the result in the original variable. (For all non-leader threads, SRed is a no-op.) Finally, the last barrier forces all threads to wait until the reduction is complete before proceeding to any remaining code, and it also redistributes the team’s permissions. 3.6

Design Considerations

There are many different ways of translating the OpenMP specification document into operational semantics. Our semantics is aimed to uncover variable and synchronization errors, and so the following considerations are especially important: Barrier is the only operation that synchronizes running threads. An operational semantics is easiest to reason with when each step is performed by one thread, and concurrency can be expressed by the interleaving of steps of individual threads. Every one of our rules except Step-Barrier is local in this sense: each thread may enter a for or single region, or execute privatization or reduction, independently of all other threads, with coordination accomplished via the asynchronous sync_ectx (the first thread to enter a region sets the ectx, and the others read it). Only Step-Barrier requires that all threads in a team be at the same instruction and moves all threads forward simultaneously. Thus, all synchronization in an execution can be traced specifically to barrier operations (or to thread creation via Step-Parallel). Operations that can race are not atomic. If two operations can occur in either order, it is important that our semantics observe the resulting nondeterminism, which is hidden if the operations are both performed as part of a single step. For example, we could have combined Step-End-Priv and Step-Red-Leader into a single end-of-region step, but since both access privatized variables, this would obscure possible races between reduction and ending privatization. By separating them, our semantics identifies the need for a barrier between the two steps15 , and could identify possible races if, e.g., we implemented the nowait clause that removes the barrier at the end of a region. Another consequence of this separation is that there is no step that both synchronizes threads and accesses memory, which leads to the next point. 14 15

We do not support the no_wait clause that skips these implicit barriers. This synchronization is not explicitly mentioned in the OpenMP specification, but its absence leads to races in programs that should be well-defined, and both GCC and Clang place a barrier before reduction.

16

K. Du et al.

A thread must have permission to perform its memory accesses. Steps that access memory (such as privatization and reduction) only succeed if the thread performing them has the required permissions at the start of the step. This allows the permissions to serve their intended purpose of race detection: the fact that permissions are always consistent in an execution state is enough to guarantee the absence of data races. We discuss race-freedom further in Section 4.2. As a side note, we are also able to support the OpenMP critical construct by elaborating it to acquire and release of a dedicated lock, since lock operations are already supported by the CPM.

4

Properties of the ClightOMP Semantics

The ClightOMP semantics inherit from Clight and the CPM some safety properties that are implicitly proved as part of demonstrating an execution. Moreover, demonstrating an execution also guarantees that the execution is free of data races. 4.1

Invariants and Safety Properties

First, Clight’s semantics enforces memory safety: Theorem 1 (from CompCert). If a thread uses the value of a variable, then that variable has a defined value. If a thread step accesses memory, then that memory access is valid. So proving that a program (even a sequential one) can execute under our semantics implies that threads never use uninitialized variables, access unallocated or deallocated memory, access arrays out of bounds, etc. Second, the CPM enforces permission coherence before each step: each thread’s permissions must be consistent with each other thread’s, i.e., no two threads can have write access to the same location at the same time. Theorem 2 (from CPM). If an execution from the initial state of a program reaches a state ⟨0, P, T , m⟩, then the permissions of threads in P are coherent. This is most relevant to our semantics when we perform the sync operation: we may redistribute permissions freely within the team at team creation and at barriers, but the new distribution must always be coherent. This is useful for proving race freedom, as we will see in the next section. As a consequence of these properties, demonstrating an execution of a program under our semantics implies the absence of several categories of common bugs. Variable initialization, memory errors, and data races are responsible for many real-world errors in OpenMP programs [1], so even without proving specific properties of a program (e.g., functional correctness), showing that it executes according to ClightOMP makes it much more likely to be correct.

A Formal Semantics of C with OpenMP Parallelism

4.2

17

Race-Freedom

The CPM’s permissions are intended to guarantee race-freedom of any execution under its semantics, and its authors prove that at the x86-TSO level, successful executions contain no data races [6]. Our semantics enjoys a similar property at the C level, using the fact that every thread only performs memory operations that are allowed by its current permissions: Theorem 3 (Data race freedom). If an execution contains two conflicting events e1 and e2 on the same memory location, then e1 and e2 are synchronized. The proof is in Section F. Thus, any successfully terminating execution in our semantics has not encountered undefined behavior. This also justifies our use of a sequentially consistent memory model, since OpenMP specifies that race-free programs without weak-memory atomic directives (which we do not support) have sequentially consistent behavior.

5

Related Work

C Semantics and Concurrency. Our work builds on the Concurrent Permission Machine [6], which is part of an effort to modularly lift CompCert’s semantics and correctness proof to concurrency. Other approaches to adding concurrency to CompCert include CompCertTSO [18], which directly extends CompCert with the TSO memory model, and CASCompCert [8], which is similar to the CPM but works with memory footprints instead of permissions. CASCompCert’s semantics are simpler than the CPM’s and do not involve as much explicit permission management, but it requires that concurrency primitives be implementable as atomically executed blocks of ordinary C commands, which does not permit the team management involved in OpenMP directives. Two other major formalizations of C’s semantics are KC [7] and Cerberus [15,14]. The former does not include concurrency at all, but the latter does, and could also be extended with OpenMP support. While CompCert/the CPM has the advantage of connecting to a verified compiler, Cerberus has an associated model checking tool that is useful for detecting unusual concurrent behaviors. OpenMP Semantics and Verification. Atzeni and Gopalakrishnan [3] previously gave semantics to OpenMP for the purposes of defining a sound race detector. They also organize the thread hierarchy in a tree-like data structure similar to our team tree, with a different mechanism, offset-span label, to describe specific positions within the structure. However, their work is focused entirely on race detection: it elides the semantics of actual source programs, and models program execution as a stream of memory operations and concurrency events (e.g., parallel and barrier directives). Thus, there are several classes of OpenMP errors that are invisible to their semantics, including malformed control flow/region nesting and reading from uninitialized private variables. In fact, even the for construct is not explicitly modeled in their semantics, since its effects are entirely at the level of variables and control flow.

18

K. Du et al.

The CIVL concurrency verifer [16] supports verification of OpenMP programs, as well as other concurrency frameworks such as MPI and CUDA. It does so by translating OpenMP directives into concurrency primitives in CIVLC, a custom C extension with built-in concurrency operations. While CIVL-C has formal semantics and an associated verifier via SMT solvers, the translation of OpenMP to CIVL-C is part of CIVL’s trusted computing base. Our work provides a means to verify this translation by showing that the CIVL-C implementation of OpenMP is consistent with its source-level semantics.

6

Conclusion and Future Work

In this work, we have presented ClightOMP, a formal semantics for C programs with OpenMP directives. Our semantics extends the concurrent C semantics of the Concurrent Permission Machine with a team tree that tracks the states of threads spawned via OpenMP, and carefully accounts for the effects of privatization and reduction on local variables. This gives us a formal definition of the allowed behaviors of OpenMP C programs according to the OpenMP specification, and enables us to identify subtle, undesirable behaviors induced by incorrect annotations; in particular, we have shown that any execution in our semantics is data-race-free. Because most of the OpenMP logic is captured by changes to the team tree, our semantics are also fairly modular and could be reused, with minimal modification, to define OpenMP semantics for other languages (e.g., C++ or Fortran). We aim to further validate the consistency of ClightOMP semantics with the behaviors of actual OpenMP programs in two ways. First, we can test the semantics by proving that some executions of OpenMP programs have the same results in our semantics as their real-world implementations; second, we can implement a verified compiler of ClightOMP programs and test the compiled programs. We envision two main applications for this semantics: testing and verification. On the testing side, we aim to develop an executable version of our semantics that could serve as a reference interpreter for OpenMP programs. An executable semantics would allow us to test our semantics against actual OpenMP implementations, potentially uncovering bugs in either our semantics or the implementations. It could also serve as a basis for property-based testing (PBT), automatically verifying the correctness properties of OpenMP programs in a sound manner grounded in our semantics. The PBT framework would be useful for detecting race conditions and runtime errors in OpenMP programs. On the verification side, tools that automatically parallelize sequential programs by instrumentation with OpenMP pragmas [17,12,11] lack a semantic preservation guarantee. To aid this, we can prove that a program is correctly instrumented with OpenMP directives by proving that its allowed behaviors under our semantics are a subset of those of the original sequential program (i.e., refinement). We are also interested in using our semantics to verify a compiler that implements OpenMP directives with standard concurrency primitives: the

A Formal Semantics of C with OpenMP Parallelism

19

CPM already has a (mostly) proved-correct compiler to assembly, so by translating OpenMP directives into CPM spawn and lock operations, we can obtain a verified compiler for C+OpenMP. In the longer run, we note that the CPM was developed as backing for the Verified Sofware Toolchain (VST) [2], a tool for verifying functional correctness of C programs; our semantics could serve as the basis for an extension of VST to verify OpenMP programs as well, including those with more complex behavior that may not exactly match the behavior of sequential programs (at least locally).

20

K. Du et al.

A

ClightOMP Syntax

Identifier: x Integers: n ::= Z Booleans: b ::= true | false rid ::= + | * | & | | | ∼ |

&& | || | max | min num_thread clause

nc ::= n pc ::= x

∗ ∗

rc ::= (rid , x ) r

::= (rc , le)

s

::= cs

privatization clause

private(x*)

reduction clause

reduction(rid:x*)

data for reduction

∗

|

reduction_identifier

Clight Stmt

SParn nc pc rc s parallel construct ∗

#pragma omp parallel

|

SForn pc rc s

for construct

#pragma omp for

|

SSinglen pc s

single construct

#pragma omp single

|

SBarriern,b,s

barrier construct

#pragma omp barrier

|

SPriv pc s

start a privatization scope

|

SPrivEnd le

end of a privatization scope

|

SRed r

reduction

∗

Fig. 9: ClightOMP Syntax. SPriv, SPrivEnd, SRed are generated at runtime, and le stores runtime values.

B

Nested Parallel Region

Figure 11 depicts the team tree states in a possible execution of the program from Figure 10. The program starts with a single thread t1 , just like a sequential C program, and the corresponding initial team tree, as depicted in Figure 11(a). The subscript i of an OpenMP thread state denotes the thread ID, and the superscript indicates the level of nesting in a parallel region, or init to specify a freshly initialized node. When thread t1 reaches the first parallel construct on line 2, it starts a new team that executes the code associated with this construct (lines 3–9). As depicted in Figure 11(b), the parallel construct on line 2 starts a new parallel region, triggering spawn_team that adds a new team of two nodes of thread IDs t1 , t2 (along with some team context that is not shown here). The new node s2t1 supersedes the original node s1t1 for thread t1 , and starts with its own initial (empty) stack of OpenMP contexts, representing the fact that “t1 as part of the team {t1 , t2 }” is a different logical entity from “t1 as the

A Formal Semantics of C with OpenMP Parallelism

21

initial thread”. When the team ends at line 9, although t2 will terminate and t1 will continue to execute, both nodes in the team are removed from the tree by despawn_team; t1 will return to OpenMP state s1t1 , its state from before the parallel construct (Figure 11(d)). Nested parallel constructs create nested parallel regions. As depicted in Figure 11(c), when t1 of the team {t1 , t2 } meets the parallel construct on line 4 in Figure 10, it spawns a new team with the same rules, while t2 has not reached line 4 yet. When t2 reaches line 4, it likewise spawns a new team {t2 , t5 , t6 } for parallel region III for some new threads t5 , t6 , and the execution of this team does not interfere with the other team {t1 , t3 , t4 }.

// program starts with one thread t1 (Parallel Region I) #pragma omp parallel num_threads(2) // (Parallel Region II) { // a team of 2 threads {t1, t2} is created #pragma omp parallel num_threads(3) //(Parallel Region III) { // t1 creates a team of {t1, t3, t4}, t2 creates {t2, t5, t6} do_something } // the teams {t1, t3, t4}, {t2, t5, t6} ends here, the primary // thread of each team t1 and t2 resumes to parallel region II } // the team {t1,t2} ends // t1 resumes in the outmost parallel region I

1 2 3 4 5 6 7 8 9 10

Fig. 10: An OpenMP program with nested parallel regions I, II and III, marked with dotted squares.

(a) (I)

(II)

(b)

(c)

1 𝑠𝑡1

𝑖𝑛𝑖𝑡 𝑠𝑡1

1 𝑠𝑡1

ParCtx1

ParCtx1 𝑖𝑛𝑖𝑡 𝑠𝑡1

(d)

𝑖𝑛𝑖𝑡 𝑠𝑡2

1 𝑠𝑡1

All team despawned on line 9, only the initial thread t1 remains. 2 𝑠𝑡1

2 𝑠𝑡2

Team spawned on line 2

(III)

ParCtx2

𝑖𝑛𝑖𝑡 𝑠𝑡1

𝑖𝑛𝑖𝑡 𝑠𝑡3

𝑖𝑛𝑖𝑡 𝑠𝑡4

Team spawned on line 4

Fig. 11: Team tree T evolution for an execution of the program in Figure 10. Blue nodes are active; grayed out ones are inactive. (I), (II), and (III) refer to the regions in Figure 10. Each team also has an associated parallel context.

22

C

K. Du et al.

Team Tree Operations

Node operations of the form op ≜ ⟨r, f ⟩ is a pair of two functions r, f : Node → Node, in which f updates a node, and r finds the node that needs to be updated with respect to the input node: id is the identity and parent finds the parent node. n in the when clause binds to the node before applying op, and op is defined only if the when clause holds. − → − → spawn_team(pctx , t ) ≜ id, λn, n. tm ::= ⟨pctx , ⊥, new_nodes( t )⟩ when n. tm = ⊥ despawn_team(idx ) ≜ parent, λn, n. tm ::= ⊥ when n. ectx = ⊥ ∧ n. pctx = ParCtxidx ∧ ∀ n′ ∈n. mates, n′ . tm = ⊥ sync_ectx(ectx ) ≜ parent, λn, n. ectx ::= ectx when n. ectx = ⊥ ∨ n. ectx = ectx pop_ectx() ≜ parent, λn, n. ectx ::= ⊥ when n. ectx ̸= ⊥ end_ctx(idx , s) ≜ if s = SFor ∨ s = SSingle then pop_ectx else despawn_team(idx ) Tree operations op(T , i) on a tree T and a thread ID i, lifted from node operations with the same name. op to the right of ≜ binds to the node operations: op(T, i)

≜ op .1(T (i)) ::= op .2(op .1(T (i))) − → where op ∈{spawn_team(pctx , t ), despawn_team(idx ), sync_ectx(ectx ), pop_ectx(), end_ctx(idx , s)} leader(T , i) ≜ Thread ID of the leader of the team of i team_tids(T , i) ≜ Thread IDs of all teammates in the team of i

Fig. 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: [t ;t ;...;t ]

k #j 0 1 fj ≜ftk ◦ · · · ◦ ft1 ◦ ft0 where ∀j ∈ [t0 ; t1 ; . . . ; tk ], fj : T → T h i d [k0 ; . . . ; kn ] ::= [v0 ; . . . ; vn ] ≜d[k0 ::= v0 ] . . . [kn ::= vn ] → − → − → − f ( t ) ≜ map f t where f : T → T, t : List T

The privatization operation priv takes the local variable environment and − memory right before privatization, allocates private copies of → x in m, and updates le. The end of privatization operation end_priv frees variable names in leo , and restores local variable environment for these privatized variables. The → − reduction operation red gathers contributions in threads t , adds them to the original variable (by looking up the original local variable environment le o before privatization).

A Formal Semantics of C with OpenMP Parallelism → ′ − − → − (le, m) ≜ let ⟨m , l ⟩ := m. alloc (ctypes ( x )) in priv→ x ,i

23

le

− → → ⟨le[− x ::= l ], m′ ⟩ end_privi,le o (le, m) ≜ foldr λ x. let m′ := m. free (le(x)) in ⟨le[x ::= le o (x)], m′ ⟩ ⟨le, m⟩ dom(le o ) 
 − → − red_one_var→ in t ,rop,x,vo ,P (m) ≜ let v := map λ t. m (P(t). le)(x)

let v ′ := foldr λ a b. eval_expr(EBinOp rop b a)

→ vo − v in

′

m[lo ::= v ] − → − red_one_clause→ t ,rc,leo ,P (m) ≜ let (rop, x ) := rc in − →

− #xs x red_one_var→ t ,rop,x,m(leo (x)),P (m) − →

− − − red→ (m) ≜ #rcs → rc red_one_clause→ t ,rcs,le t ,rc,leo ,P (m) o ,P

Fig. 13: Supporting functions for privatization and reduction. P(t). le returns the local variable environment of the thread state P(t). alloc , free allocates and frees a chunk of memory; ctypes looks up the Clight types of variables; eval_expr evaluates a Clight expression to a value. These are defined as in CompCert. dom returns the domain of a map as a list.

E

An Example ClightOMP Execution

We demonstrate how a program executes in our semantics in Section E. We show the program on the left, and each line’s corresponding active threads on the right. The program begins with an initial thread t1 in the thread pool and an initial team tree T . When t1 executes the parallel pragma on line 3 with the rule Step-Parallel, it forks another thread t2 and makes a new team {t1 , t2 }. At this point, the variable name r in both threads refers to the same variable, and they can read r concurrently. Then t1 and t2 each enter the for construct individually with the rule Step-For: the associated Step-Priv privatizes the reduction variable r and initializes it to 0. Each thread is assigned part of the loop iterations (the assignment is set in the ForCtx when the first thread reaches the for pragma), and running these iterations updates r to be n in t1 and m in t2 by the end of the loop. The first thread reaching line 10 is then paused at the initial barrier of SBRB, until the other thread reaches line 10 and triggers StepBarrier, and t2 gives its permission on the original variable r to t1 . Then each thread executes SRed, which in t2 does nothing and in t1 combines the threads’ contributions n, m with the original value 0, setting the original version of r to 0 + n + m. After another barrier at the end of SBRB, the ForCtx’s lifetime ends and the threads each execute SPrivEnd, deallocating their private copies of r and returning the name r to refer to the original version. Therefore, after

24

K. Du et al.

they exit the for construct, both threads will execute line 11 and print the same value n + m. Eventually they reach the end of the parallel construct on line 13, where the SBRB ends the team, removes the team’s contexts and nodes from the team tree, and transfers all of t2 ’s permissions to r to t1 (so now t1 has full permissions). Finally, the program ends with just t1 in the thread pool and a node for t1 in T , and we conclude that the program terminates successfully.

1

int r = 0;

𝑟↦ 0 𝑡

2 3 4 5 6 7 8 9 10 11

12 13

SPar

#pragma omp parallel num_threads(2) { // r is shared variable #pragma omp for reduction(+:r) for(...) { // r is privatized r+=... } printf("%d\n",r); //prints n+m twice ... }

𝑟↦ 0 𝑡

𝑡

ParCtx

SFor SFor

𝑟↦ 0 𝑟 ↦0

ForCtx

𝑟↦ 0 𝑟 ↦ 0 loop iterations

loop iterations

𝑟↦ 0 𝑟 ↦ 𝑛

𝑟↦ 0 𝑟 ↦ 𝑚

𝑟 ↦ 𝑛+𝑚 𝑟 ↦ 𝑛

𝑟 ↦ 𝑛+𝑚 𝑟 ↦ 𝑚

SBRB

SPrivEnd

SPrivEnd

𝑟 ↦ 𝑛+𝑚

𝑟 ↦ 𝑛+𝑚

printf

printf

SBRB

𝑟 ↦ 𝑛+𝑚

14 15

𝑟↦ 0

// program ends

SPrivEnd

𝑟 ↦ 𝑛+𝑚

SPrivEnd

(halts)

Fig. 14: An OpenMP program. Fig. 15: The execution flow and liftime of the team contexts. Each cell contains a thread’s local view to the memory, as well as the permissions annotated as subscripts: R for Readable, and F for Freeable.

F

Data Race Freedom

We prove that any ClightOMP execution is race-free. We begin by defining the memory and synchronization events produced by a ClightOMP execution. A ClightOMP step that accesses memory emits a list of CompCert memory events; a ClightOMP step that performs synchronization emits a synchronization event. Figure 16 shows the events emitted by each step. Per-thread Clight steps and Step-Priv/Step-Priv-End/Step-Red-Leader/Step-Red-NotLeader emit a sequence of memory events corresponding to their memory operations, each indexed by the thread number i that runs the step and the accessed memory location l. Specifically, Step-Priv emits an Alloc event for each memory allocation and Step-Priv-End emits corresponding Free events;

A Formal Semantics of C with OpenMP Parallelism

25

(CompCert) MemEv ≜ Alloci l | Freei l | Readi l | Writei l − → − → SyncEv ≜ Pari t | Bar t Event ≜ MemEv | SyncEv

Step-Clight in thread i list of MemEvi privatization/reduction steps in thread i list of MemEvi − → − → Step-Parallel in thread i spawning t [Pari t ] − → − → Step-Barrier synchronizing t [Bar t ] other steps []

Fig. 16: ClightOMP memory events emitted by a step.

Step-Red-Leader emits Read events for reading the private copies of the reduction variable, followed by a Write event for updating the original copy. → − Step-Parallel emits an parallel event Pari t that synchronizes thread i → − with the spawned threads t . Step-Barrier emits a barrier event that syn→ − chronizes among the team t . We define a labeled version of our semantics → − e

⟨i · 0, P, T , m⟩ −→ ⟨0, P ′ , T ′ , m′ ⟩ where each step is labeled with the events it emits; then the event trace of an execution is the concatenation of all events emitted at each step. As is standard, we define a data race as a pair of conflicting memory events (i.e., events to the same location that are not both Reads) that are not ordered via a happens-before relation [9]. First, we need to define the happens-before relation: − Definition 3 (happens-before) Consider a list → e of events and two events → − → − e , e ∈ e where i < j are indexes to e . Then e happens before e , written i

j

i

j

ei <hb ej , if: – ei and ej are from the same thread, or → − → − – ei is Par t and the thread of ej is in t , or → − → − – one of ei and ej is Bar t and the thread of the other is in t , or – there is another event ek such that ei <hb ek and ek <hb ej . We observe that if ei <hb ej , then ei also happens before any following events by ej ’s thread; in fact, when two threads synchronize, all previous events by the first thread happen before all following events of the second thread. This makes it useful to talk about an event synchronizing with a thread, rather than simply with another event. Definition 4 (synchronizing with a thread) An event ei synchronizes with − − a thread t in a trace → e if for any event et by t, if we extend → e with a new trace → −′ → −′ → − e including et , then ei <hb et in e ++ e .

26

K. Du et al.

We can now begin to prove race-freedom. Intuitively, we can trace a permission throughout an execution: Writable permission flows forward to all threads that hold at least Readable permission for the rest of the execution, and Readable permission flows forward to some thread that holds at least Readable permission for the rest of the execution. We now formalize and prove this intuition in terms of event synchronization. Lemma 1 (Read synchronization). Suppose we have an execution ending in a state st whose trace contains an event e = Readi l, and l is not deallocated in st, i.e., there is some thread that has some permission to l in st. Then there is some thread j such that 1) j has at least Readable permission to l in st, and 2) e synchronizes with j in the trace. Proof. By induction on the execution. In the base case, the execution consists of → − e − a single step st −→ st where Read l ∈→ e . A thread only performs operations it 0

i

has permissions to, and steps that perform Reads do not change permissions, so thread i still has Readable permission to l in st and Readi l synchronizes with i. In the inductive case, we have an execution ending in a state st with a e′

thread j as described, and we consider a next step st −→ st ′ . If j still has Readable permission to l in st ′ , then we are finished. If it does not, then e′ must be emitted from a synchronization operation that changed j’s permissions. Whether this operation was a Par or Bar, it synchronized with a set of threads → − t whose new permissions in st ′ sum to the same result as the sum of the source permissions in st, which included j’s Readable permission to l. Thus, there must → − be at least one thread k ∈ t that has at least Readable permission in st ′ , and since e synchronized with j and e′ synchronized j with k, e now synchronizes with k in the extended trace. Lemma 2 (Write synchronization). Suppose we have an execution ending in a state st whose trace contains an event e = Writei l (or Alloc or Free). Then for all threads j that have at least Readable permission to l in st, e synchronizes with j in the trace. Proof. By induction on the execution. In the base case, the execution consists → − e − of a single step st −→ st where e ∈ → e . If e is a Write or Free then thread i 0

must have had at least Writable permissions to l in st 0 , so by coherence no other thread had Readable permissions to l; if e is Alloc then its location must have not been allocated in st 0 , so i is the only thread with permissions to l in st. In either case, i is the only thread in st with at Readable permission to l, and e synchronizes with i since they are in the same thread. In the inductive case, we have an execution ending in a state st with threads e′

synchronized with e as described, and we consider a next step st −→ st ′ and a thread j with at least Readable permission to l in st ′ . If j had Readable permission to l in st, then we are finished. If it did not, then e′ must be a synchronization operation that changed j’s permissions. Whether this operation was a Par or → − Bar, it synchronized a set of threads t whose old permissions in st summed to

A Formal Semantics of C with OpenMP Parallelism

27

a result that included j’s new Readable permission to l. Thus, there must be at → − least one thread k ∈ t that had at least Readable permission in st, and since e synchronized with k and e′ synchronized k with j, e now synchronizes with j in the extended trace. These dual lemmas show that read or write/alloc/free events are always synchronized in some way with threads that hold Readable permissions after them. We can use this to prove data race freedom: Theorem 4 (Data race freedom). If an execution’s trace contains two conflicting events e1 and e2 , then e1 <hb e2 . Proof. By induction, it suffices to consider the case where e2 is produced by the last step of the execution, st → st ′ , and the execution up through st is race-free. Let t2 be the thread of e2 . Since e1 and e2 conflict, they are on the same location l and either e1 or e2 is a write/alloc/free. In the case where e1 is a write, t2 has at least Readable permission to l (since e2 must be at least a read), and so by lemma 2 e1 synchronizes with t2 and thus e1 <hb e2 . In the case where e1 is a read, l is still allocated in st (since we perform e2 on it16 ), so by Lemma 1 there must be some thread j in st with at least Readable permission to l such that e1 synchronizes with j. But we know that e2 must be either a Write or a Free, and in either case t2 must have at least Writable permission to l. By coherence, this means that no other thread has Readable permission to l, so the thread j must be exactly t2 ; once again, e1 synchronizes with t2 and thus e1 <hb e2 . Thus, any execution in our semantics is necessarily race-free.

16

Note that Clight never reallocates freed locations, so we do not need to worry about the case where e2 Allocs l after e1 reads l.

28

K. Du et al.

References 1. Ahmmed, J., Mahmud, Q.I., Shim, J., Li, L., Jannesari, A., Cohen, M.B.: Differential testing for sequential to parallel transformations. In: Proceedings of the 9th International Workshop on Software Correctness for HPC Applications. Correctness ’25 (2025) 2. Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press (2014), http://www.cambridge.org/de/academic/ subjects/computer-science/programming-languages-and-applied-logic/ program-logics-certified-compilers?format=HB 3. 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 4. Besson, F., Blazy, S., Wilke, P.: A concrete memory model for compcert. In: International Conference on Interactive Theorem Proving. pp. 67–83. Springer (2015) 5. Board, O.A.R.: OpenMP Application Programming Interface. https://www. openmp.org/wp-content/uploads/OpenMP-API-Specification-6-0.pdf (2024) 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) 7. Ellison, C., Rosu, G.: An Executable Formal Semantics of C with Applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles 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 8. Jiang, H., Liang, H., Xiao, S., Zha, J., Feng, X.: Towards certified separate compilation for concurrent programs. In: Proceedings of the 40th ACM SIGPLAN 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.org/10. 1145/3314221.3314595 9. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (Jul 1978). https://doi.org/10.1145/359545. 359563, https://doi.org/10.1145/359545.359563 10. 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 11. Mahmud, Q.I., TehraniJamsaz, A., Ahmed, N.K., Willke, T.L., Jannesari, A.: Contraph: Contrastive learning for parallelization and performance optimization. In: Proceedings of the 39th ACM International Conference on Supercomputing. pp. 596–610 (2025) 12. 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 zeroshot code parallelization using llms. 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). pp. 11821–11841 (2025) 13. 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

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 15. 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. SIGPLAN Not. 51(6), 1–15 (Jun 2016). https://doi.org/10.1145/2980983.2908081, https://doi.org/10.1145/2980983.2908081 16. 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 verification language. In: SC ’15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. pp. 1–12 (2015). https://doi.org/10.1145/2807591.2807635 17. Tehrani, A., Bhattacharjee, A., Chen, L., Ahmed, N.K., Yazdanbakhsh, A., Jannesari, A.: Coderosetta: Pushing the boundaries of unsupervised code translation for parallel programming. Advances in Neural Information Processing Systems 37, 100965–100999 (2024) 18. Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60(3), 22:1–22:50 (Jun 2013). https://doi.org/10.1145/2487241.2487248, http:// doi.acm.org/10.1145/2487241.2487248