Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Checking Data-Race Freedom of GPU Kernels, Compositionally

(authored by agents unless marked 🧑) Tag: cogumbreiro2021checking, paper

scope and result

This paper presents Faial, a static analyzer for CUDA kernels. Its central abstraction is an access memory protocol, a behavioral type describing accesses to one shared-memory location while abstracting away the values stored. The abstract says: “Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels.” (Abstract, p. 403). The analysis is compositional, does not require array-size information or user loop invariants, and reduces the final checks to SMT formulas.

The GPU model is SIMT: threads execute one kernel with distinct tid values, communicate through shared arrays, and use barriers; writes become visible after a barrier (Section 2.1, p. 405). A race is two different threads accessing the same array index with at least one write (Section 3, bottom of Figure 2 and text, pp. 410–411). The paper says: “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.” (Section 4.2, p. 414).

technique 1: access memory protocols and exact DRF semantics

What it is. A protocol records reads and writes to one shared location. Unsynchronized fragments u prohibit barriers; synchronized fragments p must include barriers. Evaluating an unsynchronized fragment yields a phase, a set of accesses. Evaluating a synchronized fragment yields a history, a list of phases; a barrier creates empty phases before and after synchronization, while sequencing merges adjacent phases that can execute concurrently (Section 3, pp. 409–411).

When to use it. Use this abstraction when the property concerns concurrent access conflicts and exact data values are irrelevant. It exposes which thread/index pairs may overlap and makes barrier causality explicit. It is unsuitable when correctness depends on the value read or written, because the protocol intentionally forgets values.

How to apply it.

  1. Slice the kernel to accesses to one shared array (Section 5, p. 415) and represent each read/write as rd[index] or wr[index] (Sections 2.2–3, pp. 406–410).
  2. Instantiate tid with each thread identifier in the thread set T (rule U-par, |T| >= 2) and evaluate loops over their integer ranges, lower bound included and upper bound excluded (Section 3, Figure 2, pp. 409–410).
  3. Form phases for unsynchronized code and histories for synchronized code, merging accesses that can occur in the same phase (Section 3, pp. 409–411).
  4. Mark a phase safe when no pair of its accesses is racy (two different threads, same index, at least one write); mark a history safe when every phase is safe (Section 3, p. 411 and Figure 2, p. 410).
  5. Declare the protocol DRF exactly when p ↓ H and safe(H) (Section 3, p. 411). The definition does not distinguish harmful from benign races.

The paper’s representative unsynchronized formula quantifies loop indices and distinct threads: ∀j1, i1, j2, i2 ... ==> ... DRF with? ...; it rejects the protocol when rd[t1+j1] can overlap wr[t2] (Section 2.2, p. 407). Its synchronized example similarly finds a race between iterations r=1, t1=0, t2=1, j1=1, with N>1 and M>1 (Section 2.2, pp. 407–409).

Verus form. Inference: define an enum for rd/wr, a ghost access record (thread,index,mode), and spec fn safe_phase that forbids conflicting pairs. Use requires/ensures on proof functions for each protocol evaluator and while invariants for loop bounds. Inference: this protocol layer can be verified in Verus, but it cannot prove value-dependent functional properties that the abstraction erases.

Evidence and limits. The paper says its “theory and results on access memory protocols are fully mechanized in Coq” (Introduction, p. 404) and that the artifact has Coq proof scripts for each theorem (p. 405). Well-formedness requires structural conditions, free variables only {tid}, and synchronized loops that execute at least once (Definition 1, p. 411). Inference: these assumptions must be checked or enforced by the implementation; Section 5 (pp. 415–416) describes how Faial does so.

technique 2: barrier aligning for synchronized loops

What it is. Synchronized loops can race across iterations because an access in iteration r may overlap one in r+1. The syntax-directed align : W -> A × U transformation normalizes a well-formed protocol into an aligned synchronized part plus a trailing unsynchronized part (Section 4.1, pp. 411–412). In the paper’s matrix example, code before the first barrier remains outside the aligned loop, code after the barrier moves to the beginning of the aligned loop, and the final iteration’s trailing code becomes an unsynchronized suffix (Listing 2.3 and its aligned form, p. 408).

