PaperlayerView exact revision on arXiv

Source-linked AI summary

WarpDRF: Data-Race Freedom for Warp-Level Programming

Zheyuan Chen, Simon Kagle, Tiago Cogumbreiro, Tyler Sorensen

arXiv:2610.07541v1cs.PL

TL;DR

GPU warp primitives synchronize execution-determined thread subsets, but the data-race-freedom contract relied on by kernels has not been stated precisely or empirically tested. WarpDRF formalizes and tests that contract, then applies a warp-aware checker to llama.cpp; it guarantees reference-equivalent behavior for satisfying kernels and finds that 77 of 95 analyzed kernels satisfy its conditions.

  • Problem

    Warp-primitive participation and synchronization have lacked a precise data-race-freedom contract, despite differing reconvergence guarantees and scheduling behavior across GPU languages.

    Source: §1 · p. 2

  • Method

    WarpDRF specifies memory-ordering and participant-set conditions by configuration, proves a reference-semantics guarantee, and is implemented in an MLIR interpreter and a Faial-based checker.

    Source: §1.1 · p. 2, §3.3 · p. 7

  • Results

    77 of 95 llama.cpp kernels (81.1%) satisfied both WarpDRF conditions, while 18 were buggy; satisfying kernels match the reference participants, reads, and final memory.

    Source: §3.3 · p. 7, §5.2 · p. 12

  • Takeaways & Limitations

    Across tested systems, full-warp programs behaved consistently, whereas partial participation varied across languages, compilers, and targets.

    Source: §7 · p. 13

    The weakest WarpDRF configuration remains empirically tested; the authors cannot claim it is vendor-supported, even through informal prose.

    Source: §4.3 · p. 10

Abstract

from arXiv · show

Warp primitives such as tensor core operations, shuffles, reductions, and barriers are critical to high-performance GPU kernels, and every major GPU language supports some set of them. The threads that participate in a primitive, and therefore synchronize, are determined dynamically by how threads diverge and reconverge, and by intra-warp scheduling such as independent thread scheduling. In practice, many high-performance kernels use these primitives and behave as expected, following an intuitive but unwritten data-race-freedom contract that has never been stated precisely or empirically tested. We present WarpDRF, the first abstract warp programming model to make this contract precise, with participation rules parameterized by reconvergence guarantees and per-primitive requirements so that instantiations match different GPU languages. We prove (formalized in Rocq) that a kernel satisfying WarpDRF executes every warp primitive with the participants the reference semantics assigns and produces the same results, so a programmer can reason in the reference semantics alone. We implement the model in MLIR with a reference interpreter and fuzz 10K conformance tests for each of three configurations across CUDA, HIP, HLSL, Metal, and SPIR-V on 16 device and backend pairs; at least one WarpDRF configuration describes each, with CUDA honoring the strictly weakest configuration. Finally, we extend Faial, a static data-race analyzer for CUDA, into the first DRF checker for an empirically validated warp model, and apply it to llama.cpp, where most kernels that use warp primitives already satisfy the contract, but three contain previously unknown data races, showing the need for tools that check it.

1 Introduction

Warp primitives enable high-performance GPU kernels, but their dynamically determined participants and synchronization behavior have lacked a precise data-race-freedom contract. WarpDRF defines such a contract, tests GPU implementations against it, and applies a warp-aware checker to llama.cpp kernels.

1 Introduction

  • Warp primitives are collective operations whose participants depend on control flow, affecting both returned values and which threads are ordered.Independent thread scheduling and differing reconvergence guarantees make participant assumptions language-dependent.Source: §1 · p. 1
  • A data-race-freedom contract for warp primitives was previously unstated, and the code relying on it had not been checked against one.GPU memory models and analyzers treat synchronization as occurring among fixed groups of threads, not execution-determined warp subsets.Source: §1 · p. 2

1.1 WarpDRF: Contract, Conformance, Code

  • WarpDRF requires conflicting memory accesses to be ordered and each primitive instance to have an unambiguous participant set.The conditions depend on each other because a primitive orders memory only for its participants.Source: §1.1 · p. 2
  • WarpDRF configurations specify reconvergence and per-primitive participant requirements, and satisfying kernels match the reference semantics on conforming systems.The guarantee covers participant sets, reads, and final memory; the proof is formalized in Rocq.Source: §1.1 · p. 2
  • Across 10K tests per configuration on 16 device and backend pairs, each language conformed to at least one configuration, while CUDA honored the weakest.The weakest configuration permits primitives only when every warp thread executes them.Source: §1.1 · p. 2
  • 77 of 95 llama.cpp kernels (81.1%) satisfied both conditions; the other 18 mapped to four source patterns with confirmed or input-conditional alarms.The checker extends Faial to support warp primitives and checked the kernels using them.Source: §1.1 · pp. 2–3

2 Background

Warp primitives provide communication and synchronization within execution groups, but divergence makes their participants depend on control flow and language guarantees. Because only participating threads receive a primitive’s ordering, memory-race freedom alone does not ensure correct participation or collective results.

