Correct program parallelisations

As mentioned above, in this paper we consider a frequently used subset of OpenMP constructs, using only the following pragmas: omp parallel, omp for, omp simd, omp for simd, omp sections, and omp single, as well as all allowed clauses. We illustrate these OpenMP features by means of examples. For full details on OpenMP, we refer to [20]. Later, Sect. 4 shows how programs in this subset are encoded into our core parallel programming language, and Sect. 8 shows how to verify that these programs can safely be parallelised, after the user has added the necessary program contracts.

In OpenMP, all variables which are not local to a parallel region are considered as shared by default unless they are explicitly declared as private (using the private clause) when they are passed to a parallel region.

Since OpenMP 4.0, support for the single instruction multiple data (SIMD) execution model has been added to the OpenMP standard. The SIMD execution model is a well-known technique to speed up vector arithmetics, specifically in scientific applications.

Our program specification language is based on permission-based separation logic, combined with the look-and-feel of the java modeling language (JML) [18]. In this way, we exploit the expressiveness and readability of JML, while using the power of separation logic to support thread-modular reasoning. We briefly explain the syntax and semantics of the permission-based separation logic formulas and how they extend the standard JML-program annotations in first-order logic.

Syntax Threads hold permissions to access memory locations. Permissions are encoded by fractional values, as introduced by Boyland [9]: any fraction in the interval \((0, 1)\) denotes a read permission, while 1 denotes a write permission. Permissions can be split and combined, but soundness of the logic ensures that for every memory location the total sum of permissions over all threads to access this location does not exceed 1. This guarantees that if the permission specifications can be verified, the program is data-race-free. The set of permissions that a thread holds are typically called its resources.

Formulas F in our program specification language are built from first-order logic formulas b, permission predicates \({\textsf {Perm}(e_1,e_2)}\), conditional expressions (\(\cdot ?\cdot :\cdot \)), separating conjunction \(\mathop {\star }\), and universal separating conjunction \(\bigstar \) over a finite set I. The syntax of formulas is formally defined as follows:where b is a side-effect free Boolean expression, e is a side-effect free arithmetic expression, [.] is a unary dereferencing operator—thus [e] returns the value stored in the address e in shared memory—v ranges over variables and n ranges over numerals. We assume the first argument of the \({\textsf {Perm}(e_1,e_2)}\) predicate is always an address and the second argument is a fraction. For convenience, we often use the keyword read instead of an explicit fraction to specify an arbitrary read permission, and the keyword write instead of 1 to denote a write permission.

We use the array notation a[e] as syntactic sugar for \([a+e]\) where a is a variable containing the base address of the array a and e is the subscript expression; together they point to the address \(a+e\) in shared memory.

Semantics Our semantics mixes concepts of implicit dynamic frames [25] and separation logic with fractional permissions, which makes it different from the traditional separation logic semantics and more aligned towards the way separation logic is implemented using traditional first order logic tooling. For further reading on the relationship between separation logic and implicit dynamic frames, we refer to the work of Parkinson and Summers [22].

To define the semantics of formulas, we assume the existence of the following domains: \(\textsf {Loc}\), the set of memory locations, \(\textsf {VarName}\), the set of variable names, \(\textsf {Val}\), the set of all values, including memory locations, and \(\textsf {Frac}\), the set of fractions ([0, 1]).

We define memory as a map from locations to values \(h:\textsf {Loc}\rightarrow \textsf {Val}\). A memory mask is a map from locations to fractions \(\pi : \textsf {Loc}\rightarrow \textsf {Frac}\) with unit element \(\pi _0: l \mapsto 0\) with respect to the point-wise addition of heap masks. A store is a function from variable names to values: \(\sigma : \textsf {VarName} \rightarrow \textsf {Val}\).

Formulas can access the memory directly; the fractional permissions to access the memory are provided by the \(\mathsf {Perm}\) predicate. A strict form of self-framing is enforced, meaning that the Boolean formulas expressing the functional properties in pre- and postconditions and invariants should be framed by sufficient resources (i.e. there should be sufficient access permissions for the memory locations that are accessed by the Boolean formula, in order to evaluate this formula).

