The main data structure used in the algorithms is that of a State, which stores both program variables and scheduling information, in the attributes *finder* , *rounds taken*, and *delays taken*. For a state s, variables s.*rounds taken* and s.*delays taken* represent the number of times the scheduler started a round and delayed a thread, resp., to get to s. Variable s.*finder* contains the index of the thread whose action produced s. This is enough information to continue

**Algorithm 1.** Verifying property C against all reachable states of program P

```
Input: n-thread asynchronous program, property C
Output: "safe", "violation of C", or "unknown"
1: Reached := (finite) set of initial states -
                                             Reached: states reached so far
2: r := 0; d := 0
3: repeat
4: Frontier := {s ∈ Reached : s.rounds taken = r}
5: r++
6: for s ∈ Frontier do
7: Reached := Reached ∪ FinishRounds(s, r + 1, C)
8: r++
9: until round plateau of length 1
10: repeat
11: Frontier := {s ∈ Reached : s.delays taken = d}
12: d++
13: for s ∈ Frontier do
14: s-
          := s -
                                                          copy of state s
15: s-

          .delays taken++
16: s-

          .finder := (s-

                      .finder + 1) mod n
17: if s-

            .finder mod n = 0 then
18: s-

             .rounds taken++
19: Reached := Reached ∪ FinishRounds(s-

                                          , r, C)
20: if new abstract state found during for loop in Line 13 then
21: goto 3 -
                                   abort second repeat loop; go back to first
22: until delay plateau of length n − 1
23: if α(Reached) is closed under disrespectful actions then
24: return "safe"
25: else
26: return "unknown"
```
**Algorithm 2.** *FinishRounds*(s, r, C)

the execution from s later, starting with the thread after *finder* . For the initial states, *rounds taken* and *delays taken* are zero, and *finder* is n−1 (the latter so that expanding the initial states starts with thread (n − 1) + 1 mod n = 0). For set membership testing, two states are considered equal when they agree on their finders and on program variables. The *rounds taken* and *delays taken* variables are for scheduling purposes only and ignored when checking for equality.

As mentioned in Prop. 3, the sequence of reachability sets is monotone with respect to both rounds and delays, for any program. This entails two useful properties for Algorithm 1. First, we can increase the bounds in any order and at individual rates. Second, it suffices to expand states at the frontier of the exploration, without missing new schedules. When adding a new delay, we only need to delay those states that were (first) found in schedules using the maximum delays. When adding a round, we only need to expand states that were (first) found in the last round of a schedule.

Algorithm 1 first advances the round parameter r until a round plateau has been reached (Lines 3–9). It does so by running the *FinishRounds* function on *frontier states* s: those that were reached in the final round r of the previous round iteration. *FinishRounds* (Algorithm 2) explores from the given state s, Round-Robin style, up to the given round, without delaying any thread. The actual expansion of a state happens in function *Image* (Line 8 of Algorithm 2), which computes a state's successors and initializes their scheduling variables: *rounds taken* and *delays taken* are copied from u, the *finder* of the successor is the next thread (+1 mod n). If this wraps around, *rounds taken* is incremented as well.

Back to the main Algorithm 1: we have reached a round plateau of length 1 if the entire **for** loop in Line 6 sees no new *abstract* states (no new elements in α(*Reached*)). If so, we are not ready yet to perform the convergence test (recall Example 8). Instead, Algorithm 1 now similarly advances the delay parameter d (Lines 10–22). For each frontier state (*delays taken* = d), we delay the thread scheduled to execute from this state (by incrementing (mod n) the *finder* variable), and record the taken delay (Line 15). Then we again call the *FinishRounds* function and merge in the states found. Importantly, these merges preserve states already in *Reached*, meaning that the algorithm will keep states found earlier in the exploration (with smaller r, d).

The loop beginning in Line 10 repeats until a delay plateau of length n − 1 is encountered (as required by Theorem 7). This means that during n − 1 consecutive **repeat** iterations, the **for** loop in 13 did not find any new abstract states. When the round and delay plateaus have the required lengths (1 and n−1, resp.), we invoke the convergence test (Line 23), which amounts to applying Theorem 7. If the test fails, Algorithm 1 returns "unknown".

Towards proving partial correctness of Algorithm 1, we first show that the states eventually collected in set *Reached* by the algorithm correspond exactly to the round- and delay-bounded reachability sets R(r, d), and that—after the two main **repeat** loops—a plateau of sufficient length has been generated. As a corollary, the algorithm is partially correct, i.e. it returns correct answers if it terminates.

**Lemma 9.** *If Algorithm 1 reaches Line 23, the current values of* r *and* d *satisfy: (i) Reached* = R(r, d)*, and (ii)* R(r − 1, d − (n − 1)) = R(r, d)*.*

**Corollary 10.** *The answers "safe" and "violation of* C*" returned by Algorithm 1 are correct.*

The algorithm won't return either "safe" or "violation of C" in one of two situations: when the convergence test fails in Line 23 (it gives up), and when it fails to ever reach this line. The latter can be prevented using a finite-domain α:

**Lemma 11.** *If the domain* A *of abstraction function* α *is finite, Algorithm 1 terminates on every input.*

Since abstraction α approximates the information contained in a state, a plateau may be *intermediate*, e.g. R(1, 0) - R(1, 1) = R(2, 2) - R(2, 3). Thus, stopping the exploration simply on account of encountering a plateau—even of lengths (1, n−1)—is unsound. Intermediate plateaus make our algorithm (unavoidably) incomplete: if the test in Line 23 fails, then there are known-to-be-reachable abstract states with abstract successors whose reachability cannot be decided at that moment. If we knew the plateau to be intermediate, we could keep exploring the sets R(r, d) for larger values of r and d until the next plateau emerges, hoping that the convergence test succeeds at that time. In general, however, we cannot distinguish intermediate from final plateaus.

#### **5 DrUBA with Unbounded-Domain Variables**

In addition to unbounded control structures like stacks, which come up in pushdown systems and were discussed in Ex 5, infinite state spaces in programs are often due to (nominally) unbounded-domain program variables. This presents no problem for the computation of the concrete reachability sets *Reached* in Algorithm 1: for any round and delay bounds (r, d), the set of concrete reachable states *RR*(r, d) is finite and thus explicitly computable (no symbolic data structures are needed).2 On the other hand, termination of the same algorithm requires that it eventually reach a plateau in r and d of sufficient length. This is guaranteed by an abstraction function α that maps concrete states into a finite abstract space. A finite abstract domain is therefore highly desirable.

A generic abstraction that reduces an unbounded data domain to a finite one is predicate abstraction [4,13, see [14] for a short primer]. The goal in this section is to demonstrate how the simple scheme of delay-unbounded analysis can be combined with predicate abstraction to verify unbounded-thread programs.

2 Contrast this to a *context-switch* bound, under which reachability sets can be infinite.

#### **5.1 The Fixed-Thread Case**

Consider program P in Fig. 1 on the left [8, page 4: program P]. Intuitively, variable m counts the number of threads spawned to execute P concurrently. It is easy to see that "the assertion in [P] cannot be violated, no matter how many threads execute [P], since no thread but the first will manage to" [8] enter the *true* branch of the **if** statement and reach the assertion.

**Fig. 1. Left:** program P; **Right:** how Algorithm 1 operates on (an abstraction of) it

Previous work has shown that even the 1-thread version of this program cannot be proved correct using predicate abstraction **unless** we permit predicates that depend on both shared and local variables [9, for the unprovability result], which have been referred to as *mixed* [8]. An example is the predicate p :: (s = l), which comes up in the assertion. The dependence of p on both shared and thread-local data causes standard solutions that track the truth value of p in a shared or local Boolean variable to be unsound. The solution proposed in [8] is to use *broadcast* instructions to have the executing thread notify all other threads whenever the truth value of p changes. This solution comes with two disadvantages: (i) the resulting Boolean broadcast programs are more expensive to analyze than strictly asynchronous Boolean programs, and (ii) the solution cannot be extended to the unbounded-thread case.

Let us consider how we can verify this program using Algorithm 1, for the fixed-thread case; we consider n = 2 threads. We will have to use mixed predicates as in [8], but since we never execute the abstract Boolean program, there is no need for constructing it. As a result, there is no need for broadcast instructions.

The program generates an unbounded number of reachable concrete states, but we explore it only under round and delay bounds r and d. As per Algorithm 1, we increase these bounds until we have reached plateaus of lengths 1 and n − 1 = 1, resp. Plateaus are determined over the abstract-state set, so we need a function α.

*First attempt: a single predicate.* We define α as follows, for a concrete state c:

$$\alpha\_1(c) \;=\; (c.pc\_0, \; c.s = c.l\_0) \in \mathbf{0}, \; \dots, \mathbf{4} \times \{0, 1\} \;, \; c$$

where c.*pc*0, c.l0, and c.s are the values of thread 0's *pc* and local variable l, and of shared variable s, in state c, respectively. The function extracts from a concrete state the current program location of thread 0 and the value of predicate p :: (s = l) for thread 0.3 The only statement *not* respecting α1 is the **if** statement in Line 1: here, the new value of the *pc* cannot be determined from the current values of *pc* and predicate p alone. All other statements respect α1.

We can now perform an iterative exploration of this program—bounded but exhaustive within each bound. In Fig. 1 on the right, red arrows denote "new abstract state reached". A red horizontal arrow (r++) means: "keep increasing r". A red vertical arrow (d++) means: "switch to increasing r". In other words, following a red arrow—no matter the direction—we always go "right" (r++). The green horizontal arrow followed by a green vertical arrow at the end indicates that we have reached the first plateaus of length 1 in *both* directions: at (r, d) = (7, 4).

At this point we have reached a total of 7 abstract states. State (3, 0) (*pc* = 3, s = l) is not among them, so the assertion has not been violated so far. We run the convergence test, to determine whether set R(7, 4) is closed under disrespectful actions. Since the **if** in Line 1 is the only disrespectful statement, we only need to check successors of abstract states of the form (1, ?) (i.e., with *pc* = 1). Unfortunately, R(7, 4) contains abstract state (1, 0) (a reachable abstract state) but not its abstract successor (2, 0). This state is unreachable, but we do not know that at this point. This causes Algorithm 1 to return "unknown".

*Second attempt: two predicates.* The disrespectful action causing the failure suggests that we need to keep track of whether the branch in Line 1 can be taken, i.e. whether m = 1. We refine our abstraction using this (non-mixed) predicate:

$$\alpha\_2(c) \quad = \quad (c.pc\_0, \ c.s = c.l\_0, \ c.m = 1) \in 0, \ldots, 4 \times \{0, 1\}^2 \, . \tag{4}$$

The abstract successors of the **if** statement can now be decided based only on knowledge provided by α2, i.e. the statement respects α2. There is, however, another statement disrespecting α2, and only one: the increment m++ in Line 0. If m = 1, we cannot decide whether m = 1 will be true after the increment.

We again perform our iterative exploration of this program, and find the first suitable plateau at the same point (r, d) = (7, 4). This time, however, we have reached a total of 12 abstract states (all of them "safe"). We run the convergence test: we only need to check already reached abstract states of the form (0, ?, 0) (*pc* = 0, m = 1). Set R(7, 4) contains exactly one state of this form: (0, 1, 0), which m++ can turn into (1, 1, 0) and (1, 1, 1)—note that the next *pc* value is unambiguous (1), and predicate s = l is not affected. **The good news** is now that both abstract states (1, 1, 0) and (1, 1, 1) are contained in R(7, 4). This proves this set closed under disrespectful actions; Algorithm 1 terminates: the assertion is safe for any execution schedule, for the case of n = 2 threads.

3 Tracking these values for thread 0 suffices: the multi-threaded program is symmetric.

We summarize that, in our solution above, we assumed a lucky hand in picking predicates—the question of predicate discovery is orthogonal to the delayunbounded analysis scheme. However, the proof obtained using Algorithm 1 does not involve costly broadcast operations, previously proposed as an ingredient to extend predicate abstraction to concurrent programs. A second, more powerful advantage is that, unlike the earlier broadcast solution, Algorithm 1 extends gracefully to the unbounded-thread case. This is the topic of the rest of this section.

#### **5.2 The Unbounded-Thread Case**

The goal now is to investigate whether an asynchronous unbounded-domain variable program is safe for *arbitrary* thread counts (and thread interleavings).

*Existing solutions.* We are aware of only one general technique that combines predicate abstraction with unbounded-thread concurrency [15]. That technique can achieve the above goal, roughly as follows. In addition to standard and mixed predicates used also in the fixed-thread case, we now permit *inter-thread* predicates, which quantify over all threads other than the executing one. Such predicates allow us to express, for example, that a thread's local variable l's value is larger than that of any other thread: ∀i : i = *self* : l>l*i*. Predicates of this type are provably required during predicate abstraction to verify the safety of the Ticket Lock algorithm [3,15].

Abstraction against inter-thread predicates leads to a *dual-reference program* [15], a process that is already far more complex than standard sequential or even fixed-thread predicate abstraction. But we pay another price for using these predicates: namely, the loss of *monotonicity* of the transition relation w.r.t. a standard well-quasiordering on infinite state sets of unboundedthread Boolean programs. In this context, monotonicity states, roughly, that adding passive threads to a valid transition keeps the transition intact.

This price is heavy, since monotonicity w.r.t. would have given us a well-quasiordered infinite-state transition system, for which local-state reachability properties are decidable [1]; working implementations exist. The abovementioned prior work attempts to salvage the situation, by adding a set of transitions (the *non-monotone fragment*) to the dual-reference program that restore monotonicity and further overapproximate but without affecting the reachability of unsafe states [15].