2.1 Execution Hierarchy and Synchronization Scopes

  • Warp-scoped collectives exchange or combine register values, while only barriers with documented memory semantics order accesses, and only within their scope.A warp barrier cannot order accesses between different warps, even in the same block.Source: §2.1 · p. 3

2.2 Divergence and Collective Participation

  • Divergence and reconvergence shape primitive participants; separate executions of a source-level primitive, including loop iterations, have distinct participant sets.Cooperative matrix operations require full-group participation, and an explicit mask selects one primitive’s participants without guaranteeing general reconvergence.Source: §2.2 · p. 3, Table 1 · p. 4

2.3 Why Memory DRF Is Insufficient

  • A barrier after the conditional cannot order thread 1’s write before thread 0’s branch read when thread 1 did not join the earlier barrier.Moving the barrier before the conditional orders conflicting writes before reads; reconvergence itself supplies no memory ordering.Source: §2.3 · p. 4, Figure 2 · p. 4
  • A partial-warp collective can be memory-race-free yet return a register value that depends on how threads are grouped.The participant set therefore matters even for primitives that do not order memory.Source: §2.3 · p. 4
  • WarpDRF’s portable fully convergent rule requires every executed warp primitive to include the complete warp while allowing divergent paths and distinct operands between primitives.This avoids relying on API-specific reconvergence rules; the barrier moved before the conditional follows the rule, whereas the partial-warp barrier does not.Source: §2.3 · p. 4

3 The WarpDRF Contract

WarpDRF defines a data-race-freedom contract by settling primitive participation before reasoning about memory ordering. It parameterizes the contract for language-specific guarantees and proves that satisfying kernels match the reference semantics on conforming targets.

3.1 The WarpDRF Language

  • Configurations encode warp width, each primitive’s memory-ordering and participant requirements, and participation under divergence.The language is a pragmatic subset rather than a complete formalization of any one GPU language, and does not model CUDA or HIP bitmasks.Source: §3.1 · p. 5
  • Dynamic blocks determine which threads execute a primitive instance together; separate loop iterations and repeated calls create distinct groups.The deliberately small language models memory accesses, warp primitives, and structured control flow, but excludes unstructured control flow.Source: §3.1 · pp. 5–6

3.2 The Contract

  • The contract requires ordered conflicting memory accesses and unambiguous primitive participation satisfying the configuration’s participant constraint.The conditions depend on one another because primitive ordering applies only to its participants, and changing a group can also change a primitive’s result.Source: §3.2 · p. 6

3.3 The Guarantee

  • A kernel satisfying WarpDRF executes each primitive with the reference-assigned participants and produces the same reads and final memory on a conforming target.The guarantee also covers partial groups when the configuration guarantees them and the reference semantics determines them.Source: §3.3 · pp. 6–7
  • SSO waits until every thread that may still reach a primitive has arrived or taken an excluding path, and the mechanized theorem shows it supports WarpDRF.The weaker speculative model can execute with an incomplete group and permit a racing execution even for a kernel satisfying WarpDRF; the theorem is formalized in Rocq.Source: §3.3 · p. 7

3.4 Instantiating Configurations

  • The portable complete-warp configuration relies on an empirically observed CUDA join-point rule, while partial-warp __activemask() grouping lacks an observed stable reconvergence rule.SPIR-V’s optional maximal-reconvergence mode supplies a different, structured reconvergence guarantee.Source: §3.4 · p. 8

4 Testing Implementations

The study tests WarpDRF configurations against GPU implementations using an MLIR reference interpreter and fuzzed kernels. Across 16 device/backend pairs, every system conforms to at least one configuration, while CUDA conforms only to the weakest.

4.1 Conformance Tests and Oracle

  • The interpreter supplies one expected result per test, and each test observes participation by having every thread record the count returned by wave_count_bits.Tests launch exactly one complete warp using the target's warp width, and each thread writes to a distinct array location.Source: §4.1 · p. 9

4.2 Configurations and Test Generation

  • The generator fuzzes control flow and places primitives only where each configuration guarantees participant sets; FMR, SMR, and CUDA form a strict strength ordering.FMR permits primitives anywhere, SMR excludes switch join nodes, and CUDA permits them only with full-warp participation.Source: §4.2 · p. 9

4.3 Conformance Across 16 Systems

  • All tested GPU stacks honor the CUDA configuration, the weakest WarpDRF instantiation, but it permits primitives only when the full warp participates.This provides a portable interface across the tested systems, at the cost of ruling out non-uniform warp primitives.Source: §4.3 · pp. 9–10
  • CUDA conformance implies that warps begin converged, avoid spurious divergence, and fully reconverge at joins, though these guarantees remain empirically tested.The paper says these weak conditions are not stated in CUDA documentation and lack even informal vendor support.Source: §4.3 · p. 10
  • The two NVIDIA CUDA pairs fail SMR, and tested CUDA devices show no reliable supported model between CUDA and SMR.Consequently, __activemask() cannot be relied on to provide deterministic participants in divergent code; Metal and HLSL agreement with SMR is empirical because neither specifies a general reconvergence rule.Source: §4.3 · p. 10
  • Ten of 16 systems provide FMR; failures include every NVIDIA pair, PowerVR, and Adreno under GLSL, with four failures limited to switch statements.At a shared switch case reached by fallthrough, the reference groups threads with different selectors, while the RTX 4070 GLSL path keeps them separate.Source: §4.3 · p. 10