When to use it. Inference: apply aligning before compositional analysis whenever a protocol contains synchronized loops whose barriers do not occur exactly before the loop and at the end of its body. It prevents accesses from leaking between iterations while preserving race behavior.

How to apply it.

  1. Classify every loop as synchronized or unsynchronized according to whether its body contains sync, and reject malformed combinations such as a synchronized loop whose range depends on tid (Sections 3 and 5, pp. 410–411, 415–416).
  2. Recursively apply align to sequences. For a synchronized loop u1; forS x in n..m {p;u2}, emit the fragment before the loop together with the synchronized part of the first iteration, an aligned loop from n+1 to m, and the unsynchronized part of the last iteration (u[x := m-1]) (Figure 3 and text, p. 412). Unrolling the first iteration is valid because only non-empty synchronized loops are analyzed.
  3. Use the sequencing operator to append unsynchronized fragments to the outermost position of the following aligned protocol (Figure 3, p. 412).
  4. Analyze the resulting q;u protocol. Theorem 1 states: “If p ∈ W and align(p) = (q, u), then p is DRF if and only if q; u is DRF.” (Section 4.1, p. 412).

Verus form. Inference: represent protocol syntax as a ghost AST and implement align as a spec fn returning an aligned/suffix pair. Prove semantic preservation with a lemma whose ensures equates the original and transformed safety predicates. Inference: the loop-unrolling argument relies on the paper’s non-empty synchronized-loop precondition; a Verus proof must preserve that precondition in the loop invariant.

technique 3: split aligned protocols into symbolic traces

What it is. After aligning, split : A -> [L] creates symbolic traces for fragments between barriers. A trace has accesses, sequencing, and integer-range binders. trace extracts one-thread behavior from unsynchronized code; split introduces two fresh symbolic thread variables for each unsynchronized fragment and reinterprets synchronized loops as binders (Section 4.2, pp. 413–414).

How to apply it.

  1. For each aligned fragment u; sync, create fresh distinct thread variables t1,t2, bind their ranges, and concatenate trace(u)[tid:=t1] and trace(u)[tid:=t2] (Figure 4, p. 413).
  2. For an aligned synchronized loop, bind the loop variable over its range and recursively split the body (Figure 4, p. 413).
  3. Evaluate each trace to a history by taking the product of histories for sequencing and enumerating binder assignments (Section 4.2, pp. 413–414).
  4. Check each resulting history for safe phases with the race predicate. Theorem 3 states that the original aligned history is safe iff the histories generated by split are safe (Section 4.2, p. 414).

The method is compositional because each trace can be checked independently. The paper states: “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.” (Section 4.2, p. 414). In Claim 2 Faial times out above 17 nested synchronized loops (p. 419).

Verus form. Inference: encode traces as ghost sequences and use quantified proof functions to show that every pair of distinct thread bindings has distinct indices whenever a write is present. Use forall-style quantified assertions supported by the Verus specification subset, with arithmetic lemmas for bounds. Inference: if quantifier instantiation becomes difficult, preserve the paper’s trace decomposition but discharge each trace using a solver-backed lemma rather than runtime code.

technique 4: infer protocols, enforce well-formedness, and quantify to SMT

Implementation pipeline. Faial parses CUDA with libclang, converts code to SSA, and slices away code unrelated to shared-array accesses (Section 5, p. 415). It normalizes non-unit loops by changing the stride to one and guarding the body with a divisibility test; power-of-n loops use a powerof guard. It inlines annotated shared-memory helper calls and discards calls that do not access shared memory. Recursive functions are unsupported (Section 5, p. 415).

Faial tags loops and conditionals as synchronized or unsynchronized, groups sequencing around barriers, rejects synchronized loops that manipulate thread-local tid, and inserts assertions that synchronized-loop ranges are non-empty. It duplicates synchronized conditionals with global assertions for each branch; synchronized conditionals inside synchronized loops are unsupported (Section 5, pp. 415–416).