*Alternative solution.* We now propose a solution that uses the same type of interthread predicates (this is inevitable), but renders dual-reference programs, the monotone closure of the transition relation and all other "overhead" introduced in [15] unnecessary. We will use Algorithm 1 as a sub-routine.

The idea is as follows. Sect. 5.1 suggests a way to verify fixed-thread asynchronous programs, using a combination of predicate abstraction and Algorithm 1 . To handle the unbounded-thread case, we wrap another layer of incremental resource bounding around this combined algorithm—the "resource" this time is the number n of threads executing the program. For each member of a sequence of increasing fixed thread counts we compute the set of abstract states reachable under arbitrary thread interleavings. This is purely a sub-routine; we will use the method proposed in Sect. 5.1 (others are possible, e.g. [8]).

The incremental (in n) analysis proceeds until we have reached a thread plateau *of length 1*, and then run the convergence test: we check the current abstract reachability set for closure under disrespectful actions. This time, the abstract transitions must take into account that the number of executing threads is unknown. It is easy to see that a plateau of length 1 is sufficient: we compute the set of abstract states reachable under *arbitrary* thread schedules; thus, the obstacle of non-schedulability of thread i in the proof of Theorem 7 that forced us to wait for a (delay) plateau of length n − 1 does not apply here.

#### **A non-monotone resource parameterization**

Before we demonstrate this idea on program P, we justify our strategy of combining resource bounds. The idea presented above can be viewed as a multi-resource analysis problem where we increment r and d in an "inner loop" (represented by Algorithm 1 as a sub-routine to compute fixed-thread reachability sets), and n in an outer loop. Both loops compute monotonously increasing reachability sequences: for "inner" this is Prop. 3; for "outer" this is easy to see. Theorem 7 relies upon the monotonicity: without it, the test R(r, d) = R(r + 1, d + n − 1) makes the algorithm unsound.

The way we nest the three involved resource parameters is not arbitrary: Round-Robin reachability under an increasing thread count is not monotone. More precisely, making the thread-count parameter n explicit, let R(r, d, n) denote the set of states reachable in the n-thread program P under *RR*(r, d) scheduling. Then R(r, d, n) ⊆ R(r, d, n + 1) is **not** valid. The following example illustrates this (at first counter-intuitive) monotonicity violation:

**Example 12.** *Consider the asynchronous Boolean program over shared varinables* s *and* t *on the right. Here we have* R(3, 0, 1) ⊆ R(3, 0, 2)*: given 1 thread (sequential execution), a state with*

s = 1 *is reachable. With 2 symmetric threads, under delay-free Round-Robin scheduling (*d = 0*), the first and second thread will repeatedly flip* t *to* 1 *and back to* 0*, resp., before either one has a chance to get past the guard in* Line 1.

*A stronger result is: for all* r ∈ N*,* R(3, 0, 1) ⊆ R(r, 0, 2)*, i.e. we cannot make up for the poor scheduling of the second thread by adding more rounds.*

The consequence for us is that we cannot compute, for fixed r, d, the sets R(r, d,∞), using the closure-under-disrespectful-actions paradigm. Instead we must, for each n, compute R(∞,∞, n) (using Algorithm 1 or otherwise) and increase n in the outer loop.

#### **Verifying program** P **for unbounded thread count**

We recall that, given the two predicates shown in Eq. (4) and the pc, we were able to verify program P correct (under arbitrary thread interleavings) for n = 2 threads; a total of 12 abstract states were reached (out of 5 · 22 = 20 possible). Advancing the outer loop, we invoke Algorithm 1 for n = 3 threads. This reveals another reachable abstract state, namely *pc* = 0, s = l, m = 1. Unfortunately, this state causes Algorithm 1 to return "unknown": under α2, one currently unreached abstract successor is *pc* = 1, s = l, m = 1, violating closure. Observing that a thread executing Line 1 with m = 1 must be the first thread executing, we try tracking the initial value of m:

$$\alpha\_3(c) \quad = \quad (c.pc\_0, \ c.s = c.l\_0, \ c.m = 1, \ c.m = 0) \in 0, \ldots, 4 \times \{0, 1\}^3. \tag{5}$$

Interestingly, *all actions (statements) of program* P *respect abstraction* α3. This means that the test for closure under disrespectful actions is *vacuously true*—we can stop as soon as we have reached a plateau in n of length 1. We don't have to wait long for this plateau: we invoke Algorithm 1 for n = 3 and n = 4 under abstraction α3. (Note that n = 4 requires a longer plateau than n = 3.) The abstract reachability sets consist of the same 14 abstract states in both cases. We report the program safe, for arbitrary interleavings and arbitrary thread counts. We can also report the exact set of 14 reachable abstract states.

We again summarize that, while we still (and unavoidably) use mixed predicates, we do not construct a thread-parameterized abstract program, which would require broadcast statements [8] and a rather involved dual-reference transition semantics [15]. In fact, we did not even need to test for closure under any abstract images, since the chosen abstraction enjoys respect from all actions.

#### **6 Evaluation**

Our goal for the evaluation of DrUBA was to answer the following questions:

Questions 1 and 2 serve to compare DrUBA against other techniques; Questions 3 and 4 investigate features of Algorithm 1.

To this end we implemented, in Java 11, a verifier using Algorithm 1 that takes concurrent pushdown systems as input; we refer to this verifier as DrUBA in this section.4 We also implemented the AI approach in Java 11. For the comparison with the context-unbounded approach, we used a publicly available tool5. Our experiments are based on the concurrent benchmark programs also used in [18]. The experiments are performed on a 3.20GHz Intel i5 PC. The memory limit was 8GB, with a timeout of 1 h.

4 DrUBA implementation available at https://doi.org/10.5281/zenodo.4726301.

5 https://github.com/lpzun/cuba.

#### **6.1 Results**

Table 2 reports the benchmark names, the thread counts, and the size of the reachable abstract state space (columns 1–3). The second part of the table shows the time it took each verifier to fully explore the state space and confirm convergence. For the AI approach, we check whether the abstract state space is closed under *all* operations each time either r or d is incremented. Algorithm 1 was faster than "AI" on every example except Stefan-4,5. Stefan is the only program that actually does not require any delays to discover all reachable abstract states. The results indicate that the AI approach spends approximately half of its computation time doing repeated convergence tests after each bound increment. Furthermore, as state sets increase in size, AI seems to take even longer, as with the Bluetooth3 (2+3) example. The convergence test needed for "AI" includes checking closure under both respectful and disrespectful actions, making it more costly than the one used in Algorithm 1.

Algorithm 1 also improved on the results with "CUBA". For examples that took longer than a few seconds, DrUBA was able to run in less time on the same benchmark. The difference on small examples is likely due to a different implementation language (C++ vs. Java). DrUBA does not explore as many schedules, and explores fewer as the delay and round bounds approach their cutoff values (as noted below). Additionally, DrUBA was less memory-intensive for large examples for which the CUBA approach cannot prove that the set of reachable states per context bound is finite. In this case, "CUBA" requires the use of more expensive symbolic representations of states sets. Algorithm 1 does not suffer from this problem—the reachability sets in each iteration are finite. For the Stefan-5 example, "CUBA" ran out of memory after 23 min. DrUBA was able to prove convergence for this example (as was "AI").

Table 3 reports the number of times Algorithm 1 computed the image (successors) of a state until reaching the final r-d-plateau (Col. 3) and during the final plateau (Col. 4), as well as the total number of image computations without the *frontier* optimization (Col. 5). The table offers convincing evidence to support our heuristic that waiting for a long d-plateau at the end of exploration is not costly, answering Question 3.. On most benchmarks, the amount of computation done during the plateau (Col. 4) was negligible. This included our largest example, Bluetooth3 (2+3). The exception to this is the Stefan examples, which—as mentioned earlier—do not require any delays to reach the full abstract state set (the d-plateau starts at (rmax,0)). Finally, a naive implementation that does not take advantage of monotonicity, forgoing the frontier approach to expanding the state set, was orders of magnitude worse. This is because it has to recompute the whole set for every iteration of r or d. This answers Question 4..

Comparing Col. 7 in Table 2 to the cutoff context-switch bounds from [18], we find that, while the r and d bounds were large, not all programs that needed large bounds took a long time to verify. For example, the Bluetooth3 (2+1) example took much less time than Stefan-5, despite requiring 21 more delays (with similar rounds). A hint for the reason can be found in Table 3. Once the set of abstract states is close to the R, there are very few new states on the

**Table 2.** Benchmark description and running times for different algorithms. Threads: # of threads (a + b: the respective numbers of threads from two different templates); R: number of reachable abstract states; Time: running time (sec) for each algorithm ("—": timeout or memory-out); rmax, dmax: round and delay counts at the *end* of each plateau when convergence was detected.

frontier. We can see this in the small numbers in Col. 4, but it also applies to the round bound. If a state is rediscovered, it is not expanded in further round increments. Once the round bound is large enough, there are few deep schedules of maximum possible length (nr) that produce new concrete states.

#### **6.2 Unbounded-Thread Experiments**

We implemented Algorithm 1 in combination with predicate abstraction as detailed in Sect. 5.2 to check the effectiveness of our technique on a tricky concurrent program that requires unbounded variable domains. The Ticket Lock

**Table 3.** Detailed analysis of Algorithm 1, measuring the number of times the program computed the successors of a state. Col. 3 reports the image operations Algorithm 1 performed before reaching the FP (final plateau), Col. 4—the number of additional image operations computed until the program ended. Col. 5 shows the image operations without the *frontier* improvement, requiring recomputing each R(r, d) from the initial states.

protocol [3] and the predicates used to prove its correctness are shown in Fig. 2. In Line 0, threads wait to enter the Critical Section, whose code is at the beginning of Line 1; the rest of Line 1 is exit code to prepare the thread for re-entry. In the predicates on the right, subscript i denotes thread i's copy of a local variable.

This example has been shown to require significant adjustments to predicate abstraction to accommodate fixed-thread concurrency [8], and has been claimed to require an entirely new theory to cope with the unbounded-thread case [15]. We rely on the same predicates used in earlier work, and it is clear what motivates each predicate. P1 ensures t is a"new" ticket larger than previous ones, P2 is

**shared int** *s* := 0, *t* := 0 **local int** *l* := fetch and add(*t*) 0: **while** *s* -= *l* **do**; wait for *s* = *l* 1: *critical-section code here* inc(*s*) *l* := fetch and add(*t*) **goto** 0 **P4:** ∀*i* : *i* -

**P1:** ∀*i* : *t>li* **P2:** |{*i* : *pci* = 1}| ≥ 2 **P3:** *s* = *l* = *self* : *l* -= *li*

**Fig. 2. Left:** the Ticket Lock protocol; **Right:** four predicates used to prove it correct

used to check the safety property, P3 tracks the condition in Line 0, and P4 means that the operating thread's l is unique. DrUBA finds four abstract states for both 2 threads and 3 threads using Algorithm 1. This is an n-plateau of length 1.

To prove convergence for both Algorithm 1 and the "outer loop" incrementing n, we used the ACL2s theorem prover [7]. We specified the data in a concrete state, and the four abstract states that were found. Only the second statement disrespects this abstraction w.r.t. r, d and n, as we know the value of the test in the first statement for an abstract state. Given these, ACL2s was able to verify that the set of abstract states is closed under the semantics of statement 1. As a result, we can report that Ticket Lock is safe (P2 is invariantly false), for an arbitrary number of threads and arbitrary thread interleavings.

#### **7 Discussion of Related Work**

This work is inspired from two angles. The first is clearly the delay-bounded scheduling (DBS) technique [10]. The authors formalize this concept and show its effectiveness as a testing scheme. Their computational model of a dynamic task buffer is somewhat different from ours. We have not discussed dynamic thread creation here; it can be simulated by creating threads up-front and delaying them until such time as they are supposed to come into existence. The DBS paper also presents a sequentialization technique that can be turned into a symbolic verifier via verification-condition generation and SMT solving. This, however, requires bounding loops and recursion. Our approach combines exhaustive finite-state model exploration with convergence detection and thus does not suffer from these restrictions.

The second inspiration comes from an earlier context-unbounded analysis technique [18]. Similar in spirit to the present work, [18] started from a yet earlier context-bounded analysis technique and describes a condition under which a chosen context bound is sufficient to reach all states reachable under some abstraction. For the case of concurrent pushdown systems (CPDS)—the verification target of [18]—, the pop operation plays a crucial role in establishing this condition; note that, in our work, pop actions disrespect the top-of-the-stack abstraction commonly used for CPDS.

Our work has a number of advantages over [18]. First, and crucially, the set of states reachable under a context bound can be infinite (a single context can already generate infinitely many states); its determination thus requires more expensive symbolic reachability methods. In contrast, the reachability set under Round-Robin scheduling with a round- and a delay bound *is always finite*; moreover, it can be computed very easily, even for complex programs. This makes our technique a prime choice for lifting existing testing schemes to verifiers. A second advantage over [18] is that we retain much of the efficiency of the "almost deterministic" exploration delay-bounded scheduling, as demonstrated in Sect. 6. A downside of our work is that our convergence condition is sound only after a plateau has emerged of length roughly equal to the number of running threads; this is not required in [18]. However, as also demonstrated in Sect. 6, our efforts to compute reachable states for increasing r, d in a *frontier-driven* way nearly annihilates this drawback: in most cases, only a small number of image computations happen along the plateau.

An alternative to our verification approach is a classical analysis based on abstract interpretation [6]. Given function α, such analysis interprets the entire program abstractly, and then computes a fixed point under the abstract program's transition relation. This fixed point, if it exists, overapproximates the set of reachable abstract states. Hence, the absence of error states in the fixed point implies safety, but the presence of errors does not immediately permit a conclusion. In contrast, our technique interleaves *concrete* state space exploration (enabling genuine testing) with *abstraction-based* convergence detection. We believe this to be a useful approach in practical programming environments, where abstract proof engines with poorly understood bug-finding capabilities may be met with skepticism. A more detailed discussion of DrUBA vs. Abstract Interpretation can be found in the Appendix of [14].

Underapproximating program behaviors using bounding techniques is a widespread solution to address undecidability of safety verification problems. Examples include depth- [12] and context-bounding [16,17,20], delay-bounding [10], bounded asynchrony [11], preemption-bounding [19], and phase-bounded analysis [2,5]. Many of these bounding techniques admit decidable analysis problems [16,17,20] and thus have been successfully used in practice for bug finding. Round- and delay-bounded Round-Robin scheduling trivially renders safety decidable, since the delay-program is finite-state. In addition, it is very easy to implement, avoiding, for example, the need for symbolic data structures and algorithms to represent and process intermediate reachability sets.

#### **8 Conclusion**

We have presented an approach to enhancing delay-bounded scheduling in asynchronous programs with a convergence test that, if successful, certifies that all states from some chosen abstract domain have been reached. The resulting algorithm inherits from earlier work the capability to detect bugs efficiently, but can also prove safety properties, under arbitrary thread interleavings. It exploits the monotonicity of delay-bounded reachability sets to expand states and test for convergence only when needed. We have further demonstrated that, combined with predicate abstraction using powerful predicates, tricky unbounded-thread routines over unbounded data, such as the Ticket Lock, can be verified using substantially less machinery than proposed in earlier work. We have shown the experimental competitiveness of our approach against several related techniques.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Checking Data-Race Freedom of GPU Kernels, Compositionally

Tiago Cogumbreiro1(B) , Julien Lange2 , Dennis Liew Zhen Rong1 , and Hannah Zicarelli1

1 University of Massachusetts Boston, Boston, USA<EMAIL_ADDRESS>2 Royal Holloway, University of London, Egham, UK<EMAIL_ADDRESS>
Abstract. GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing approaches produce too many false alarms and struggle to handle larger programs. To address these limitations we formalize a novel compositional analysis for DRF, based on access memory protocols. These protocols are behavioral types that codify the way threads interact over shared memory.

Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels. Our theory is implemented in Faial, a tool that outperforms the state-ofthe-art. Notably, it can correctly verify at least 1*.*42× more real-world kernels, and it exhibits a linear growth in 4 out of 5 experiments, while others grow exponentially in all 5 experiments.

Keywords: GPU · Data-race · Static analysis · Behavioural types

#### 1 Introduction

GPUs are massively parallel devices that promise a great return on investment at a cost: they are notably difficult to program. In GPU programming, hundreds of lightweight threads share portions of arrays in parallel (without locks)—very different from the programming model of multithreaded programs written in C or Java with heavy-weight heterogeneous threads. Data-race freedom (DRF) analysis aims to guarantee that for all possible executions, every array cell being written by one thread cannot be concurrently accessed by another thread.

In the field of static analysis of DRF in GPU programs, there is a tension between efficiency and correctness (no missed data-races and no false alarms) that thus far is unresolved. Bug finding tools [26,27,33] favor correctness over efficiency: they provide correct results at small scales, by simulating the program execution. Such tools are incapable of handling certain parameters symbolically (*e.g.*, array size) and can easily exhaust users' resources (*e.g.*, loops with long iteration spaces or unknown bounds). Approaches based on Hoare logic [5,7,22]

Fig. 1. Work-flow of the verification.

can cope with medium-sized programs, do not miss data-races, and do not require array size information; however, they suffer from a high-rate of false alarms and require code annotations written by concurrency experts. Finally, tools that can cope with larger programs and do not require array size information either miss data-races [24] or overwhelm the user with false alarms [37].

To appease this tension, we introduce a novel static DRF analysis that can handle larger programs and produce fewer false alarms than related work, without missing data-races. Additionally our analysis does not require code annotations or array size information. Our verification framework hinges on *access memory protocols*, a new family of behavioral types [1] that codify the way threads interact through shared memory. Our behavioral types also make evident two aspects of the analysis that can be made separate: concurrency analysis (*i.e.*, could these two expressions run in parallel?) and data-race conflict detection (*i.e.*, do these array indices match?).

*Contributions and Synopsis.* This paper includes the following contributions.

Listing 2.1 Examples of racy kernels, l.h.s. is from [34] and r.h.s. simplifies l.h.s. for clarity, with one-dimensional array and thread identifier, and 1-stride loops.

Our paper is accompanied by an implementation (Faial), an evaluation framework (inc. datasets), and proof scripts (in Coq) for each theorem. All of these are available in our artifact [9].

#### 2 Overview

This section gives an overview of our approach by examining a data-race we found in published work [17,34]. We discuss the challenges that such examples pose to the state-of-the-art of DRF analysis. Then we introduce a verification framework based on *access memory protocols*: behavioral types [1] that codify the way threads interact via shared memory. Figure 1 gives an overview of the verification pipeline. We start from CUDA kernels, from which we infer access memory protocols. Protocols are then checked for well-formedness and transformed in three steps into formulas that are verified by an SMT solver.

#### 2.1 Challenges of GPU Programming

GPU Programming Model. The key component of GPU programming is the *kernel* program, or just kernel, that runs according to the Single-Instruction-Multiple-Thread (SIMT) execution model, where multiple threads run a single instruction concurrently. A kernel is parameterized by a special variable that holds a thread identifier, henceforth named tid. In parallel, each member of a group of threads runs an instantiated copy of the kernel by supplying its identifier as an argument. Threads communicate via shared memory (arrays) and mediate communication via barrier synchronization (an execution point where all threads must wait for each other before advancing further). Writes are only guaranteed to be visible to other threads after a barrier synchronization.

GPU programming platforms usually group threads hierarchically in multiple levels, across which no inter-groups synchronization is possible. In both the literature [6,24] and this work, the focus is on intra-group communication.

Challenges. We motivate the difficulty of analyzing data-races by studying a programming error found in the wild, reported in Listing 2.1 (left). This excerpt comes from a tutorial [34] on optimizing numeric algorithms for GPUs. The code listing transposes a matrix N-times with an outer loop indexed by variable r.

Remarkably, the tutorial [34] does not inform the readers that Listing 2.1 contains a subtle *data-race*: one transpose-operation starts (the writes to tile Listing 2.2 Minimal representative example of an access memory protocol highlighting the data-race in Listing 2.1.

```
1 // r = 0
2 forU j in 0..M // for ( int j = 0; j<M; j++)
3 {rd[ tid+j ]}; // _ = tile [ tid+i ];
4 // r = 1
5 forU i in 0..M // for ( int i = 0; i<M; i++)
6 {wr[ tid ]} // tile [ tid ] = _;
```
in line 3) without awaiting the termination of the previous transpose-operation (the reads from tile in line 6), thus corrupting the data over time and possibly skewing the timing of the optimization to appear faster than it should be. We found a related data-race in [17], which reuses code from [34].

Our tool, Faial, successfully identifies the program state that triggers the data-race in Listing 2.1: when r=1 and N=2. However, state-of-the-art tools struggle to accurately analyze Listing 2.1, as evaluated in Sect. 6 (Claim 1: Test 1). Symbolic execution tools, such as [26,27], timeout for N>1, and, in general, cannot handle symbolic (unknown) bounds. GPUVerify [6], a tool based on Hoare logic, reports a false alarm: a spurious data-race when r=0 and N=1. PUG [24] incorrectly identifies the example as DRF, as its analysis appears to ignore dataraces originating from different iterations of a loop.

#### 2.2 Memory Access Protocols by Example

We now investigate the data-race in Listing 2.1 with an access memory protocol. For presentation purposes, we focus our discussion on Listing 2.1 (r.h.s.), that simplifies the l.h.s. whilst retaining the root cause of its data-race, which stems from the interaction between both loops. We discuss how we support multi-dimensional arrays, multi-dimensional thread identifiers, and arbitrary loop strides in Sect. 5. In our Coq formalism the notion of "accesses" (and their dimensions) is a parameter of the theory, thus orthogonal to the theory presented here.

Consider the execution of the end of the first iteration (r=0) and the beginning of the second (r=1) iteration of the outer-loop. In this case, the execution of the j-loop when r=0 is not synchronized with the execution of the i-loop when r=1 as there is no call to \_\_syncthreads() in between.

The access memory protocol in Listing 2.2 captures this *partial* execution from the viewpoint of array tile. By design access memory protocols over approximate kernels by abstracting away *what* data is being written to/read from an array, to focus on *where* data is being written. The protocol models the two problematic loops of Listing 2.1, *i.e.*, the j-loop when r=0 and the i-loop when r=1. The first loop reads (rd[tid+j]) from the array, while the second writes (wr[tid]) to it. Evaluation of a protocol follows the SIMT model: each thread evaluates wr[tid] by instantiating tid with their unique identifier (hereafter, an integer), *e.g.*, thread 0 yields wr[0] and thread 1 yields wr[1].

Analysis of Unsynchronized Protocols. We say that a protocol is DRF when all concurrent accesses are pair-wise DRF, *i.e.*, when issued by different threads on the same index, then neither access is a write. For instance the respective sets of concurrent accesses of threads 0 and 1 in Listing 2.2 is given below

$$\begin{array}{c} \text{tid} = 0\\ \{\text{rd}[j] \mid 0 \le j < M\} \cup \{\text{wr}[0] \} \end{array} \\ \begin{array}{c} \text{tid} = 1\\ \text{l} \text{r} \text{l} \mid 0 \le j < M \end{array} \\ \begin{array}{c} \text{tid} = 1\\ \text{l} \text{r} \text{l} \mid 0 \le j < M \end{array} \\ \begin{array}{c} \text{tid} = 1\\ \text{l} \text{r} \text{r} \mid 0 \le j < M \end{array} \\ \begin{array}{c} \text{tid} = 1\\ \text{l} \text{r} \text{r} \mid 0 \le j < M \end{array} $$

When M>1, thread 0 (l.h.s) accesses rd[1] and thread 1 (r.h.s) accesses wr[1]. Thus, there is a data-race on index 1 of the array.

A fundamental challenge of static DRF verification is how to handle loops. Symbolic execution approaches that unroll loops, *e.g.*, [26,27], cannot handle large nor symbolic iteration spaces. Static approaches that use Hoare logic, *e.g.*, [5,7,22], require user-provided loop invariants. Another approach is to reduce loops to verifying the satisfiability of a corresponding universally quantified formula, *e.g.*, [25,30]. This has the advantage of being fast and not requiring invariants. However, its previous application to GPU programming, *i.e.*, PUG, is unsound due to the interaction between barrier synchronizations and loops, *e.g.*, PUG misses the data-race in Listing 2.1. We give more details in Sect. 6.

*Our Approach.* A key contribution of our work is to identify conditions that allow a kernel to be reduced to a first-order logic formula, by precisely characterizing the effect of barrier synchronization in loops. To this end, the language of access memory protocols distinguishes syntactically between protocol fragments that synchronize from those that do not. For instance, the protocol in Listing 2.2 is identified as *unsynchronized*, as it does not include any synchronization.

In Sect. 4, we show that the DRF analysis of unsynchronized protocols can be precisely reduced to a first-order logic formula, where universally quantified formulae represent loops, thus obviating the need to unroll them explicitly. For instance, we reduce the verification of Listing 2.2 to asking whether for all M, t1, and t2, where t1 -= t2 are thread identifiers, the following holds:

$$\begin{aligned} \{\forall j\_1, i\_1, j\_2, i\_2 \colon 0 \le j\_1 < M \land 0 \le i\_1 < M \land 0 \le j\_2 < M \land 0 \le i\_2 < M \implies \\ \{\operatorname{rd}[t\_1 + j\_1] \} \quad \cup \{\operatorname{wr}[t\_1] \} \quad \operatorname{DRF} \ \operatorname{with} \end{aligned} \quad \begin{aligned} \{\operatorname{rd}[t\_2 + j\_2] \} \quad \xrightarrow{\sim} \{\operatorname{rd}[t\_2 + j\_2] \} \end{aligned}$$

This formula is *unprovable* since rd[t1 + j1] races with wr[t2] when, *e.g.*, t1 = 0, t2 = 1, j1 = 1, and M > 1. Hence, our technique flags Listing 2.2 as racy.

Analysis of Synchronized Protocols. The protocol in Listing 2.3 (left) models *all* the interactions over the shared array tile from Listing 2.1. This protocol consists of one outer loop r that contains two inner loops separated by a barrier synchronization (sync). The first inner loop writes (wr[tid]) to the array, while the second reads (rd[tid + j]) from the array.

Listing 2.3 access memory protocols (left) of array tile from Listing 2.1 and its aligned version (right).

This protocol illustrates how our language syntactically differentiates between protocols fragments that synchronize from those that do not. Concretely, our language precludes an unsynchronized loop (forU x ∈ n..m {u}) from calling sync anywhere in u, and it requires that a synchronized loop (forS x ∈ n..m {p}) includes at least one occurrence of sync. The superscript U (resp. S) stands for *s*ynchronized (resp. *u*nsynchronized). This distinction can be inferred automatically and yields a compositional analysis, as we explain below.

The behavior of synchronized loops is difficult to analyse because they may contain data-races that span more than one iteration. For instance an instruction of iteration r in Listing 2.3 may race with an instruction of iteration r+1.

*Our Approach.* In this work we show that the DRF analysis of synchronized protocols can safely be reduced to a first-order logic formula when such loops are *aligned*, *i.e.*, when there is at least one synchronization exactly before the loop and one at the end of its body. In Sect. 4.1 we show how to transform an arbitrary access memory protocol into an aligned protocol using a syntax-driven transformation technique called *barrier aligning*. Intuitively, barrier aligning normalizes loops so that they do not "leak" accesses between iterations. The right-hand side of Listing 2.3 shows the result of applying *barrier aligning* on the protocol from Listing 2.3 (left). Observe that the fragment before the aligned loop (line 1) corresponds to the unsynchronized part of the original loop (before sync). The original loop itself is rearranged so that the part succeeding sync is moved to the beginning of the aligned loop (lines 3–6). The fragment following the aligned loop (line 7) corresponds to the unsynchronized loop that appears after the sync in the original protocol.

In Sect. 4.1 we show that aligned protocols enable *compositional* verification: protocol fragments between two barriers can be analyzed independently. This compositional analysis is possible because (i) there is no causality between instructions, except through sync and (ii) aligned protocols syntactically delimit the causality induced by sync. For instance, the aligned protocol in Listing 2.3 can be reduced to analyzing the following three protocol fragments independently:

$$\text{for}^{\mathsf{U}} \, i \in 0..M \, \{\mathsf{wr}[\text{tid}]\} \qquad \text{for}^{\mathsf{U}} \, j \in 0..M \, \{\mathsf{rd}[\text{tid}+j]\}$$

$$\text{for}^{\mathsf{S}} \, r \in 1..N \, \{\mathsf{for}^{\mathsf{U}} \, j \in 0..M \, \{\mathsf{rd}[\text{tid}+j]\}; \text{for}^{\mathsf{U}} \, i \in 0..M \, \{\mathsf{wr}[\text{tid}]\}; \text{succ}\}$$

The first two protocols are handled like Listing 2.2 because they are unsynchronized. Representing a synchronized loop as a formula becomes possible when the protocol is *aligned*: both threads must share the same value for r at each iteration. Hence, we reduce the verification to asking whether for all N, M, t1, and t2 where t1 -= t2 and the following holds:

$$\begin{aligned} \forall \overline{\eta}, j\_1, i\_1, j\_2, i\_2 &\colon 1 \le r < N \choose 0 \le j\_1 < M \land 0 \le i\_1 < M \land 0 \le j\_2 < M \land 0 \le i\_2 < M\\ \implies \{\mathrm{rd}[t\_1 + j\_1] \} &\cup \{\mathrm{wr}[t\_1] \} \quad DRF \; with \, \theta \quad \{\mathrm{rd}[t\_2 + j\_2] \} \to \{\mathrm{wr}[t\_2] \} \end{aligned}$$

Our technique identifies Listing 2.3 as racy since this formula is *unprovable*, *i.e.*, rd[t1+j1] races with wr[t2] when r = 1, t1 = 0, t2 = 1, j1 = 1, N > 1 and M > 1.

#### 3 Access Memory Protocols

An access memory protocol describes the interaction between a group of threads and a single shared-memory location. A protocol records *where* in memory accesses take place, but abstracts away from *what* data is read from/written to memory. The language of protocols distinguishes between an unsynchronized protocol fragment u ∈ U, that disallows synchronization, from a synchronized fragment p ∈ S that must include a synchronization. The syntax and semantics of access memory protocols is given in Figure 2. Our operational semantics is inspired by the synchronous, delayed semantics (SDV) from Betts et al. [6], where threads execute independently and communicate upon reaching a barrier.

Hereafter, i, j, k are metavariables over non-negative integers picked from the set N. An arithmetic expression n is either: an integer variable x, an integer i, or a binary operation on integers that yields an integer.  We write n ↓ i when expression n evaluates to integer i, where evaluation is defined in the natural way. We overload the notation for Boolean expressions, *e.g.*, b ↓ true means that expression b evaluates to true.

*Unsynchronized Fragment.* A protocol u ∈ U either does nothing (skip), accesses a shared memory location o[i] (reads from/writes to index i), performs sequential composition, or loops. Figure 2 gives the semantics of unsynchronized protocols, which is parameterized by a set of thread identifiers T ⊆ N, where |T | ≥ 2.

Evaluation of an unsynchronized protocol u by a thread identifier i, written u ↓*i* P, yields a *phase*, *i.e.*, a set P ∈ P of *access values* α ∈ A. Each access value, or just access, notation i:o[j], consists of its issuing thread identifier i, an access mode o (read/write), and an index j. Protocol skip produces no accesses. A memory access o[n] evaluates the index and creates a singleton phase. Sequencing and looping are standard. Loop ranges include the lower bound and exclude the upper bound. Similarly to SDV, Rule U-par executes a copy of the unsynchronized code u for each thread i ∈ T by replacing the special variable tid by the thread identifier, u[tid := i], which results in the union of the accesses of all threads. To simplify the presentation we omit the unsynchronized conditionals, however they are included in our Coq formalism and are fully supported by Faial, see Sect. 5.

Syntax

Big-step semantics for U u ↓*i* P u ↓ S

$$\begin{array}{cccc} \mathcal{U}\text{-SKIP} & \mathcal{U}\text{-ACC} & \mathcal{U}\text{-SEQ} \\ \hline \mathsf{skip }\downarrow\_{i}\varnothing & & \overline{o[n]\downarrow\_{i}\{i:o[j]\}} & \overline{\mathit{u}\_{1}\downarrow\_{i}P\_{1}} & \mathcal{u}\_{2}\downarrow\_{i}\mathit{P}\_{2} \\ \hline \end{array}$$

$$\begin{array}{cc} \mathcal{U}\text{-FOR-2} \\ \hline (n < m) \downarrow \mathtt{true} & u[x:=n] \downarrow\_i P\_1 & \text{for}^\Downarrow \ x \in n + 1..m \ \{u\} \downarrow\_i P\_2 \\ \hline \end{array}$$

$$\begin{array}{c} \mathcal{U}\text{-PAR} \\ \hline S = \bigcup \{u[\text{tid}:=i] \downarrow\_i P\_i \mid i \in \mathcal{T} \} \\ \hline \end{array}$$

History concatenation and merging H · H H

[P1 ...P*n*] · [P*n*+1 ...P*n*+*k*]=[P1 ...P*n*+*k*] (H · [P]) ([P- ] · H- ) = H · [P ∪ P- ] · H- Big-step semantics for S p ↓ H

$$\begin{array}{ccccc} \mathcal{S}\text{-SYNC} & \mathcal{S}\text{-PAR} & \mathcal{S}\text{-SEQ} & \mathcal{S}\text{-FOR-1} \\ \hline \text{sync}\downarrow[\emptyset,\emptyset] & & u\downarrow\_{T}\,P & & p\downarrow H & q\downarrow H' \\ \hline \text{sync}\downarrow[\emptyset,\emptyset] & & & p\downarrow H\odot H' & \text{f}\text{-FOR-1} \\ \end{array} \qquad \begin{array}{ccccc} \mathcal{S}\text{-FOR-1} & \mathcal{S}\text{-FOR-1} & \mathcal{S}\text{-FOR-1} \\ & (n\geq m)\downarrow\,\text{true} & \\ \hline \text{for } \mathcal{S} & x\in n.m \;\{p\}\downarrow[\emptyset] \\ \end{array}$$

$$\frac{\frac{\text{S-FOR-2}}{\text{( $n < m$ )} \downarrow \text{true}}{\text{ }} \quad p[x := n] \downarrow H \qquad \text{for }^{\text{g}} x \in n + 1..m \text{ } \{p\} \downarrow H'} $$

Structurally well-formed protocols *swf* (p)

$$\begin{array}{ccccc} swf(u;\text{sync}) & \frac{swf(p)}{swf(p;q)} & \frac{swf(p)}{swf(u\_1;\text{for}^\\$\ x\in n.\text{.}\{p:\}a/)} \\ \text{Data-race, safe phase, and safe history} & \boxed{\alpha \# \beta} & \boxed{safe(P)} & \boxed{safe(H)} \\ \hline \frac{wr\in\{o,o'\}}{:o[k]\#\ j:o'[k]} & \frac{\forall \alpha,\beta\in P\colon-(\alpha\#\beta)}{safe(P)} & \boxed{\frac{\forall P\in H:safe(P)}{safe(H)}} \end{array}$$

#### Fig. 2. Syntax, semantics, and properties of access memory protocols.

H

U-for-1

(n ≥ m) ↓ true forU x ∈ n..m {u} ↓*i* ∅

*Synchronized Fragment.* A protocol p ∈ S may perform barrier synchronization sync, run unsynchronized code u, perform sequential composition, and loop. Figure 2 gives the semantics of a protocol, notation p ↓ H. Evaluation of a protocol p yields a *history* (ranged over by H), *i.e.*, a list of phases (P) that records how memory was accessed. We use :: as list constructor and · for the usual list concatenation operator. Histories are merged using the special -operator.

A barrier synchronization creates two empty phases, corresponding to phases before and after synchronization. Running an unsynchronized protocol yields a single phase containing all accesses performed by that protocol. Sequencing two synchronized protocols p with q merges the last phase of the former with the first phase of the latter, as these two phases run concurrently. The base case of a synchronized loop produces a singleton history containing the empty phase. Running one iteration of a synchronized loop sequences the history of the first iteration with the rest of the loop, by merging the two histories.

Next, we introduce the notion of well-formed protocols, a restriction of structurally well-formed protocols, see *swf* (p) in Figure 2. We discuss how wellformedness is enforced in Sect. 5. We write *fv*(p) (resp. *fv*(n)) for the free variables of p (resp. n).

Definition 1 (Well-formed protocol, p ∈ W). *We say that a protocol is wellformed, notation* p ∈ W*, when swf* (p)*, fv*(p) ⊆ {tid}*, and every synchronized loop executes at least one iteration.*

DRF is formalized at the bottom of Figure 2. Two accesses are in a data-race (or racy) when there exist two different threads that access the same index k, and one of these accesses is a write. Our definition does not distinguish between harmful and *benign* data races, a data-race in which both threads write the same value. Phase P is *safe* iff each pair of accesses it contains is not racy. History P is *safe* when all of its phases are safe. We say that p is DRF iff p ↓ H and *safe*(H).

#### 4 DRF-Preserving Transformations of Protocols

This section presents the main steps of the DRF analysis summarized in Figure 1: barrier aligning (Sect. 4.1) and splitting (Sect. 4.2).

This section also includes our key theoretical results. We establish that these steps preserve and reflect data-races (*i.e.*, any and all data-races are found), see Theorem 1 and Theorem 3. We make precise the notion of compositionality that makes our approach scalable in Theorem 2.

#### 4.1 Aligning Protocols

The first transformation step normalizes protocols by aligning synchronized loops, which in turn enables a form of compositional verification. The goal of the transformation is to produce protocols which belong to A, see top of Figure 3.

*Barrier aligning* (or just aligning) is performed by function *align*, given in the bottom half of Figure 3.  Aligning protocols.

aligned and synchronized protocol, and whose second element is an unsynchronized protocol. Intuitively, the pair represents a sequence which we delimitate syntactically. We note that the output of *align*, say (q, u), can be trivially made into an aligned protocol: q; u;sync. The case for synchronization is simple, *align* returns the input protocol as the first component of the pair and skip as the second component (the input protocol is already fully aligned). The case for sequence consists of the sequential composition of the pair aligned with unsynchronized code using operator (o 9).

Dealing with synchronized loops is more involved. Given a loop u1; forS x ∈ n..m {p; u2}, we produce a protocol consisting of the fragment preceding the loop and the synchronized part of its first iteration (q1), an aligned loop starting at n+1, and the unsynchronized part of its last iteration (u[x := m−1]). See Listing 2.3 for an example of protocol aligning. We note that we can always unroll the loop because the analysis only considers non-empty synchronized loops; we discuss how to enforce this assumption in Sect. 5.

We now state two fundamental properties of barrier aligning: preserving and reflecting DRF (Theorem 1), and enabling compositional verification (Theorem 2). Theorem 1 states that verifying DRF of a well-formed protocol p is equivalent to verifying DRF of its aligned counterpart.

Theorem 1 (Correctness of Align). *If* p ∈ W *and align*(p)=(q, u)*, then* p *is DRF if and only if* q; u *is DRF.*

To state our compositionality result, we introduce a language of contexts:

C ::= [ \_ ] | u;sync | p; C|C; p | C; forS x ∈ n..m {p} | p; forS x ∈ n..m {C}

Syntax

L h ::= skip | n:o[m] | h ; h | var x in n..m; h

Product of histories H ⊗ H

$$H\_1 \otimes H\_2 = \left[P\_1 \cup P\_2 \: \mid \: \left(P\_1, P\_2\right) \in H\_1 \times H\_2\right]$$

Big-step semantics h ⇓ H

skip ⇓ [∅] n ↓ i m ↓ j n:o[m] ⇓ [{i:o[j]}] h1 ⇓ H1 h2 ⇓ H2 h1 ; h2 ⇓ H1 ⊗ H2 (n ≥ m) ↓ true var x in n..m; h ⇓ [∅] (n<m) ↓ true h[x := n] ⇓ H1 var x in n + 1..m; h ⇓ H2 var x in n..m; h ⇓ H1 · H2

Projection *trace* : U→L

$$\begin{array}{cc} \mathit{trace}(o[n]) = \mathit{td:o}[n] & \mathit{trace}(\mathit{for}^{\mathsf{U}} \ x \in n..m \ \{u\}) = \mathsf{var} \ x \ \mathsf{in} \ n..m; \mathit{true}(u) \\\\ \mathit{trace}(u\_1; u\_2) = \mathit{trace}(u\_1); \mathit{trace}(u\_2) & \mathit{trace}(\mathsf{skip}) = \mathsf{skip} \\\\ \mathit{Splitting}(\mathit{protok}) & \overline{\mathit{spotocols}} \end{array}$$

$$split(p;q) = split(p) \cdot split(q)$$

$$\begin{array}{lcl} \hline t\_1, t\_2 \text{ fresh} & h\_1 = \text{trace}(u)[\text{tid} := t\_1] & h\_2 = \text{trace}(u)[\text{td} := t\_2] \\ \hline \\ \text{split}(u; \text{sync}) = [\text{var } t\_1 \text{ in } 1..|\mathcal{T}|; \text{var } t\_2 \text{ in } 0..t\_1; h\_1 ; h\_2] \\ \hline \\ \text{split}(p; \text{for}^{\text{g}} \ x \in n. m \text{ } \{q\}) & = \text{split}(p) \cdot [\text{var } x \text{ in } n. m; h \ | \text{ } h \in \text{split}(q)] \\ \hline \end{array}$$

The base cases correspond to a hole [ \_ ] or an unsynchronized protocol (followed by sync). The other cases follow the structure of access memory protocols.

Theorem 2 (Compositionality). *Let* C *be a context, s.t.* C[skip;sync] *is DRF. For all* p ∈ A*, if* p *is DRF, fv*(p) ⊆ {tid}*, then* C[p] ∈ A *and* C[p] *is also DRF.*

Compositionality allows Faial to analyze each fragment of an aligned protocol independently, by splitting the given protocol into multiple symbolic traces.

#### 4.2 Splitting Protocols into Symbolic Traces

The second verification step, *splitting*, consists in transforming an aligned protocol into *symbolic traces*, *i.e.*, symbolic representations of sets of memory accesses which occur between two synchronizations.

*Symbolic Traces.* Intuitively, symbolic traces are a thin abstraction over an SMT formula. We describe how to translate a symbolic trace to a formula in Sect. 5.

We give the syntax and semantics of symbolic traces in Figure 4. Expression skip terminates a trace. Expression n:o[m] states that thread n accesses index m with mode o. Expression h1; h2 composes two symbolic traces using operator ⊗, also given in Figure 4. Expression var x in n..m; h binds variable x in h, where variable x is an integer in the range induced from n and m. The semantics of a symbolic trace yields a history with a phase for each possible variable assignment. Expression skip yields a single empty phase. Expression n:o[m] evaluates to a singleton set that contains the access value that results from evaluating the thread-identifier expression n and the index expression m. Sequencing histories h1; h1 consists of performing the product of phases (operator ⊗), which consists of merging every phase of H1 with every phase of H2. A variable binder behaves like a skip when the range of values is empty. Otherwise, we fork two histories H1 and H2. We assign the lower bound of the set in H1, and we recursively evaluate a variable binder where we increment its lower bound in H2.

*Barrier splitting* is the transformation from aligned protocols to symbolic traces, performed via functions *trace* and *split*, defined in Figure 4. Function *trace* extracts the symbolic trace of an unsynchronized program for a single thread. Memory accesses are tagged with the owner thread tid, and unsynchronized loops are converted into variable bindings. Function *split* returns a list of symbolic traces. The case for p; q is trivial (operator · stands for list concatenation). The base case of *split* is for unsynchronized protocol fragment u, which produces a list containing a single symbolic trace. It introduces fresh variables t1 and t2 that represent two (distinct) symbolic thread identifiers. The rest of the trace consists of the trace of u instantiated to the first thread identifier t1 followed by its instantiation to the second thread identifier t2. The case for synchronized loops simply reinterprets the loop as a variable binder. Function *split* leads to an exponential blow up wrt. nesting of synchronized loops, but this has not posed problems in practice, *c.f.*, Claim 2.

*Example 1.* Let pˆ = wr[tid + 1];rd[tid + 2];sync. We have that *split*(ˆp) returns:

$$\text{var } t\_1 \text{ in } 1..|T|; \\ \text{var } t\_2 \text{ in } 0..t\_1; \\ t\_1 ; \text{var}[t\_1+1]; \\ t\_1 ; \text{rd}[t\_1+2]; \\ t\_2 ; \text{var}[t\_2+1]; \\ t\_2 ; \text{rd}[t\_2+2]$$

We show that barrier splitting preserves and reflects DRF.

Theorem 3. *Let* p ∈ A*, such that* p ↓ H1*, and* H2 = [H | h ∈ *split*(p)∧h ⇓ H]*, then safe*(H1) *if and only if safe*(H2)*.*

Hence we have established that aligning (Theorem 1) and splitting (Theorem 3) preserve and reflect data-races, *i.e.*, any and all data-races are found. Thus, the only source of approximation in our analysis stems from the inference of protocols from CUDA kernels, which we discuss in the next section. Theorem 3 highlights the compositionality of our analysis, as each symbolic trace resulting from function *split* can be analyzed independently.

#### 5 Implementation

In this section we present our tool, Faial, that implements the steps described in Figure 1. Faial takes a CUDA kernel as input and produces results that either identify the kernel as DRF or list specific data-races. In this section, we describe the implementation of the protocol inference, well-formedness checks, and transformation to SMT.

*Inference.* This step transforms a CUDA kernel into access memory protocols (one for each shared array). It uses libclang [23] to parse the kernel, a standard single static assignment (SSA) transformation to simplify the analysis of indices and arrays, and code slicing to only retain code related to *shared* array accesses. We note that Faial supports constructs of the CUDA programming model that are not directly modeled by access memory protocols, *e.g.*, unstructured loops, conditionals, function calls, and multi-dimensional arrays. To support multidimensional thread identifiers, we extend the language of protocols to support multiple thread identifiers, and adapt function *split* accordingly. The main challenges are related to loops and function calls.

Whenever possible loops are transformed to loops with a stride of 1 following ideas from loop normalization [24] and abstraction [30]. For instance, in for(int i=lb;i<ub;i+=s){S} we change the stride from s into 1 by executing the loop body S when the loop variable i is divisible by stride, *i.e.*, the loop becomes for(int i=lb;i<ub;i++) if((i+lb)%s==0){S}. Similarly, a loop ranging over powers of n, *e.g.*, for(int i=lb;i<ub;i\*=s), becomes for(int i=lb;i<ub;i++) if(powerof(i,s)){S}, where function powerof(i,s) tests whether i is a power of base s. We approximate whiles as a structured loop with an unknown upper bound.

Function calls that manipulate shared memory are uncommon in GPU programming. Additionally auxiliary functions that manipulate shared memory have a compiler annotation to inline their bodies, hence we can inline such calls easily. Faial cannot handle recursive functions, but these rarely occur in practice. Function calls that do not access shared memory are simply discarded.

*Well-Formedness.* This step ensures that kernels Faial analyzes meet the wellformedness conditions, *i.e.*, p ∈ W, including the assumptions that synchronized loops iterate at least once, see Definition 1. First, Faial annotates loops with a synchronized/unsynchronized tag according to the presence of sync in the loop body, then adjusts the precedence of sequencing to group all unsynchronized code preceding a sync or a synchronized loops. Synchronized loops of well-formed protocols cannot manipulate thread-local variables (*i.e.*, tid), an assumption shared by the CUDA programming model. Hence, Faial flags such kernels as erroneous. Next, Faial adds assertions before/after synchronized loops to check that the loop range is non-empty, *i.e.*, loops execute at least once. Similarly to loops, conditionals are tagged as synchronized or unsynchronized. Then, Faial inlines synchronized conditionals, *i.e.*, when a synchronized conditional is found, two copies of the input program are created and each copy is prefixed by a global assertion corresponding to the condition. Faial does not support synchronized conditionals that appear within synchronized loops. We have not found realworld kernels that include such a construction.

*Quantification.* This step transforms each symbolic trace (Figure 4) into an SMT formula, to check for *safety*, *c.f.*, Figure 2. The presented formalism assumes a decidable fragment. However, as CUDA programs may include multiplication in index expressions, Faial uses an undecidable logic (SMTLib's QF\_LIA). Essentially, the generated formula guarantees that the indices of array accesses are distinct when there is at least one write. We illustrate this straightforward transformation with Example 2.

*Example 2.* The formula generated from the trace in Example 1 is given below:

$$\begin{aligned} \left( \forall t\_1, t\_2 \colon 1 \le t\_1 < |\mathcal{T}| \land 0 \le t\_2 < t\_1 \land \left( \mathfrak{m}\_1 = \mathsf{w}r \lor \mathfrak{m}\_2 = \mathsf{w}r \right) \implies \\ \left( \left( \mathsf{idx}\_1 = t\_1 + 1 \land \mathfrak{m}\_1 = \mathsf{w}r \right) \lor \left( \mathsf{idx}\_1 = t\_1 + 2 \land \mathfrak{m}\_1 = \mathsf{rd} \right) \right) \\ \land \left( \left( \mathsf{idx}\_2 = t\_2 + 1 \land \mathfrak{m}\_2 = \mathsf{w}r \right) \lor \left( \mathsf{idx}\_2 = t\_2 + 2 \land \mathfrak{m}\_2 = \mathsf{rd} \right) \right) \land \left( \mathsf{idx}\_1 \neq \mathsf{idx}\_2 \right) \end{aligned}$$

where each symbolic access is translated to a conjunction representing its index (idx) and access mode (m). Observe that the formula enforces that indices idx1 and idx2 (executed by distinct threads) are different.

For multi-dimensional arrays, we generate one pair of indices per dimension, and check that at least one pair is distinct.

### 6 Experimental Evaluation

We evaluate Faial over several datasets and show how it fares against existing approaches. We structure this evaluation in three claims.

*Benchmarking Environment.* To make our evaluation reproducible, we developed a benchmarking framework to automate our experiments over the different tools and datasets. For Claim 1 and Claim 3, we designed a tool-agnostic file format for kernel functions and associated metadata (*e.g.*, expected result of DRF analysis,

Table 1. Results for Claim 1. DRF indicates that a (static analysis) tool reported a test case as DRF. NRR indicates that a (symbolic execution) tool did not report any data-race. Label *x/y* indicates that the tool reported *y* data-races, *x* of which are actual races. Label *timeout* indicates that the tool did not terminate within 90s. A test passes if the tool returns the expected result and all reported races are valid.

grid and block dimensions, and include directives). And for Claim 2, we created a tool that generates kernels according to given templates, *e.g.*, see Figure 7.

We evaluate Faial against the following verification tools: GPUVerify [5] v2018- 03-22; PUG [24] v0.2; and, GKLEE [26] and SESA [27] v3.0. Experiments for Claim 1 use an Inteli5-6500CPU, 7.7 GBRAM, andFedora 33OS,whileClaim2andClaim3 use an Intel i7-10510U CPU, 16 GB RAM, and Pop! OS.

*Excluded Tools.* We excluded ESBMC-GPU [33] and Simulee [37] from the evaluation because we were unable to get them to run satisfactorily. Both tools have rudimentary support for verifying arbitrary CUDA kernels. ESBMC-GPU did not find a single data-race in our benchmarks, while Simulee produced false alarms for every DRF-kernel given.

#### Claim 1: Correctness

We have selected a set of tricky kernels to expose false alarms and missed dataraces in Faial, GPUVerify, PUG, GKLEE, and SESA. Our results are reported in Table 1. The dataset consists of 5 tests, each consisting of two variations of the same kernel: one racy and one DRF. The racy version of Test 1 (*c.f.*, Listing 2.1) contains an inter-iteration data-races. The DRF version adds a sync after the second inner loop. Tests 2 to 4 expose various loop-related data-races. Their protocols are given in Figure 5. In the racy version of Test 2 wr[tid + 1] conflicts with wr[tid] of the first iteration. Similarly, in the racy version of Test 3, wr[tid + 1] of the last iteration races with wr[tid]. In the racy version of Test 4 the last iteration of a nested loop races with the first iteration of the following loop. Test 5 exposes the abstraction gap between kernel and access memory protocols (which abstract away array elements), see Figure 6.

Faial passes more tests than any other tool. Failed Test 5 is caused by access memory protocols abstracting away from *what* data is being read from/written

Fig. 5. Protocols for Tests 2 to 4, *c.f.*, Claim 1, where N is a free thread-global variable. Yellow shaded code only appears in the DRF version of first-iter and last-iter. Red shaded code only appears in the racy version of last-iter-first-iter (Color figure online).

Fig. 6. Kernels and protocols for Test 5 (read-index), *c.f.*, Claim 1; x becomes a free thread-local variable as protocols do not model array elements.

to arrays, *i.e.*, array elements. In each case, Faial reports one spurious data race (*0/1*). We report on performance trade-offs wrt. tracking array elements in Claim 2.

GPUVerify passes Test 5 because it tracks array elements, but fails the remaining 4 tests. Some reported false alarms are ill-formed, *e.g.*, on the racy component of Test 2, the report (0 : wr[tid]; 16 : wr[tid]) has disjoint indices.

PUG obtains the worst score amongst static tools. Notably, the tool misses a data-race in Test 1, demonstrating its unsoundness, *c.f.*, Sect. 2.1.

GKLEE and SESA timeout for tests that include loops, as the loop bounds are unknown.Both tools miss the data-race in Test 5. Symbolic tools may be able to report data-races when the bound is known, *e.g.*, timeouts start in Test 1 when the bound is at least 2, in Test 2 when the bound is at least 23, 000.

#### Claim 2: Scalability

We evaluate the scalability of our approach with a synthetic dataset that aims at demonstrating how different kernel constructs affect run time and memory usage of Faial, GKLEE, GPUVerify, PUG, and SESA. Our dataset is divided into five categories, one per syntactical construct in the language of access memory protocols, as well as conditionals, which are supported by our inference step, *c.f.*, Sect. 5. Figure 7 shows the protocols of the kernel patterns we generate in each category: (i) repeated accesses (read then write), (ii) repeated barrier synchronizations separated by writes, (iii) repeated conditionals, (iv) increasingly nested unsynchronized loops, and (v) increasingly nested synchronized loops. In each category, we vary the problem size by repeating a pattern from 1 to 50 times. Note that all kernels generated this way are DRF.

Fig. 7. Synthetic protocols generated for Claim 2. N is a free thread-global variable, and n1, n2. . . are positive integer literals.

Figure 8 shows the average run time and memory usage over five runs on logarithmic and linear scales, respectively. For each run, we set a timeout of 90s and we exclude any run that times out or reports a false alarm. Cutoffs in the memory plots are determined by the cutoffs in the run time plots.

Overall Faial is the most scalable tool. In 4 out of 5 categories, Faial has the slowest growth for all experiments, and verifies all tests within 0.46 s. In the largest problem sizes, our tool is the fastest in 3 categories (access, conditional, unsynchronized loop), 2nd for barriers, and 3rd for synchronized loops. Overall, the memory usage of Faial is competitive with other tools. Faial is the only tool with a near constant time/memory for up to 50 unsynchronized loops, indicating the scalability of reducing unsynchronized loops to universally quantified formulas. Faial only times out for kernels which consists of >17 nested synchronized loops. However such kernels are uncommon, *e.g.*, the levels of nested synchronized loops in the real-word kernels studied in Claim 3 are at most 3.

GPUVerify remains stable in the barrier and conditional categories but is affected negatively by loops and accesses. Loops are a known bottleneck in GPUVerify [2]. In the access category there is an exponential slowdown due to GPUVerify keeping track of what data is being written to/read from array.

PUG tool remains stable with the number of barrier synchronizations but is affected negatively by the number of conditionals and loops. PUG is the fastest tool with smaller inputs, but it raises false alarms in the access category, hence these measurements are omitted from the corresponding plots.

We discuss GKLEE and SESA together since SESA processes GKLEE's NVCC byte code output by concretizing variables, before passing it to GKLEE itself. There are two main factors that affect negatively these symbolic execution tools: (i) the number of loops, since they unroll each loop; and (ii) the amount of bookkeeping required to keep track of what is read from/written to memory. Figure 8 shows clear exponential curves for the access and barrier synchronization categories. Observe that these tools timeout immediately in the loop categories.

#### Claim 3: Real-World Usability

We evaluate the usability of our approach by comparing Faial with other static verification tools (GPUVerify and PUG) on real-world kernels wrt. rate of false alarm and run time. We curated a set of CUDA kernels from [2], which consists of 3 benchmark suites (totaling 227 CUDA kernels): NVIDIA GPU Computing

Fig. 8. Results for Claim 2. Run time (left plots) are given on a logarithmic scale, and memory (right plots) are given on a linear scale. Flatter and lower curve is better. Tools annotated with a triangle are excluded due to timeouts or errors.

SDK v2.0 (8 CUDA kernels); NVIDIA GPU Computing SDK v5.0 (166 CUDA kernels); Microsoft C++ AMP Sample Projects (20 kernels); gpgpu-sim benchmarks (33 kernels). All kernels are DRF and have been pre-processed by the authors of [2] to facilitate verification. Each kernel is in a distinct file, all dependencies are available, and kernels are annotated with minimal pre-conditions to allow for automatic analysis (*e.g.*, thread count is given).

(d) Run time (top) and memory usage (bottom) of true-positives. Time (resp. memory) is cropped at 10s (resp. 100MB) and plotted on a logarithmic (resp. linear) scale.

Fig. 9. Results for Claim 3, on a set of 227 DRF CUDA kernels.

As we aim to evaluate fully automatic verification of three tools, we removed code annotations (pre-conditions and loop invariants) specific to GPUVerify. Additionally, we made minor changes to some kernels to meet the limitations of the front-end of Faial and PUG. For instance we converted nested array lookups to use temporary variables and inlined functions calls that operate on arrays in 22 kernels. Another 8 kernels were modified to simplify their control flows. Our curated dataset will be included in our artifact submission.

Figures 9a, b, and c give the correctness results of Faial, GPUVerify, and PUG, respectively. Correct refers to the true-positive rate, *i.e.*, when the tool correctly identifies the kernel as DRF. False Alarm refers to the false alarm rate, *i.e.*, when the tool incorrectly identifies the kernel as racy. A kernel is Unsupported if it makes the tool crash. A Timeout occurs when the tool exceeds the limit of 60s to verify a kernel. The values shown are an average calculated over five runs. Figure 9d shows the average run time and memory usage of every true-positive report (we omit invalid reports) across the three tools.

Overall Faial has the highest rate of true-positives at 96%. Our tool is second in terms of run time and memory usage, showing a good compromise w.r.t. time and space. Faial verifies most kernels within 1s, and all kernels that need more time are only verified by Faial. GPUVerify shows lower memory usage at the cost of a higher verification run time. PUG verifies the lowest number of kernels (34.8%), as most kernels are unsupported (62.6%).

### 7 Related Work

*SMT-Based DRF Analyses.* Li and Gopalakrishnan propose a direct encoding of DRF analysis of GPU programs in SMT, with PUG [24,25]. Both PUG and Faial follow a similar approach of barrier splitting: having a symbolic representation of a canonical interleaving, and dividing up the analysis over barrier intervals. The two major distinctions are that (1) PUG misses inter-thread data-races in synchronized loops, *e.g.*, Listing 2.1, and (2) the algorithms of PUG are unspecified and lack soundness proofs. In [24, Sect. 6.3] the authors identify the challenge of detecting inter-thread data-races, but do not elaborate a solution. Ma *et al.* [30] present a similar technique to detect data-races and deadlocks in OpenMP programs (CPU-based parallelism). However, their work does not guarantee DRF, and they do not formalize their algorithms. In [8], Prasanth *et al.* propose a polyhedral encoding of DRF for OpenMP programs, which is only applicable to programs with affine array accesses. However the prevalence of linearized array expressions in GPU kernels is known to stump polyhedral analysis [16].

*Hoare-Logic-Based DRF Analyses.* The main drawback of Hoare-logic based tools is their high rate of false alarms. They also require code annotations from a concurrency expert to handle loops. GPUVerify [2,3,5,6,12] can verify CUDA and OpenCL kernels using Boogie [4] as a backend. GPUVerify also relies on a two-thread abstraction (pen and paper proof)—in this paper, we present the first *machine-checked* proof of the two-thread abstraction idea. VeriCUDA [20,21] focuses on reasoning about the functional correctness of GPU programs using Hoare-logic. In [22] the authors extend VeriCUDA to proving DRF. In a similar vein, VerCors [7] uses separation logic to prove the functional correctness and DRF of GPU kernels. Both VeriCUDA and VerCors expect a tool-specific language, hence cannot handle real-world kernels directly.

*Data-Race Finders.* These include dynamic data-race detection, symbolicexecution, and model-checking. Such techniques are better suited for highly detailed analysis in smaller kernels, and typically are unable to prove DRF. Dynamic data-race detection executes a kernel to find data-races on a fixed input, *e.g.*, [14,18,19,28,32,38,39]. This technique only reports real data-races, but suffers from a slowdown of at least 10× compared to the non-instrumented program, and requires the kernel input data, which might be unavailable or unknown. Symbolic execution and model checking have been extended to detect data-races [10,11,26,33,37]. These techniques do without the kernel input data and can detect more data-races than dynamic data-race detection.

*Miscellaneous.* Ferrel *et al.* introduce a machine-checked formalism to reason about the semantics of CUDA assembly [15]. Dabrowski *et al.* mechanize the DRF-analysis of multithreaded programs [13]. Muller and Hoffmann present a logic to reason about the evaluation cost of CUDA kernels [31].

Other behavioral types have been used to verify parallel and multithreaded systems that communicate via message-passing [29,35,36]. However these do not capture shared memory (only message-passing), thus cannot address data-races.

#### 8 Conclusion

We tackle the problem of statically checking DRF in GPU kernels, with a new family of behavioral types, *i.e.*, access memory protocols. We provide a novel compositional analysis of access memory protocols, along with fully mechanized proofs and an implementation. Our evaluation explores challenging and diverse benchmarks (229 real-world and 258 synthetic kernels) to demonstrate that our approach is more precise (false alarms and missed alarms), scalable (time/memory growth), and usable (real-world kernels correctly verified) than other tools.

Acknowledgements. We thank Rumyana Neykova, Stephen Chang, and the anonymous reviewers for their insightful feedback on earlier versions of this work.

#### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### **GENMC: A Model Checker for Weak Memory Models**

Michalis Kokologiannakis(B) and Viktor Vafeiadis

MPI-SWS, Kaiserslautern, Germany<EMAIL_ADDRESS>
**Abstract.** GenMC is an LLVM-based state-of-the-art stateless model checker for concurrent C/C++ programs. Its modular infrastructure allows it to support complex memory models, such as RC11 and IMM, and makes it easy to extend to support further axiomatic memory models.

In this paper, we discuss the overall architecture of the tool and how it can be extended to support additional memory models, programming languages, and/or synchronization primitives. To demonstrate the point, we have extended the tool with support for the Linux kernel memory model (LKMM), synchronization barriers, POSIX I/O system calls, and better error detection capabilities.

#### **1 Introduction**

For any software developer or verification engineer, it is no news that concurrent programming is difficult, that concurrent software is often buggy, and that therefore verification of concurrent programs has attracted a lot of research interest. Within the verification community at least, it is also common knowledge that verification of concurrent programs is challenging because of the huge number of interleavings of the threads comprising a concurrent program.

What has changed in the last decade, however, is the importance of *weak memory consistency* [6,11,13,14,21,25,32,36,40,41] as a key factor contributing to the complexity of concurrent programming. Weak memory models do not simply increase the number of thread interleavings; they also confound programmers, who typically have little intuition about how to reason about the behaviors induced by these additional interleavings.

GenMC is a fully automatic verification tool meant for such programmers. It is a *stateless model checker* (SMC) [23] that can be used to verify bounded clients of intricate concurrent algorithms, such as implementations of synchronization primitives and shared data structures (e.g., queues, sets, and maps). It accepts as input a C/C++ program using C/C++11 atomics and/or the concurrency primitives from the pthread library, and reports any data races, assertion violations, or other errors encountered. By default, verification is performed with respect to the RC11 memory model [32], but there are command line options for selecting other models, such as IMM [41] and LKMM [10].

Since the theory underlying GenMC has already been published elsewhere [28,29,31], this paper focuses on the overall design of the tool and on various enhancements implemented in it. Our main design goals of GenMC were:

**Usability:** The tool should provide useful and readable error messages.

**Extensibility:** The tool should be easily adaptable to support additional models and synchronization primitives, and to tweak its performance. Extensibility is key to achieving the other goals, since it allows gradual improvements to the tool in terms of coverage, performance, and error detection/reporting.

These goals are achieved by a combination of techniques:

GenMC's core SMC algorithm [29,31] is parametric in the choice of the memory model—subject to a few minimal constraints (see Sect. 2).

The implementation is based on LLVM, a versatile intermediate language for multiple programming languages.

GenMC follows a modular architecture minimizing dependencies across components (see Sect. 3), which makes it easy to extend with support for additional memory models (Sect. 4) and synchronization primitives (Sect. 5).

Its architecture contains hooks to provide fast approximate consistency checks, which are exploited by the memory model implementations (see Sect. 4).

GenMC contains a number of optimizations that provide noticeable performance benefits on common workloads (Sect. 7).

GenMC keeps additional metadata so as to present error messages in terms of variables names appearing in the source code (Sect. 6).

GenMC has been applied to a few industrial settings, where it has found bugs and/or verified bounded correctness of concurrent libraries [39].

*Related Work.* There has been extensive work on SMC, with most tools focusing on sequential consistency [7,8,15,23,37]. Tools that support weak memory models include CDSChecker [38] that verifies C/C++11 programs under the original C11 memory model, Tracer [5] that verifies C/C++11 programs under the RA model, RCMC [27] that verifies C programs under RC11 [32], and Nidhugg [1,2,4,12,13] that supports SC, TSO, PSO and provides limited support for the POWER and ARMv7 memory models. In contrast to GenMC, which uses the same core algorithm for all memory models, Nidhugg uses multiple different algorithms depending on the memory model.

There has also been work on adapting SAT/SMT-based bounded model checking (BMC) techniques for weak memory models [9,17,22]. Dartagnan [22] is a BMC tool that is parametric in the choice of the memory model, as it accepts the memory model as input in the litmus format [11].

#### **2 Memory Model Requirements**

GenMC's core algorithm is parametric in the choice of the memory model provided that it can be expressed in an axiomatic way and satisfies a few basic requirements that we describe below.

Axiomatic memory models represent the executions of a concurrent program as *execution graphs* [11] that satisfy a certain consistency predicate. Execution graphs comprise a set of *events* (nodes) that represent the individual memory accesses performed by the program, and some relations on these events (edges). Example relations included in all memory models are the *preserved program order* (ppo) and *reads-from* (rf) relations: ppo relates events in the same thread that are ordered (e.g., by a chain of dependencies or a fence), while rf relates writes to reads reading from them.

GenMC can be used to verify programs under such a model as long as the model's consistency predicate fulfills the following requirements:

These requirements are satisfied by almost all axiomatic memory models (e.g., TSO [40], PSO [42], Power [11], ARMv7 [11], ARMv8 [21], RC11 [32], IMM [41], LKMM [10]). The only known axiomatic memory model that does not satisfy these requirements is the original formulation of the C/C++11 model [13], which has been criticized for its flaws [32,43].

Although these requirements cannot be satisfied by more advanced memory models that cannot be defined in an axiomatic fashion (e.g., [14,24,25,33]), there is ongoing work to support such a model.

#### **3 Tool Architecture**

Verification with GenMC comprises three stages (cf. Fig. 1, left).

The first stage invokes clang to compile the source C/C++ program to LLVM-IR. To accommodate programs written in different languages, GenMC also accepts LLVM-IR as its input, provided that it adheres to certain conventions about thread creation.

The second stage transforms the LLVM-IR code to make verification more effective by replacing spinloops by assume statements, bounding infinite loops,

**Fig. 1.** Overal architecture (left) and dynamic components (right).

and performing sound optimizations, such as dead allocation elimination. It also collects additional debugging information to enable better error reporting.

The third stage invokes the verification procedure, which explores all the executions of the program. If an error is found during this stage, the execution is halted and an error report is produced (see Sect. 6).

The architectural subcomponents of this stage are depicted in Fig. 1 (right). At the center lies the verification *driver*, which owns three independent components: an execution graph, a work set, and an interpreter.

The *execution graph* records the visited execution trace, and has routines for calculating various relation on the graph, such as the happens-before relation. As each memory model comprises different relations, the execution graph contains multiple calculators that are dynamically populated when the graph is created, and the consistency predicate is calculated as a fixpoint of all the selected relations, whenever this is requested by the driver.

The *work set* records alternate options for later exploration, the precise definition of which can depend on the memory model.

The *interpreter* merely executes the user program, notifying the driver each time a "visible" action (e.g., a load/store to shared memory) is encountered. It is directly based on the LLVM interpreter lli [35], and is the only part of our code base that heavily depends on LLVM. In turn, the driver modifies accordingly the execution graph, possibly pushes some items to the work set, and returns control back to the interpreter, along with a value that will be used by the interpreter, if necessary (e.g., in the case of a load). In effect, the driver and the interpreter can be thought of as *coroutines* [18]. The interpreter calls the driver whenever it encounters a visible action or finishes running a thread, while the driver monitors execution consistency, schedules the program threads, and discovers alternative exploration options, which are pushed to the work set.

The aforementioned components are all parameterized by the user's configuration options. The most important of these options is the memory model, which also determines whether dependencies between instructions should be tracked by the interpreter and stored in the execution graph. Another important option is when and how consistency is to be calculated. Since checking consistency at each step can be expensive for some memory models, it is possible to provide an approximate consistency check to be applied at each step and only perform the full consistency check once an error is detected.

To facilitate memory-model-specific optimizations, the driver is overridden for each memory model. Each instance sets up the (approximate) consistency checks and can provide specialized methods for crucial verification components.

#### **4 Supporting New Memory Models**

Adding support for a new memory model entails three basic steps.

First, one has to provide definitions for any memory model primitives that the interpreter should intercept beyond those already supported (i.e., plain memory accesses and C/C++11 atomics). One can either provide a header file mapping these primitives to LLVM-IR instructions or create special event types for them.

Second, one has to provide calculators for the memory model's relations that are not already supported by GenMC. Depending on the memory model, this step may require a variable amount of effort, but it effectively boils down to translating relational calculations into matrix operations.

Third, one can also provide approximations for the consistency checks. Such approximations entail storing crucial information about a memory model's relations as vector clocks (e.g., causally preceding events, for some notion of causality), but deciding what to store is up to the user to decide and encode. Importantly, GenMC's performance depends not only on the calculators provided in the previous step, but also on the effectiveness of the approximations, which quickly filter out inconsistent exploration options. For instance, GenMC's current RC11 driver treats SC accesses as release-acquire (RA) accesses (the consistency of which can be quickly determined), and only checks for full RC11 consistency when an error has been triggered, a heuristic that seems to work well in practice for programs that have both SC and non-SC accesses.

All in all, adding support for a memory model largely depends on the complexity of the model. Adding support for models like SC or RA is trivial, since such accesses are already supported as part of RC11 and IMM. In contrast, adding support for LKMM involved much more work, as we describe below.

#### **4.1 Supporting the Linux Kernel Memory Model (LKMM)**

LKMM [10] is a memory model that encompasses a variety of different architectures supported by the Linux kernel. As LKMM differs substantially from RC11 and IMM, supporting it required all steps described above as well as a few other engineering decisions, the most important of which are discussed below.

First, LKMM uses complex constraints for checking consistency of an execution graph. As repeatedly calculating these constraints can be expensive, we designed approximations for them. Unlike most other memory models, LKMM does not define a suitable happens-before relation for checking coherence and detecting races. (Its hb relation cannot be used for this purpose.) We thus defined a custom happens-before relation that can rule out inconsistent executions very quickly, and use it to approximate coherence and race detection checks.

Second, although LKMM dictates that non-atomic accesses (called plain in LKMM's jargon) only conditionally contribute to ppo, we incorporate such accesses in GenMC's ppo (thus arriving at a stronger notion of ppo), mostly for technical reasons. Specifically, the calculation of dependencies between only non-plain accesses is difficult because each non-plain access in the source-code level may map to several plain and non-plain accesses in LLVM-IR level.

To increase confidence in our implementation, we ran all litmus tests distributed along with LKMM as part of the Linux kernel (32 tests in total), and compared our results with the results of the Herd [11] memory model simulator. Both tools explored the same number of executions for all tests.

In addition, we extracted some manually written tests from LKMM's supplementary repository [34] (categories atomic and kernel). We picked these categories as they contain tests written in C pseudocode (thus easily translatable to C) and do not contain tests with plain accesses, which, as described, GenMC treats slightly differently from what LKMM dictates. In total, these categories amount to another 84 tests, from which we excluded two tests containing unsupported primitives, one test for which Herd did not terminate within 42 h, and three tests that cannot be cleanly translated to C. Out of the remaining 78 tests, GenMC explores the same number of executions for 75 tests. The discrepancies observed in the three remaining tests are due to the different way the two tools produce and calculate dependencies. (In GenMC, control dependencies extend to all subsequent memory accesses of the same thread, whereas in Herd they extend only to the merge point of a conditional statement.)

We note that Herd took about 18 min to run all the above tests, while GenMC needed less than 2 s.

#### **5 Supporting New Languages and Libraries**

Supporting additional programming languages is straightforward as long as they can be compiled to LLVM. This was, for example, the case when we extended GenMC to accept C++ (the initial version accepted only C input). All we had to do was to create stub header files for the C++ library, and to extend the interpreter to recognize the memory (de)allocation calls generated by clang.

Supporting different runtime environments (e.g., JVM bytecode) requires constructing a new interpreter for the desired runtime system that calls the driver whenever a visible action is encountered. In addition, since the driver and the interpreter communicate using the LLVM type information, it may be necessary to add a translation layer between the interpreter(s) and the driver.

Supporting new concurrency libraries requires localized changes. If the library's semantics can be implemented in terms of memory accesses, one has to construct an appropriate header file or extend the interpreter to provide the mapping from library calls to the relevant memory access events. If this is not possible and/or if native support for a library is desirable (e.g., for performance reasons), then the execution graph has to be extended with new kinds of events and the consistency checks have to be adapted accordingly.

Next, we present two such library extensions, one mapping its calls to individual memory accesses, and the other creating new kinds of events.

*System Calls.* As part of [26], we extended GenMC with support for system calls, such as open(), close(), read() and write(), which can be modeled by making multiple primitive calls (reads and writes) to a different address space.

There are two ways one could implement these system calls: either by providing an actual implementation (which would then be compiled to LLVM-IR) or by adding support in the interpreter to internally implement those calls and communicating multiple times with the driver.

We preferred the latter solution because it is more portable. An external implementation would have to be manually ported whenever support for more languages is added. In contrast, the internal implementation needs no change. Further, even if a new interpreter for a different runtime system is added, it should be simple to decouple the system calls from the interpreter, and have the different runtime systems share the infrastructure that handles system calls.

*Barriers. N*-way barriers are a widely-used synchronization primitive. They have two functions: barrier init and barrier wait. The former initializes a barrier object with the number of threads that will rendezvous at the barrier, while the latter is called every time a thread reaches the barrier. A thread that is calling barrier wait blocks until the initially specified number of threads reaches the barrier, at which point all threads will be simultaneously unblocked, and the barrier value will reset to the one specified with barrier init.

Barriers can be straightforwardly implemented with a shared variable counting the number of threads that have called barrier wait. But doing so yields poor model checking performance. For *N* threads calling barrier wait, there are *N*! possible orders in which they can update the shared counter, thus crippling the performance of the tool. Tracking the order of these updates is not only expensive but also completely unnecessary. For many real-world use cases of barriers (e.g., scatter-gather workloads), the order in which different threads reached the barrier is irrelevant, and the thread that reached last unimportant.

We leverage this intuition and provide built-in support for barrier init and barrier wait calls that does not track the relative ordering among barrier wait calls synchronizing with one another, thereby achieving an exponential reduction in verification time. Concretely, in the simple program below where *N* threads execute barrier wait concurrently, GenMC explores only one execution instead of *N*! executions:

```
barrier wait(); ... barrier wait();
```
Our extension is called BAM (Barrier-Aware Model-checking) and is detailed and evaluated in a companion paper [30].

#### **6 Error Detection and Reporting**

GenMC detects a number of different kinds of errors: violations of user-supplied regular and persistency assertions, data races, memory errors and simple cases of termination errors. It reports errors by printing an offending execution graph and highlighting the event(s) that caused the violation. Upon request, GenMC can also print a total ordering of the instructions that lead to the violation, or produce the offending execution in the DOT graph description language.

*Persistency Errors.* To verify persistency properties of programs performing file I/O, we allow user programs to contain a special *recovery routine* [26], which would typically check some invariant over the persisted state.

When such a routine is present, GenMC simulates all possible ways in which the program could have crashed because of a power failure, executing the recovery routine at the end of every such execution. Of course, to avoid the obvious state-space explosion, the simulation of all the possible failures is done in an optimized fashion, driven by the memory accesses of the recovery routine.

The performance of GenMC when verifying persistency properties of programs under the ext4 filesystem has been evaluated at [26].

*Memory Errors.* Memory errors refers to accessing uninitialized, unallocated or deallocated memory. In models like RC11 [32], reasoning about memory safety can be tricky at times, as demonstrated by the example below:

*p* := **alloc**(); ∗*p* :=rlx 42; *x* :=rlx 1; **if** *x* = 1 **then** *a* :=rlx *p*; *b* :=rlx ∗*a*;

This example is erroneous under RC11 because the allocation of *p* is not guaranteed to have propagated to the second thread by the time it is dereferenced. (Since all accesses are relaxed, there is no synchronization between the threads.)

GenMC also accounts for more complicated scenarios such as *p* being concurrently freed when accessed, *p* being freed twice, or *p* being the address of a local (stack) variable that might not be alive when accessed.

*Refining Error Reports.* It is often useful to refine the error reporting. For example, in memory models that treat data races as errors (such as RC11), GenMC by default detects data races and reports them as errors. This, however, can be costly in terms of verification time or even prohibit the verification of programs that use compiler/custom primitives to access shared memory, as such programs would almost certainly be considered racy.

To deal with such cases, GenMC provides switches that disable race detection and refine the range of errors that will be reported to the user. Switches of the latter kind are especially useful when dealing with programs that contain system calls. By default, when such system calls fail, GenMC reports an error, which is inconvenient for programs that contain proper error handling, as some system errors are rather benign (e.g., a file not existing). With the appropriate switch, in case of system errors, an appropriate value is written in errno, as dictated by the POSIX standard.

*Case Study.* We demonstrate the error reporting capabilities of GenMC with a real use case. We consider a flat-combining queue [19] that has been proposed to be ported in Rust's crossbeam library.

This queue serves as a nice case study for a couple of reasons. First, it contains loops that can diverge, and so its verification requires loop bounding, which GenMC can do automatically. Second, it is implemented using compiler primitives for concurrent accesses, and so its verification requires disabling race detection. Third, while experimenting with it, we found it to be buggy.

The error report produced by GenMC can be seen in Fig. 2. The error is quite intricate: it requires three threads to manifest, each of which executes a large number of instructions. The error is due to an ordering bug (relaxed accesses are used instead of release/acquire), which demonstrates the need for model checking tools that handle weak memory models.

```
Error detected: Attempt to read from uninitialized memory!
Event (3, 63) in graph:
<-1, 0> main:
<0, 1> thread_n:
  (1, 18): Urel (cmb.queue, 0) [(0, 36)] L.169: combiner.c
  (1, 19): Urel (cmb.queue,<PHONE_NUMBER>) L.169: combiner.c
  (1, 96): Racq (m.msg._meta.next,<PHONE_NUMBER>) [(2, 26)] L.228: combiner.c
  (1, 112): Wrlx (cmb.takeover,<PHONE_NUMBER>) L.158: combiner.c
<0, 2> thread_n:
  (2, 26): Wrel (m.msg._meta.next,<PHONE_NUMBER>9592) L.167: combiner.c
<0, 3> thread_n:
  (3, 18): Urel (cmb.queue,<PHONE_NUMBER>) [(1, 19)] L.169: combiner.c
  (3, 19): Urel (cmb.queue,<PHONE_NUMBER>) L.169: combiner.c
  (3, 50): Rrlx (cmb.takeover,<PHONE_NUMBER>) [(1, 112)] L.87: combiner.c
  (3, 63): Racq (m.msg._meta.next, 0) [BOTTOM] L.187: combiner.c
Number of complete executions explored: 2795
Number of blocked executions seen: 6001
Total wall-clock time: 2.12s
```
We note that the error report contains helpful debugging information, such as the names of variables accessed (e.g., m.msg. meta.next) and the values read/written. To display this information, GenMC maintains a mapping from addresses to program variables using the additional debugging information collected in the "Transformation" phase.

#### **7 Other Performance Enhancements to GenMC**

In this section, we briefly discuss two recent changes to the driver to optimize its performance for certain kinds of programs.

*Symmetry Reduction.* Many programs, such as the flat-combining queue of Sect. 6, have a symmetric structure: each thread runs the same code. In such cases, many execution graphs are equivalent up to some thread relabeling—a property that is exploited by *symmetry reduction* (SR) [16,20].

We implemented a simple SR algorithm that detects whether multiple threads with the same code are spawned with no intervening memory accesses, and avoids exploring executions for which a symmetric one (by relabeling such threads) has already been explored. This can yield exponential improvements. For example, a program with *N* threads incrementing a shared variable atomically has *N*! executions; employing SR yields only one execution. With SR, the verification time of the corrected flat-combining queue drops from 15 s to 2.5 s.

To further demonstrate the benefits of SR, we measured the performance of GenMC with and without SR on some realistic lock implementations adapted from the literature. The results can be seen in Table 1. All reported times are in seconds, unless mentioned otherwise. We ran both GenMC versions three times for each benchmark, with an increasing number of threads each time (the initial thread number for each benchmark is provided in the second column). As it can be seen, SR leads to a significant performance improvement in all cases.

**Table 1.** Testing lock implementations (1 h timeout; 4 GB memory limit)

*Lock-Aware Partial Order Reduction.* A common problem with locking is that of false sharing, where *N* threads contend to acquire the same lock even if it is unnecessary for correctness. In such cases, GenMC's partial order reduction algorithm [29] will explore all *N*! orders in which the lock can be acquired even though they all lead to the same outcome.

We have implemented *lock-aware partial order reduction* (LAPOR) [28], an enhancement to partial order reduction that does not track ordering among locks unless their critical regions have conflicting accesses, in which case the lock ordering is induced from the ordering among those accesses. With LAPOR, GenMC achieves exponential improvements in lock-based implementations of concurrent libraries that have false sharing, such as search trees with coarsegrained or hand-over-hand locking. LAPOR has been evaluated at [28].

#### **8 Conclusion**

We presented GenMC, a state-of-the-art stateless model checker that can be used to verify consistency and persistency properties of C/C++ programs. We described its architecture, and how its modular design can be leveraged to account for new features and memory models. To widen the applicability of GenMC, we have extended it with support for LKMM, basic system calls and additional synchronization primitives. We have also improved its performance with optimizations, such as symmetry reduction and lock-aware partial order reduction that can exponentially decrease its search space.

In the future, we plan to implement a DSL for memory models, so as to make it easier to extend GenMC with new models and quickly tweak their approximation strategies. We are also planning to incorporate further optimizations into the tool to enable more effective verification of lock-free algorithms.

**Acknowledgements.** We thank the anonymous reviewers for their feedback. This work was supported by a European Research Council (ERC) Consolidator Grant for the project "PERSIST" under the European Union's Horizon 2020 research and innovation programme (grant agreement No. 101003349).

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

**Hybrid and Cyber-Physical Systems**

## **Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming**

Qiuye Wang1,2(B) , Mingshuai Chen3(B) , Bai Xue1,2(B) , Naijun Zhan1,2(B) , and Joost-Pieter Katoen3(B)

1 SKLCS, Institute of Software, CAS, Beijing, China 2 University of Chinese Academy of Sciences, Beijing, China<EMAIL_ADDRESS>3 RWTH Aachen University, Aachen, Germany<EMAIL_ADDRESS>
**Abstract.** A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over the infinite time horizon. We present a novel condition on barrier certificates, termed the *invariant barrier-certificate condition*, that witnesses unbounded-time safety of differential dynamical systems. The proposed condition is by far the least conservative one on barrier certificates, and can be shown as the weakest possible one to attain inductive invariance. We show that discharging the invariant barrier-certificate condition thereby synthesizing invariant barrier certificates—can be encoded as solving an *optimization problem subject to bilinear matrix inequalities* (BMIs). We further propose a synthesis algorithm based on differenceof-convex programming, which approaches a local optimum of the BMI problem via solving *a series of convex optimization problems*. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divide-and-conquer fashion. We present a weak completeness result of our method, in the sense that a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify safety of the system. Experimental results on benchmark examples demonstrate the effectiveness and efficiency of our approach.

#### **1 Introduction**

Hybrid systems are mathematical models that capture the interaction between continuous physical dynamics and discrete switching behaviors, and hence are widely used in modelling cyber-physical systems (CPS). These CPS may be

This work has been partially funded by the NSFC under grant No. 61625206, 61732001, 61872341, and 61836005, by the ERC Advanced Project FRAPPANT under grant No. 787914, and by the CAS Pioneer Hundred Talents Program.

complex and safety-critical, with sensitive variables of the environment in its sphere of control. Everyday examples include process control at all scales, ranging from household appliances to nuclear power plants, or embedded systems in transportation domain, such as autonomous driving maneuvers in automotive, aircraft collision-avoidance protocols in avionics, or automatic train control applications, as well as a broad range of devices in health technologies, such as cardiac pacemakers.

The safety-critical feature of these CPS, with increasingly complex behaviors, has initiated automatic safety or, dually, reachability verification of hybrid systems [1,15]. The problem of reachability verification is undecidable in general [1], albeit with decidable families of sub-classes (see, e.g., [2,16–18,31]) identified in the literature. The hard core of the verification problem lies in reasoning about the continuous dynamics, which are often characterized by ordinary differential equations (ODEs). In particular, when nonlinearity arises in the ODEs, the explicit computation of the exact reachable set is usually intractable even for purely continuous dynamics [49].

Therefore in the literature, a plethora of approximation schemes, as surveyed in [15], for reachability analysis of hybrid systems has been developed, including an invariant-style reasoning scheme known as *barrier certificate* [41]. A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set, thereby witnessing safety of hybrid systems possibly over the infinite time horizon. A common way to synthesize barrier certificates is to reduce the condition defining barrier certificates to a numerical optimization or constraint solving problem. There is, however, a trade-off between the expressiveness of the barrier-certificate condition and the efficiency in discharging the reduced constraints. Hence, to enable efficient algorithmic synthesis of barrier certificates via, e.g., linear programming (LP), second-order cone programming (SOCP), semidefinite programming (SDP) and interval analysis [11,30], the general condition on inductive invariance (that a barrier certificate defines an invariant, see [8,51]) has been strengthened into a spectrum of different shapes, e.g., [8,29,51,60,62]. It has been, nevertheless, a long-standing challenge *to find a barrier-certificate condition that is as weak as possible while admitting efficient synthesis algorithms*.

In this paper, we present a new condition on barrier certificates, termed the *invariant barrier-certificate condition*, based on the sufficient and necessary condition on being an inductive invariant [36]. Our invariant barrier-certificate condition is by far, to the best of our knowledge, the least conservative one on barrier certificates, and can be shown as the weakest possible one to attain inductive invariance. We show, by leveraging Putinar's Positivstellensatz [32], that discharging the invariant barrier-certificate condition —thereby synthesizing invariant barrier certificates— can be encoded as solving an optimization problem subject to *bilinear matrix inequalities* (BMIs). We further show that general bilinear matrix-valued functions can be decomposed as a difference of two psd-convex (extension of convexity to matrix-valued functions) functions using eigendecomposition, thus resulting in a synthesis algorithm as per *difference-ofconvex programming* (DCP) [33,52], which solves a series of convex sub-problems (in the form of *linear matrix inequalities* (LMIs)) that approaches (arbitrarily close to) a local optimum of the BMI problem. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divideand-conquer fashion. We present a weak completeness result of our method, in the sense that a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify the system's safety. A similar result on completeness is previously provided only by symbolic approaches, yet to the best of our knowledge, not by methods base on numerical constraint solving, e.g., [4,60,61]. Experiments on a collection of examples suggested that our invariant barriercertificate condition recognizes more barrier certificates than existing conditions, and that our DCP-based algorithm is more efficient than directly solving the BMIs via off-the-shelf solvers.

Due to space restrictions, proofs and benchmark details have been omitted; they are found in an extended version of this paper [57].

#### **2 A Bird's-Eye Perspective**

We use the following example to give a bird's-eye view of our approach.

*Example 1 (* overview [11]*).* Consider the following continuous-time dynamical system modelled by an ordinary differential equation:

$$
\dot{\mathbf{x}} = \begin{pmatrix} \dot{x}\_1 \\ \dot{x}\_2 \end{pmatrix} = \begin{pmatrix} x\_1 + x\_2 \\ x\_1 x\_2 - 0.5 x\_2^2 + 0.1 \end{pmatrix}.
$$

The verification obligation is to show that the system trajectory originating from any state in the initial set X0 = {**x** | I(**x**) ≤ 0} with I(**x**) = x2 1 + (x2 − 2)2 − 1 will never enter the unsafe set Xu = {**x** | U(**x**) ≤ 0} with U(**x**) = x2 + 1. -

A barrier certificate satisfying our condition in Definition 4 serves as an inductive invariant that suffices to isolate the unsafe region Xu from the set of reachable states from X0, thereby proving safety of the system over the infinite time horizon. To this end, we proceed in the following steps.

**1) Encode as Sum-of-Squares (SOS) Constraints.** We set a (polynomial) barrier-certificate template B(**a**, **x**) = ax2 with unknown coefficient a ∈ R. According to Theorem 1, we only need to consider Lie derivatives up to order NB,*f* = 1, i.e., L0 *f* B(**a**, **x**) = ax2 and L1 *f* B(**a**, **x**) = a(x1x2 − 0.5x2 2 + 0.1).

By Theorem 5, B(**a**, **x**) is an invariant barrier certificate if there exists a polynomial v(**x**), SOS polynomials σ(**x**), σ (**x**) and a constant > 0 such that

$$-\underbrace{ax\_{B}+\sigma(\mathbf{x})\underbrace{\left(x\_{1}^{2}+(x\_{2}-2)^{2}-1\right)}\_{\mathcal{I}}}\_{\mathcal{L}\_{f}^{1}B},\tag{1.1.\text{initial}}$$

$$\underbrace{-a\underbrace{\left(x\_{1}x\_{2}-0.5x\_{2}^{2}+0.1\right)}\_{\mathcal{L}\_{f}^{1}B}+v(\mathbf{x})\underbrace{ax\_{2}}\_{\mathcal{L}\_{f}^{0}B},\tag{1.2.\text{Lioconsecution}}\tag{1.2.\text{Lioconscection}}}$$

are SOS polynomials. We set = 0.01 in this example.

**2) Reduce to a BMI Optimization Problem.** Observe that the above SOS constraints can be formulated as BMI constraints. For instance, let us assume that (1.2) is an SOS polynomial of degree at most 2 and v(**s**, **x**) = s0+s1x1+s2x2 is a template polynomial with unknown coefficients **s**. Then constraint (1.2) is equivalent to the BMI constraint

$$\mathcal{F}\_2(\mathbf{a}, \mathbf{s}) = -\begin{pmatrix} -0.1a & 0 & 0.5as\_0 \\ 0 & 0 & 0.5(as\_1 - a) \\ 0.5as\_0 \ 0.5(as\_1 - a) & as\_2 + 0.5a \end{pmatrix} \preceq 0$$

meaning that the bilinear matrix (LHS of ) is negative semidefinite. Note that the bilinearity arises due to the coupling of the unknown coefficients **a** and **s**.

Constraints (1.1) and (1.3) can be reduced to BMI constraints in an analogous way1, yielding F1 and F3. It then follows that, to solve the SOS constraints, we need to find a feasible solution (**a**, **s**) such that2

$$\mathcal{F}\_1(\mathbf{a}, \mathbf{s}) \preceq 0 \land \mathcal{F}\_2(\mathbf{a}, \mathbf{s}) \preceq 0 \land \mathcal{F}\_3(\mathbf{a}, \mathbf{s}) \preceq 0. \tag{2}$$

To exploit well-developed optimization techniques, the feasibility problem (2) is transformed to an optimization problem subject to BMI constraints:

$$\begin{array}{ll}\underset{\lambda,\mathbf{a},\mathbf{s}}{\text{maximize}} & \lambda\\\text{subject to} & \mathcal{B}\_{i}(\lambda,\mathbf{a},\mathbf{s}) \triangleq \mathcal{F}\_{i}(\mathbf{a},\mathbf{s}) + \lambda I \preceq 0, \quad i = 1,2,3\end{array} \tag{3}$$

where I is the identity matrix with compatible dimensions. Note that problem (2) has a feasible solution if and only if the optimal value λ∗ in (3) is non-negative.