The semantics of an expression e depends on a store \(\sigma \), a memory h, and a memory mask \(\pi \) and yields a value: \(\sigma ,h,\pi \mathop {[e\rangle }v\). The store \(\sigma \) and the memory h are used to determine the value v, and the memory mask \(\pi \) is used to determine if the expression is correctly framed, i.e. sufficient access permissions are available. For example, the rule for array access is:where \(\sigma (a)\) is the initial address of array a in the memory and i is the array index that is the result of evaluating of index expression e. Apart from the check for correct framing as explained above, the evaluation of expressions is standard and we do not explain it any further.

The semantics of a formula F, given in Fig. 6, depends on a store, a memory, and a memory mask and yields a memory mask: \(\sigma ,h,\pi \mathop {[F\rangle }\pi '\). The given mask \(\pi \) denotes the permissions by which the formula F is framed. The yielded mask \(\pi '\) denotes the additional permissions provided by the formula. Thus, a Boolean expression is valid if it is true and yields no additional permissions, (rule Boolean), while evaluating a \(\mathsf {Perm}(e_1, e_2)\) predicate yields additional permissions to the location, provided the expressions \(e_1\) and \(e_2\) are properly framed (rule Permission). Note that evaluation of expression \(e_1\) results in a location \(l\), while evaluation of expression \(e_2\) results in a fraction f. The rule checks that the permissions already held on location \(l\) plus the additional fraction \(f\) does not exceed 1. The rules for evaluation of a conditional formula are standard (rules Cond 1 and Cond 2). We overload standard addition \(+\), summation \(\varSigma \), and comparison operators to be, respectively, used as pointwise addition, summation and comparison over the memory masks. These operators are used in the rules SepConj and USepConj. In the rule SepConj, each formula \(F_1\) and \(F_2\) yields a separate memory mask, \(\pi '\) and \(\pi ''\), respectively, where the final memory mask is calculated by pointwise addition of two memory masks, \(\pi ' + \pi ''\). The rule checks if \(F_1\) is framed by \(\pi \) and \(F_2\) is framed by \(\pi +\pi '\). Note that since \(F_2\) is framed by \(\pi +\pi '\), this implicitly guarantees that the permissions per location never exceed 1. Finally, the rule USepConj extends the similar evaluation by quantifying over a set of formulas conjoined by the universal separating conjunction operator. Again, rule USepConj checks that the permission fractions on any location in the memory cannot exceed 1.

Finally, a formula F is valid for a given store \(\sigma \), memory h and memory mask \(\pi \) if starting with the empty memory mask \(\pi _0\), the required memory mask of F is less than \(\pi \):

Figure 8 presents the PPL syntax. The basic building block of a PPL program is a block. Each block has a single entry point and a single exit point. Blocks are composed using three binary composition operators:The entry block of the program is the outermost block. Basic blocks are:where \({\textsf {N}} \) is a positive integer variable that denotes the number of parallel threads, i.e. the block’s parallelisation level, \({\textsf {S}}\) is a sequence of statements and \({\textsf {V}}\) is a sequence of guarded assignments \(b \Rightarrow \textsf {assg} \).

In the grammar, we define a vectorised block at a different level than the other basic blocks, because this allows us to define the semantics in a more convenient way, while it does not prevent us from writing programs such as the parallel or fusion composition of a parallel and a vectorised block.

We assume a restricted syntax for fusion composition such that its operands are parallel basic blocks with the same parallelisation levels. This is checked by an extra well-formedness condition over PPL programs. Each basic block has a local read-only variable \(\textsf {tid} \in \mathsf {[0..{\textsf {N}})} \) called thread identifier, where \({\textsf {N}} \) is the block’s parallelisation level. We (ab)use the term iteration to refer to the computations of a single thread in a basic block. So a parallel or vectorised block with parallelisation level \({\textsf {N}}\) has \({\textsf {N}}\) iterations. For simplicity, but without loss of generality, threads have access to a single shared array which we refer to as heap. We assume all memory locations in the heap are allocated initially. A thread may update its local variables by performing a local computation (\(v\,{:}{=}\,e\)), or by reading from the heap (\(v\,{:}{=}\,\textsf {mem}(e)\)). A thread may update the heap by writing the value of one of its local variables to it (\(\textsf {mem}(e){:}{=}\,v\)). For the arrays, we use notation a[e] as syntactic sugar for [a+e] where a is a variable containing the base address of the array a and e is the subscript expression.

The behaviour of PPL programs is described using a small step operational semantics. For a convenient and understandable definition, the operational semantics is defined in several layers, as defined below. Throughout, we assume existence of the finite domains:We write to concatenate two statement sequences ( ).

Program State To define the program state, we use the following definitions.

We model the program state as a triple of block state, program store and heap and thread state as a pair of local state and heap \((\textsf {LS},h)\). The program store is constant within a block and it contains all global variables (e.g. the initial addresses of arrays).

BlockState We distinguish various kinds of block states: an initial state \(\textsf {Init}\), composite block states \(\textsf {ParC}\) and \(\textsf {SeqC}\), a state in which a parallel basic block should be executed \(\textsf {Par}\), a local state \(\textsf {Local} \) in which a vectorised or a sequential basic block should be executed, and a terminated block state \(\textsf {Done}\).

The \(\textsf {Init}\) state consists of a block statement \({\mathcal {P}}\). The \(\textsf {ParC}\) state consists of two block states, while the \(\textsf {SeqC}\) state contains a block state and a block statement \({\mathcal {P}}\); they capture all the states that a parallel composition and a sequential composition of two blocks might be in, respectively. The basic block state \(\textsf {Par}\) captures all the states that a parallel basic block \(\textsf {Par}\) (\({\textsf {N}}\)) \({\textsf {S}}\) might be in during its execution. It contains a mapping \(\mathbb {LS} \in \mathsf {[0..{\textsf {N}})} \rightarrow \textsf {LocalState} \), which maps each thread to its local state, to model the parallel execution of the threads. There are three kinds of local states: a vectorised state \(\textsf {Vec}\), a sequential state \(\textsf {Seq}\), and a terminated sequential state \(\textsf {Done}\).

The \(\textsf {Vec}\) block state captures all states that a vectorised basic block \(\textsf {Vec}\) (\({\textsf {N}} \)) \({\textsf {V}}\) might be in during its execution. It consists of \(\varSigma \in \mathsf {[0..{\textsf {N}})} \rightarrow \textsf {PrivateMem} \), which maps each thread to its private memory, the body to be executed \({\textsf {V}}\), a private memory \(\sigma \), and a statement \({\textsf {S}}\). As vectorised blocks may appear inside a sequential block, keeping \(\sigma \) and \({\textsf {S}}\) allows continuation of the sequential basic block after termination of the vectorised block. To model vectorised execution, the state contains an auxiliary set \({\textsf {E}} \subseteq \mathsf {[0..{\textsf {N}})} \) that models which threads have already executed the current instruction. Only when \({\textsf {E}}\) equals \(\mathsf {[0..{\textsf {N}})}\), the next instruction is ready to be executed. Finally, the \(\textsf {Seq}\) block state consists of private memory \(\sigma \) and a statement \({\textsf {S}}\).

To simplify our notation, each thread receives a copy of the program store as part of its private memory when it initialises. This is captured in rules Init Par and Init Seq (Fig. 11), where the local store \(\gamma \) is passed as an argument to the Seq block state.

Operational Semantics The operational semantics is defined as a transition relation between program states: \(\rightarrow _{p} \subseteq (\textsf {BlockState} \times \textsf {Store} \times \textsf {SharedMem}) \times (\textsf {BlockState} \times \textsf {Store} \times \textsf {SharedMem})\), (Fig. 11), and using an auxiliary transition relation between thread local states: \(\rightarrow _{\textit{s}} \subseteq (\textsf {LocalState} \times \textsf {SharedMem}) \times (\textsf {LocalState} \times \textsf {SharedMem})\), (Fig. 12), and then a standard transition relation: \(\rightarrow _{\textit{assg}} \subseteq (\textsf {PrivateMem} \times {\textsf {S}} \times \textsf {SharedMem}) \times (\textsf {PrivateMem} \times \textsf {SharedMem})\) to evaluate assignments (Fig. 13). The semantics of expression e and Boolean expression b over private memory \(\sigma \), written \({\mathcal {E}}\llbracket e \rrbracket _{\sigma }\) and \({\mathcal {B}}\llbracket b \rrbracket _{\sigma }\), respectively, is standard and not discussed any further. We use the standard notation for function update: given a function \(f:A \rightarrow B\), \(a\in A\), and \(b \in B\):As mentioned, the main transition relation between program states is defined in Fig. 11. Program execution starts in a program state where \({\mathcal {P}} \) is the program’s entry block. Depending on the form of \({\mathcal {P}} \), a transition is made into an appropriate block state, leaving the heap unchanged (see rules Init ParC, Init SeqC, Init Fuse, Init Par and Init Seq).

The evaluation of a \(\textsf {ParC}\) state non-deterministically evaluates one of its block states (i.e. \(\textsf {EB} _1\) or \(\textsf {EB} _2\)), until both blocks are done (rule ParC Done).

Evaluation of a sequential block is done by evaluating the local state. The evaluation of a \(\textsf {SeqC}\) state evaluates its block state \(\textsf {EB} \) step by step. When this evaluation is done, evaluation of the subsequent block is initialised.

Rule Lift Seq captures that evaluation of a thread local state is defined in terms of the local thread execution (as defined in Fig. 12). When the local thread state is fully evaluated, this results in a terminated block state (rule Local Done).

The evaluation of a parallel basic block is defined by the rules Par Step and Par Done. To allow all possible interleavings of the threads in the block’s thread pool, each thread has its own local state \(\textsf {LS}\), which can be executed independently, modelled by the mapping \(\mathbb {LS}\). A thread in the parallel block terminates if there are no more statements to be executed and a parallel block terminates if all threads executing the block are terminated.

The evaluation of sequential basic block’s statements as defined in Fig. 12 is standard except when it contains a vectorised basic block. A sequential basic block terminates if there is no instruction left to be executed (Seq Done). The execution of a vectorised block (defined by the rules Init Vec, Vec Step1, Vec Step2, Vec Sync and Vec Done in Fig. 12) is done in lock-step, i.e. all threads execute the same instruction no thread can proceed to the next instruction until all are done, meaning that they all share the same program counter. As explained, we capture this by maintaining an auxiliary set, \({\textsf {E}}\), which contains the identifier of the threads that have already executed the vector instruction (i.e. the guarded assignment \(b \Rightarrow \textsf {assg} \)). When a thread executes a vector instruction, its thread identifier is added to \({\textsf {E}}\) (rules Vec Step). The semantics of vector instructions (i.e. guarded assignments) is the semantics of assignments if the guard evaluates to true and it does nothing otherwise. When all threads have executed the current vector instruction, the condition \({\textsf {E}} = \textsf {dom} (\varSigma )\) holds, and execution moves on to the next vector instruction of the block (with an empty auxiliary set) (rule Vec Sync). The semantics of assignments as defined in Fig. 13 is standard and does not require further discussion.

Figure 14 defines a grammar which captures a commonly used subset of OpenMP [2]. This grammar defines the OpenMP programs that can be encoded into PPL (and thus can be verified using the verification technique presented below).

Our grammar supports the following OpenMP annotations: omp parallel, omp for, omp simd, omp for simd, omp sections, and omp single. Every program is a finite and non-empty list of Jobs enclosed by omp parallel. The body of omp for, omp simd, and omp for simd, is a for-loop. The body of omp single is either a program in our OpenMP subset or it is a sequential code block \(\mathsf {SpecS}\). The omp sections block is a finite list of omp section sub-blocks, where the body of each omp section is either a program in our OpenMP subset or it is a sequential code block \(\mathsf {SpecS}\). For our translation, the relevant clauses are simdlen(M), schedule static, and nowait, all other clauses are ignored.

This section discusses the encoding of OpenMP programs that can be derived from the grammar in Fig. 14 into PPL. The encoding algorithm is presented in Fig. 15 in a functional programming-like style.

Line 2 to 7 of the algorithm define some syntactic macros of several program patterns, to improve readability of the algorithm. Note that in the macro ParVec, \(\mathsf {tid}_1\) refers to the thread identifier of the parallel block, while \(\mathsf {tid}_2\) refers to the thread identifier of the vectorised block. The algorithm consists of two steps: a recursive translate step, and a compose step. The translation step recursively encodes all Jobs into their equivalent PPL code blocks without caring about how they will be composed. Later, the compose step conjoins the translated code blocks together to build a PPL program.

The translation step is a map, which applies the function match to the list of input jobs and returns a list of equivalent PPL code block. The input jobs are encoded in the form (A, C) where A is an OpenMP annotation and C is a code block written in C. The translation returns a list of the form (P, [A]), where P is the PPL program corresponding to the C code, and [A] are the OpenMP annotations that are needed to decide how to combine this PPL block with the other code blocks. Notice that the resulting PPL program is not necessarily a single basic block. The function match works as follows:The match function uses the function sec which recursively calls match on nested parallel blocks. A sequence of sequential statements with a contract is encoded as a parallel block with a single thread. Notice that in these cases, any nested OpenMP clauses are passed on; therefore, the match function returns a pair of a PPL program and a list of OpenMP annotations.

The compose step takes as its input a list of tuples in the form (P, [A]) (the output of the translate step); then it inserts appropriate PPL composition operators between adjacent program blocks in the list, provided certain conditions hold. To properly bind tuples to the composition operators, the operators are inserted in three individual passes; one pass for each composition operator, based on the binding precedence of the operators from high to low as follows: .

Operator insertion is done by the function bundle (lines 40–44). In each pass, bundle consumes the input list recursively. Each recursive call takes the two first tuples of the list and inserts a composition operator if the tuples satisfy the conditions of the composition operator; otherwise, it moves one tuple forward and starts the same process again. Notice that ultimately the head of the list x is composed with the head of the recursive call, rather than with the second element of the list. This is okay, because the composition to be applied is determined locally, and not affected by the compositions of the other blocks.

For each composition operator, the conditions are different. The conditions for parallel and fusion compositions are checked by the functions fusible and par_able. As explained in Sect. 2, fusion of two parallel loops \(\mathsf {L1}\) and \(\mathsf {L2}\) means that the corresponding iterations of \(\mathsf {L1}\) and \(\mathsf {L2}\) are executed by the same thread without waiting. Therefore, fusion composition is inserted between two consecutive tuples \((P_i,[A_i])\) and \((P_j,[A_j])\) if:The parallel composition is inserted between any two tuples in the program where the clauses of the first tuple include a nowait. Otherwise, the sequential composition is inserted. The final outcome is a single merged tuple (P, [A]) where P is the result of the encoding and [A] can be eliminated.

To illustrate the encoding, we discuss the translation of two small OpenMP programs into PPL.

Using the compose function on the list with these two pairs results in the following PPL program:

An iteration contract consists of: a resource contract \(\textit{rc(i)}\), and a functional contract \(\textit{fc(i)}\), where i is the block’s iteration variable. A resource contract indicates the permissions to access memory locations and a functional contract is related to values in the memory locations. Both the resource contract and the functional contract consist of a precondition and a postcondition. We use \(P(i)\) to denote the functional precondition, and \(Q(i)\) to denote the functional postcondition. In case the resource pre- and postcondition are the same, we simply write \(rc(i)\); otherwise, we distinguish them by \(\textit{rc}_{\textsf {pre}}(i)\) and \(\textit{rc}_{\textsf {post}}(i)\).

As mentioned above, a sequential block is executed by a single thread, thus its iteration contract coincides with its block contract, and no special verification rule is needed.

Parallel basic blocks are verified by the rule ParBlock presented in Fig. 16, where \({\textsf {S}} (i)\) is the body of the \(i^{th}\) iteration of the parallel basic block. This rule states that if each single thread respects its iteration contract, the contract for the basic block is composed by the universal separating conjunction of the iteration contract’s precondition and postcondition, respectively. As the threads execute completely independently, there is no permission transfer, and the resource pre- and postcondition coincide. Notice further that soundness of this rule implies that all threads in a parallel block must be independent, because otherwise the universal separating conjunction would not be satisfiable.

For vectorised blocks, the ParBlock rule can be used in case there are no inter-iteration data dependencies. If there are inter-iteration data-dependencies, we need to provide extra annotations that indicate how permissions are transferred inside the vectorised block. In a vectorised block, implicitly all threads synchronise between every instruction. During such a synchronisation, permissions may be transferred from the iteration containing the source of a dependence to the iteration containing the sink of that dependence. To specify such a transfer we introduce ghost statements.³ Remember that according to the PPL grammar, the body of a vectorised block is a sequence of guarded assignments \(b \Rightarrow \textsf {assg} \). A guard \(b_s(i)\) denotes the guard of statement s in iteration i.

A annotation specifies that at label \(L_s\), if a guard \(b_s(i)\) is true, the permissions and properties denoted by formula \(\phi \) are transferred to the statement labelled \(L_r\) in iteration \(i+d\), where i is the current iteration and d is the distance of dependence. A annotation specifies that the permissions and properties denoted by formula \(\psi \) are received by the current iteration from iteration \(i - d\). These annotations always come in pairs. In practice, the information provided by either the annotation is sufficient to infer the other. Therefore, to reduce the annotation overhead, optionally only one of them has to be provided by the developer. However, by providing them both, we make the specifications easier to understand.

In order to verify this example, we need a proof rule for vectorised blocks, as well as for the ghost statements.

The rule for the verification of vectorised blocks is given in Fig. 17. It is similar in spirit to the ParBlock rule, but does not require the resource pre- and postcondition to be the same.

The rules for the ghost statements are similar in spirit to the rules that are typically used for permission transfer upon lock acquiring and release (see e.g. [15]). In particular, is used to give up resources that the acquires. This is captured by the following two proof rules:Receiving permissions and properties that were not sent is unsound. Therefore, send and receive annotations have to be properly matched, meaning that: In other words, the rules in Eq. 1 cannot be used unless the syntactic criterion (i) and the proof obligations (ii) and (iii) hold.

This section discusses the soundness of the proof rules ParBlock and VecBlock above. To show soundness of these rules, we have to show that in order to prove correctness of a parallel or vectorised block, it is sufficient to reason about the body of the block, and to prove independence or inter-iteration data dependence of that body. As always, the interpretation of a Hoare triple \(\{P\}S\{Q\}\) is the following: if the precondition \(P\) holds in a state \(s\), and if execution of statement \(S\) from state \(s\) terminates in a state \(s'\), then the postcondition \(Q\) holds in this state \(s'\). As the proof rules are adapted from the proof rules for parallel and vectorised loops presented in [5], the soundness argument is also similar.

To construct the proof, we define the set of possible execution traces of atomic steps over the vectorised and parallel blocks. In addition, we also define the instrumented sequentialised execution traces for those blocks, which are the executions (1) if all iterations are executed in order and (2) such that validity of each iteration contract is checked for each separate iteration.

To prove soundness of the rule ParBlock, we show that the all execution traces of this statement are equivalent to the instrumented sequentialised execution trace of the parallel block. To prove soundness of the rule VecBlock, we show that all execution traces of this statement are equivalent to the instrumented sequentialised execution trace of the vectorised block.

Functional equivalence of the two traces is shown by transforming the computations in one trace into the computations in the other trace by swapping adjacent independent execution steps.

As mentioned above, we first assume that each basic block of a program is specified by an iteration contract with constant resources \( rc(i) \) for iteration \(i\). Further, we assume that the program is globally specified by a contract \(G\) which consists of the program’s resource contract \( RC_{{\mathcal {P}}} \) and the program’s functional contract \( FC_{{\mathcal {P}}} \) with the program’s precondition \( P_{{\mathcal {P}}} \) and the program’s postcondition \( Q_{{\mathcal {P}}} \).

Let \({\mathbb {P}}\) be the set of all PPL programs and \({\mathcal {P}} \in {\mathbb {P}} \) be an arbitrary PPL program assuming that each basic block in \({\mathcal {P}}\) is identified by a unique label. We define \( {\mathbb {B}} _{\mathcal {P}} =\{b_1,b_2,\ldots ,b_n\} \), as the finite set of basic block labels of the program \({\mathcal {P}}\). For a basic block \( b \) with parallelisation level \( m \), we define a finite set of iteration labels \(\textit{I} _b = \{0^b,1^b,\ldots ,(m-1)^b\} \) where \( i^b \) indicates the \( i^{th} \) iteration of the block \( b \). Let \({\mathbb {I}} _{{\mathcal {P}}} = \bigcup _{b \in {\mathbb {B}} _{{\mathcal {P}}}} \textit{I} _b\) be the finite set of all iterations of the program \({\mathcal {P}}\).

To state our proof rule, we first define the set of all iterations that are not ordered sequentially, the incomparable iteration pairs, \( {\mathfrak {I}}_{\perp } ^{{\mathcal {P}}} \) as:where \( \prec _{e} \subseteq {\mathbb {I}} _{{\mathcal {P}}} \times {\mathbb {I}} _{{\mathcal {P}}} \) is the least partial order which defines an extended happens-before relation. The extension addresses the iterations which are happens-before each other because their blocks are fused. We define \( \prec _{e} \) based on two partial orders over the program’s basic blocks: \( \prec \subseteq {\mathbb {B}} _{{\mathcal {P}}} \times {\mathbb {B}} _{{\mathcal {P}}} \) and \( \prec _{\oplus } \subseteq {\mathbb {B}} _{{\mathcal {P}}} \times {\mathbb {B}} _{{\mathcal {P}}} \). The former is the standard happens-before relation of blocks where they are sequentially composed by , and the latter is an happens-before relation w.r.t. fusion composition \( \oplus \). They are defined by means of an auxiliary partial order generator function such that: and \( \prec _{\oplus } = {\mathcal {G}}({\mathcal {P}},\oplus ) \). We define \({\mathcal {G}}\) as follows:where \({\mathbb {G}} = {\mathcal {G}}({\mathcal {P}} ',\delta ) \cup {\mathcal {G}}({\mathcal {P}} '',\delta )\).

The function \({\mathcal {G}}\) computes the set of all iteration pairs of the input program \({\mathcal {P}}\) which are in relation w.r.t. the given composition operator \( \delta \). This computation is basically a syntactical analysis over the input program. Now we define the extended partial order \( \prec _{e} \) as:This means that the iteration \( i^b \) happens-before the iteration \( j^{b'} \) if \( b \) happens-before \( b' \) (i.e. \( b \) is sequentially composed with \( b' \)) or if \( b \) is fused with \( b' \) and \( i \) and \( j \) are corresponding iterations in \( b \) and \( b' \).

We define the block level linearisation (b-linearisation for short) as a program transformation which substitutes all non-sequential compositions by a sequential composition. We define as a subset of \({\mathbb {P}} \) in which only sequential composition is allowed as composition operator.

Figure 18 presents the rule b-linearise. In this rule, \( rc_b(i) \) and \( rc_{b'}(j) \) are the resource contracts of two different basic blocks b and \(b'\) where \(i^{b} \in \textit{I} _b\) and \(j^{b'} \in \textit{I} _{b'}\). Application of the rule results in two new proof obligations. The first ensures that all heap accesses of all incomparable iteration pairs (the iterations that may run in parallel) are non-conflicting (i.e. all block compositions in \({\mathcal {P}}\) are memory safe). This reduces the correctness proof of \({\mathcal {P}}\) to the correctness proof of its b-linearised variant \(blin ({\mathcal {P}})\) (the second proof obligation). Then, the second proof obligation is discharged in two steps: (1) proving the correctness of each basic block against its iteration contract (using the proof rules discussed above) and (2) proving the correctness of \(blin ({\mathcal {P}})\) against the program contract.

Now we are ready to show that a PPL program with provably correct iteration contracts and a global contract that is provable in our logic (including the rule b-linearise) is indeed data race free and functionally correct w.r.t. its specifications. To show this, we prove (i) soundness of the b-linearise rule and (ii) that each verified program is free of data races.

For the soundness proof, we show that for each program execution there exists a corresponding b-linearised execution with the same functional behaviour (i.e. they end in the same terminal state if they start in the same initial state) if all independent iterations are non-conflicting. From the rule’s assumption, we know that if the precondition holds for the initial state of the b-linearised execution (which is also the initial state of the program execution), then its terminal state satisfies the postcondition. As both executions end in the same terminal state, the postcondition thus also holds for the program execution. To prove that there exists a matching b-linearised execution for each program execution, we first show that any valid program execution can be normalised w.r.t. program order and second that any normalised execution can be mapped to a b-linearised execution. To formalise this argument, we first define: an execution, an instrumented execution, and a normalised execution.

We assume all program’s blocks including basic and composite blocks have a block label and program’s statements are labelled by the label of the block to which they belong. Also there exists a total order over the block labels.

To distinguish between valid and invalid executions, we instrument our operational semantics with heap mas-ks (memory masks). A heap mask models the access permissions to every heap location. It is defined as a map from locations to fractions \(\pi : \textsf {Loc}\rightarrow \textsf {Frac}\) where \(\textsf {Frac}\) is the set of fractions ([0, 1]). Any fraction (0, 1) is a read and 1 is a write permission. The instrumented semantics ensures that each transition has sufficient access permissions to the heap locations that it accesses. We first add a heap mask \(\pi \) to all block state constructors (\(\textsf {Init}\), \(\textsf {ParC}\), \(\textsf {SeqC}\) and so on) and local state constructors (\(\textsf {Vec} \), \(\textsf {Seq} \) and \(\textsf {Done} \)). Then, we extend the operational semantics rules such that in each block initialisation state with heap mask \(\pi \) an extra premise should be discharged, which states that there are \(n \ge 2\) heap masks \(\pi _1, \ldots ,\pi _n\), one for each newly initialised state such that \(\varSigma _i^n \pi _i \le \pi \). The heap masks are carried along by the computation and termination transitions without any extra premises, while in the termination transitions heap masks of the terminated blocks are forgotten as they are not required after termination. As an example, Fig. 19 presents the instrumented versions of the rules Init ParC, ParC Done, rdsh, and wrsh, where \(\rightarrow _{p,i}\) and \(\rightarrow _{assg,i}\) denote program and assignment transition relations in the instrumented semantics, respectively. If a transition cannot satisfy its premises, it blocks.

A normalised execution is an instrumented execution that respects the program order, which is defined using an auxiliary labelling function \({\mathcal {L}}: {\mathbb {T}} \rightarrow {\mathbb {B}}^{all}_{{\mathcal {P}}} \times {\mathbb {L}}\) where \({\mathbb {T}}\) is the set of all transitions, \({\mathbb {L}}\) is the set of labels \(\{I,C,T\}\), and \({\mathbb {B}}^{all}_{{\mathcal {P}}}\) is the set of block labels (including both composite and basic block labels).where \( LB \) returns the label of each block or statement in the program. We say transition t with label (b, l) is less than \(t'\) with label \((b',l')\) if \((b \le b') \vee (l'=T \wedge b \in LB_{sub}(b'))\) where \(LB_{sub}(b)\) returns the label set of all blocks of which b is composed.

We transform an instrumented execution to a normalised one by safely commuting the transitions whose labels do not respect the program order.

The validity of and is defined by the semantics of formulas presented in 2.2.

Finally, we show that a verified program is indeed data-race-free.

Next we look at how to adapt this rule in case there are intra-block dependencies; thus, the resource pre- and postconditions of individual iterations are different, and we need send/receive annotations in order to verify the blocks.

This makes the independence check more involved: instead of just checking that the resource contracts for independent iterations are non-conflicting (\(\forall (i^b,j^{b'}) \in {\mathfrak {I}}_{\perp } ^{{\mathcal {P}}}.(RC_{{\mathcal {P}}} \rightarrow rc_b(i) \mathop {\star }rc_{b'}(j))\)), we now need to check the absence of conflicts for all combinations of resource pre- and postconditions. In case there is only a single resource transfer, we can replace this condition in the rule b-linearise by the following condition:This new version of the rule b-linearise is sound, because: However, if multiple resource transfers happen within a block, it can happen that at an intermediate point in the block, the thread holds more permissions than it holds at the beginning and the end of the block. To address this, we need to define the intermediate maximal resource contract for an intermediate statement S as the universal separating conjunction of the iteration’s precondition, and all the resources that are received by all statements that happen-before S. Absence of conflicts is then defined as a check over all intermediate resource contracts. It is future work to define this formally.

To verify our iteration contracts using Viper, we encode the behaviour of the basic blocks and the annotations as method contracts. The idea is that every block annotated with an iteration contract is encoded by a call to the method , whose contract encodes the application of the suitable Hoare Logic rule for basic blocks, instantiated for the specific iteration contract.

We also need to verify that every iteration respects the iteration contract. This is encoded by a method, parametrised by the thread identifier, containing the basic block’s body, and specified by the iteration contract.

Within the body of the basic block there may be statements.

The guards are untouched, but the statements are replaced by method calls

where

Finally, we need to check that the proof obligations in Eq. 2 and 3 hold.

Finally, for the verification of block composition, we implemented the rule b-linearize as part of the encoding into Viper. This means we implemented in VerCors:This implementation basically follows the formal definition as presented above in Sect. 6.

Next, as part of the Viper encoding, we encode the first proof obligationas lemmas for all independent iteration pairs \((i^b,j^{b'})\), i.e. these are encoded as specifications for empty method bodies of the following form:

Finally, for the b-linearised program, we prove that it satisfies the global method specification.