4.4 WarpDRF: All or Nothing

  • A non-uniform primitive can split participants at a later fully uniform primitive, with results changing across compiler configurations.On Thor, compute_75 returns 16 rather than the reference's 32 at four shared coordinates, producing 128 mismatches among 320 recorded counts; compute_110 returns 32 throughout.Source: §4.4 · p. 10, Figure 5 · p. 10
  • The observed Thor participant grouping follows the CUDA compiler's selected PTX control flow, not the target declaration or subsequent compilation path.Across 100 repetitions, the compute_75 PTX body produces 128 mismatches and the compute_110 body produces none; the experiment does not identify a specific machine instruction as the cause.Source: §4.4 · pp. 10–11

5 Checking Kernels Against the Contract

This section extends Faial into a CUDA checker for WarpDRF’s memory-ordering and full-warp participation conditions, then checks llama.cpp’s warp-using kernels. Manual alarm validation shows most satisfy both conditions, while 18 analyzed kernels contain bugs.

5.1 WarpDRF-Faial: a WarpDRF checker for CUDA

  • WarpDRF-Faial checks memory DRF through barrier-phase tracking and checks participation through full-warp masks, warp-uniform branches, and warp-uniform loop bounds.It reports the two conditions separately and deems a kernel WarpDRF only when both succeed.Source: §5.1 · p. 11

5.2 WarpDRF-Faial on llama.cpp

  • The study analyzes the 95 of 479 llama.cpp CUDA kernels that use warp primitives, runs the checker with a 60-second timeout, and manually validates reported alarms.Validation groups alarms by source location and cause, inspects a representative specialization, and considers caller constraints that exclude a path.Source: §5.2 · pp. 11–12
  • 77 of 95 analyzed kernels (81.1%) satisfy both WarpDRF conditions; 18 are buggy, while 12 of the other 30 have false-positive or caller-discharged alarms.Table 4 organizes kernels by memory-condition rows and participation-condition columns; pass means no alarms were found.Source: §5.2 · p. 12, Table 4 · p. 12
  • False positives arise when the checker cannot prove template-dependent indices are distinct, reduction results are identical across threads, or supported bounds select complete warps.Inspection showed the reported accesses were distinct; supported template and launch configurations make the bounds warp-width multiples.Source: §5.2 · p. 12
  • Alarm review separates analysis false positives, reports discharged by current callers, and input-conditional defects such as NaN-dependent expert choices or duplicate IDs.Caller-discharged conclusions apply to current callers, not arbitrary calls satisfying only local kernel parameter types.Source: §5.2 · p. 12
  • Confirmed bugs include unordered shared-memory writes and a reduction-buffer reuse race; an ID handoff needed a warp memory barrier and was fixed upstream.A shuffle coordinates register values but does not order shared memory.Source: §5.2 · p. 12

6 Related Work

Prior work treats memory ordering and warp participation in separate lines of research. WarpDRF connects them by making execution-determined participation part of a data-race-freedom guarantee.

Scoped memory models and data-race freedom

  • Scoped memory models extend DRF reasoning to hierarchical machines, but assume synchronization participants are fixed; WarpDRF requires establishing participants before using a primitive’s ordering.Prior models attach scopes to synchronization and memory operations, with guarantees characterized for heterogeneous systems, PTX, and Vulkan.Source: §6 · pp. 12–13

GPU verification and race detection

  • Existing GPU verification and race-detection approaches do not define the participant group of an explicit warp primitive under divergent control flow.Earlier approaches cover implicit fixed-warp synchronization, atomics, dynamic race detection, or CUDA synchronization bugs.Source: §6 · p. 13

Testing implementations against specifications

  • Testing campaigns have examined memory consistency and progress against existing reference models; WarpDRF applies empirical testing to participation after supplying its contract.Related efforts include stress tests, litmus-test mutation, and broad device surveys.Source: §6 · p. 13

Warp execution and participation

  • Performance research studies warp grouping, while separate analyses specify how participants form; WarpDRF makes that participation a condition of data-race freedom.Prior participation work includes SIMT-Step, SPIR-V reconvergence, and uniformity and barrier-divergence analyses.Source: §6 · p. 13

7 Conclusion

WarpDRF combines scoped memory ordering with predictable warp-primitive participation in a portable model. Its implementations and llama.cpp analysis show consistent full-warp behavior across tested systems and expose memory and participation problems.

7 Conclusion

  • Across tested systems, full-warp programs behaved consistently, while partial participation varied across languages, compilers, and targets.The paper implements WarpDRF with an MLIR interpreter, a cross-platform conformance suite, and a warp-aware Faial extension; applying the checker to llama.cpp exposed complementary memory and participation problems.Source: §7 · p. 13
Loading 2610.07541v1…