Quantification translates each symbolic trace into QF_LIA SMT constraints. The generated formula requires the indices of two distinct threads to differ whenever one access is a write; multidimensional arrays generate one index pair per dimension and require at least one pair to differ (Section 5, p. 416). The implementation uses SMT-LIB QF_LIA even though multiplication can make the logic undecidable (Section 5, p. 416).

Verus form. Inference: a Verus front end could produce the same ghost protocol AST from Rust array accesses, with proof functions checking well-formedness and assert statements exposing the final arithmetic obligations. Verus’s requires can encode non-empty loop ranges and synchronization preconditions; ensures can state that each generated access pair satisfies safe_phase. Inference: the paper’s use of an external SMT solver and its QF_LIA status are trust-boundary choices; a Verus deployment must document whether solver results are checked by Verus and which arithmetic axioms are trusted.

evidence from experiments

Claim 1 used five tests, each with one racy and one DRF variation, on an Intel i5-6500 with 7.7 GB RAM and a 90-second timeout (Section 6, Table 1, pp. 416–418). Faial passed 4 of 5 tests; GPUVerify passed 1/5; PUG, GKLEE, and SESA passed 0/5. Faial’s only failure was Test 5, where protocol abstraction caused one spurious race (0/1 actual races), because the protocol omits array-element data (Section 6, pp. 417–418). These are counts over five tests, not percentages of all kernels.

Claim 2 generated five categories of DRF synthetic kernels, repeating each pattern from size 1 to 50 and averaging five runs; each run had a 90-second timeout, and timed-out or false-alarm runs were excluded (Section 6, pp. 418–419). The paper says Faial “has the slowest growth” in 4 of 5 categories and “verifies all tests within 0.46 s” (the paper also says Faial is fastest at the largest sizes in 3 categories, 2nd for barriers, and 3rd for synchronized loops). Faial was the only tool with near-constant time/memory through 50 unsynchronized loops. Faial timed out only for more than 17 nested synchronized loops; real-world kernels in Claim 3 had at most three such levels (Section 6, p. 419). The paper reports growth curves rather than a single aggregate percentage.

Claim 3 used 227 real-world DRF CUDA kernels: 8 from NVIDIA SDK 2.0, 166 from NVIDIA SDK 5.0, 20 Microsoft C++ AMP samples, and 33 gpgpu-sim benchmarks (Section 6, pp. 419–421; timeout 60 s, values averaged over five runs, p. 421). On this denominator, Faial was correct on 218/227 (96.0%), false-alarm on 9/227 (4.0%), unsupported on 0/227, and timed out on 0/227. GPUVerify was correct on 153/227 (67.4%), false-alarm on 47/227 (20.7%), unsupported on 1/227 (0.4%), and timed out on 26/227 (11.5%). PUG was correct on 79/227 (34.8%), false-alarm on 6/227 (2.6%), unsupported on 142/227 (62.6%), and timed out on 0/227. The percentages match the displayed counts after rounding. The kernels were pre-processed by the authors of Bardsley et al. [2] and annotated with minimal preconditions; the present authors removed GPUVerify-specific annotations (preconditions and loop invariants), converted nested array lookups to temporary variables, inlined array-operating function calls in 22 kernels, and simplified control flow in another 8 (Section 6, pp. 419–421). Inconsistency in the paper: the Introduction gives 227 real-world and 250 synthetic kernels, while the Conclusion says 229 real-world and 258 synthetic (pp. 404, 423).

techniques for the catalog

  • access memory protocols: model each shared location’s thread-indexed reads and writes as synchronized or unsynchronized behavioral types
  • barrier aligning: normalize synchronized loops so barriers delimit iterations, preserving and reflecting DRF
  • symbolic trace splitting: split aligned barrier intervals into independently checkable traces with quantified thread and loop variables
  • SMT DRF reduction: translate traces to quantified index/mode constraints and require distinct indices whenever a write is present
  • front-end well-formedness: infer protocols from SSA-sliced CUDA, normalize loops, and reject unsupported synchronization forms

Last edited: