SentryWard: Formal Verification of Warp-Specialized GPU Kernels

For most of CUDA’s history, a kernel was a data-parallel program. Every thread ran the same code on its own slice of the data, and block-wide barriers kept the threads in step: load a tile, wait, multiply, wait, load the next.

Hopper and Blackwell broke this rhythm. Their tensor cores are so fast that a kernel keeps them busy only if it loads the next tile while multiplying the current one. So the fastest kernels split each thread block into roles that run at the same time, one loading, one multiplying, one writing results. The roles hand off work through asynchronous copies and barriers that count bytes.

Such a kernel is a concurrent program, and it fails like one. A missing wait does not crash anything. In some schedules, it lets threads read the result of a multiplication before the tensor core has written it, and the output is silently wrong; in others, the same kernel computes the right result. The computation itself can also go wrong, for example through an off-by-one index or a tile read in the wrong layout.

SentryWard is a verifier for these kernels. Given a kernel’s PTX, a launch configuration, and a PyTorch reference, it proves that the kernel’s barriers behave the same way in every schedule, that no schedule has a data race, and that the kernel computes the same function as the reference. The same analysis also rules out deadlocks and uses of freed resources. SentryWard found issues in popular kernel libraries; we describe three of them below. Removing synchronization that it shows to be redundant cuts kernel time by a median of 7.5% at our example inputs and 3.0% at larger ones. In this post, we look at how warp-specialized kernels synchronize, what goes wrong, and how SentryWard checks them.

Inside a warp-specialized kernel

Kernels whose warps take different roles are called warp-specialized. Much of their work is asynchronous: an instruction only starts a copy or a multiplication, and a dedicated unit, the Tensor Memory Accelerator (TMA) or the tensor core, completes it later. A block-wide barrier such as __syncthreads() cannot coordinate such a kernel: it would force the roles back into lockstep, and it does not wait for asynchronous operations. Instead, the roles signal each other through mbarriers, barrier objects in shared memory that count the arrivals and bytes they still expect. When both counts reach zero, the barrier’s current phase completes, and the threads waiting for it proceed.

Our running example is a small warp-specialized kernel on a Blackwell GPU. It computes one \(128 \times N\) tile of \(C = AB\) from a \(128 \times K\) tile of \(A\) and a \(K \times N\) tile of \(B\). In practice, \(K\) is large, and the kernel loops over blocks of \(K\), reusing its shared-memory buffers; for simplicity, we show a single iteration. The kernel has 128 threads in three roles: thread 0 is the producer, thread 32 the MMA issuer, and all 128 threads form the epilogue. Two mbarriers coordinate them: full signals that both input tiles are in shared memory, and mma_done that the product is in tensor memory. Each of the two input tiles is 16 KB.

// 128 threads (4 warps), thread index t.
if t == 0:
    init(full, 1)
    init(mma_done, 1)
syncthreads()

if t == 0:                           // producer
    arrive.expect_tx(full, 32 KB)        1
    tma_load(sA ← A, full)               2 3
    tma_load(sB ← B, full)               2 3

if t == 32:                          // MMA issuer
    wait(full, 0)                        4
    tcgen05.mma(acc ← sA * sB)           5
    tcgen05.commit(mma_done)             6

wait(mma_done, 0)                    // epilogue 7
r = tcgen05.ld(acc[t, :])                8
tcgen05.wait::ld()
st.global(C[t, :] ← r)                   8

The kernel is correct only because of the order its barriers enforce: step 4 keeps the multiplication from reading sA and sB too early, and step 7 keeps the threads from loading the accumulator too early.

A bug that depends on the schedule

Now suppose the epilogue forgets its wait, step 7:

wait(mma_done, 0)                    // epilogue (buggy)
r = tcgen05.ld(acc[t, :])
tcgen05.wait::ld()
st.global(C[t, :] ← r)

Both barriers still count exactly as before: the copies complete phase 0 of full, and the commit’s arrival completes phase 0 of mma_done. But nothing orders the epilogue’s loads after the multiplication any more. Whether the epilogue reads acc before or after the tensor core writes it depends on the schedule:

In this small kernel, the missing wait is easy to spot. In real kernels, with many more roles, pipeline stages, and asynchronous operations, it is not. The results below include a closely related missing wait in CUTLASS.

A test observes only the schedules that happen to occur, and so does a dynamic race detector such as Compute Sanitizer. Enumerating schedules is infeasible, even for this kernel with 128 threads and several asynchronous operations. We need an argument that covers every schedule without enumerating them.

SentryWard

SentryWard checks these three properties in turn: that the barriers behave the same way in every schedule, that no schedule has a data race, and that the kernel computes the same function as the reference. The first property is well-synchronization, which WEFT introduced for named barriers and SentryWard extends to mbarriers. Each check relies on the guarantee of the one before it, and every guarantee covers all schedules of the launch. When a check fails, SentryWard reports a witness, such as the two unordered accesses of a race.

Program representation

SentryWard analyzes kernels with static control flow: their branches and loop bounds may depend on the launch configuration, but not on the data. It first specializes the kernel for the launch configuration: it resolves branches and unrolls loops, so that each thread executes a finite sequence of instructions. It then records the program in two views: the event view, a graph of events, and the value view, which records what each thread loads, stores, and computes. An instruction that takes effect at once, such as a store or a barrier update, is a single event. An asynchronous instruction starts with an issue event, after which the hardware performs the rest. Program-order edges record the order that each thread’s code imposes.

Synchronization analysis

Program order covers each thread on its own; across threads, the order comes from barriers. An mbarrier goes through a sequence of phases. During each phase, it counts pending arrivals and pending bytes: arrive removes an arrival, expect_tx announces bytes, and a TMA copy subtracts its bytes when its data lands. When both counters reach zero, the phase completes, and the next phase starts with the counters reset. A thread waits for a phase with wait(bar, parity), which names the phase by its parity.

Which updates does a wait observe? Those of the phase it waits for. But the schedule can change which phase an update joins. In one schedule, an update happens before phase 0 completes, so it joins phase 0. In another schedule, phase 0 completes first, so the same update joins phase 1. SentryWard focuses on kernels in which the schedule never changes what a wait observes. Formally, it requires the kernel to be well-synchronized: every barrier update and every wait belongs to the same phase in every execution. This restriction is reasonable because programmers already intend a fixed phase for every update and every wait. Pipelined kernels, for instance, compute the parity of each wait from the loop counter.

Following WEFT, SentryWard first simulates one trace of the kernel, along any schedule that completes, and records the phase of every barrier update and every wait. From this trace it builds a candidate graph with a completion vertex for each phase. It then certifies that every schedule agrees with the trace. WEFT does this by checking that every update comes after the previous phase of its barrier completes. If certification succeeds, the candidate graph is the kernel’s happens-before graph: its orderings hold in every execution, and no execution deadlocks.

The hard part is the byte counter, for which WEFT’s check is not enough. A named barrier counts only arrivals, so a phase cannot complete before its last arrival. Pending bytes, however, go up as well as down, so a phase can reach (0, 0) before all of its updates have happened. It then completes early: the threads waiting for it proceed without the remaining updates, which join the next phase instead. To see this, consider a different mistake from the one above: the producer announces each tile’s 16 KB separately, just before starting its copy.

if t == 0:                           // producer (another bug)
    arrive.expect_tx(full, 16 KB)
    tma_load(sA ← A, full)
    expect_tx(full, 16 KB)
    tma_load(sB ← B, full)

If copy A lands before the second announcement, phase 0 completes early, and the second announcement joins phase 1. Unlike the missing wait, this kernel is not well-synchronized: the phase that the second announcement joins depends on the schedule. To catch such kernels, SentryWard checks that no phase can complete early. It looks for updates that can happen before the rest of their phase and already bring both counters to zero, like the first announcement and copy A here.

SentryWard considers only well-synchronized kernels, although a correct kernel need not be well-synchronized. The kernel with separate announcements happens to be incorrect: when copy A lands first, the MMA may read sB before the second copy writes it. In our benchmark, only one kernel is not well-synchronized, and it is a bug as well.

The kernel with the missing wait, in contrast, passes the well-synchronization check, since its barriers count exactly as in the correct kernel. But without the epilogue’s wait, its happens-before graph has no path from the MMA’s execution to the epilogue’s loads (see the “Buggy kernel” tab in Figure 5).

Race freedom and serialization

With the happens-before graph, checking races becomes a question about paths. Two accesses conflict if their footprints may overlap and at least one of them writes, and SentryWard requires every conflicting pair to be ordered. Footprints follow exact layouts, including swizzled shared-memory tiles, and an SMT solver decides overlap when addresses are symbolic.

In the buggy kernel, nothing orders the MMA’s store to acc before the epilogue’s loads, so SentryWard reports a race, with the two accesses as its witness. Uses after free are checked the same way: every use of a resource, such as tensor memory, must be ordered before the resource is freed.

A kernel that passes these checks behaves like a sequential program. On a given input, every execution has the same effect as running its events one at a time, in any order that the happens-before graph allows: every read and every write accesses the same addresses with the same values, and the final memory is the same.

Compact representation

An explicit per-thread, per-scalar representation does not scale: a block has hundreds of threads, and a single \(128 \times 256\) output tile with \(K = 4096\) involves about \(1.3 \times 10^8\) multiply-accumulates. Most of this size comes from repetition. SentryWard therefore represents each family of repeated threads, data elements, or reduction steps by a single indexed template, and analyzes the templates directly. A thread template covers a group of threads that have taken the same branches.

Reductions are represented in the same way. Instead of a chain of operations, a Fold stores a reduction by its operator \(\oplus\), its index range, its initial value \(z\), and the term \(e(k)\) at each index:

Its size does not depend on the length of the range. In the running example, the MMA computes each element of its accumulator as

SentryWard builds Folds from MMA instructions and from repeated updates in the code; memory elimination and the expression check then work on them directly, without unrolling them.

Equivalence checking

A kernel can be well-synchronized and race-free and still compute the wrong thing: an off-by-one index, a tile read in the wrong layout, a missing scale factor. Since a race-free kernel behaves like a sequential program, SentryWard analyzes its computation on a single serialization. First, memory elimination turns the serialized program into pure expressions over the inputs; then, an expression check proves that these expressions equal the reference’s.

Memory elimination

Memory elimination follows the serialization and keeps a memory state: the expression last stored at each address. Each store updates the state at its address, and each load is replaced by the expression that the state holds at its address, or by an input if nothing was stored there. The buffers in between, here sA, sB, and acc, drop out, and each output element becomes an expression built only from the inputs.

Expression checking

The expression check takes two pure expressions over the same inputs: the kernel’s, from memory elimination, and the reference’s. They are rarely identical, because an optimized kernel computes its reductions differently from the reference: it may split a reduction into parts, combine the parts in a different order, or rescale them. To prove the two expressions equal, SentryWard uses the reference as a guide: it relates the kernel’s expression, part by part, to the reference’s intermediate results.

Figure 10 shows an example: attention for one query \(q\) and four keys of dimension four, with a scalar value \(v_j\) for each key \(j\). The reference computes the scores \(s_j\), the sum \(Z\) of their exponentials, and the weighted sum \(U\) (a sum is a Fold with \(\oplus = +\) and \(z = 0\)). The optimized kernel splits each score between two threads, one for the even \(k\) and one for the odd \(k\). It processes the keys in two blocks with online softmax: within a block, it subtracts the block’s largest score before taking exponentials, and the merge rescales both blocks to the overall largest score \(m\). To show that the kernel’s output \(p / \ell\) equals \(U / Z\), SentryWard proves five equalities, in order.

In each step, SentryWard writes a part of the kernel’s expression as \(c \cdot \sum_{k \in S} t(k) + r\): a common factor \(c\) times terms \(t(k)\) of a reference sum, plus a rest \(r\). If \(S\) covers every index exactly once, the part equals \(c\) times the reference sum, and later steps use it as a known value. If the merge forgot to rescale one block, the two blocks would have different factors, and no proof would be found. SentryWard checks coverage on a compact representation of index sets (their generating functions), without listing the indices, so it also handles large and strided index ranges. SentryWard compares parts without reductions by canonicalizing both sides into exponential polynomials, and handles operations such as square roots separately.

Figure 10 is simplified: it merges just two blocks, while real kernels merge many blocks in a loop. SentryWard proves such loops correct by induction, with an invariant that relates the loop’s state to the reference. Its support for induction is limited: it relies on predefined invariants for a few patterns, such as online softmax and Welford statistics, and does not synthesize invariants in general.

The check treats floating-point values as real numbers, so equivalence holds in real arithmetic. It is also incomplete: finding no proof does not mean the kernel is wrong.

Results

Issues found in popular kernel libraries

Real kernels go wrong in the same ways as our small example, but with more threads, stages, and barriers to hide the mistake. We describe three issues that we encountered while verifying kernels with SentryWard. The first turned out to be fixed upstream already; we reported the other two, and they are still waiting for a response.

Caveat. SentryWard’s model of the hardware follows our reading of the PTX documentation. The model lives mostly in how SentryWard builds the event graph; the algorithms that follow do not depend on it and would work with a different model. The PTX documentation does not specify every detail, though, so our model may differ from how the hardware actually behaves. We welcome feedback and will refine the model as we learn more.

PyTorch: a bug that was already fixed. We happened to verify an older release, PyTorch 2.8.0, and SentryWard flagged a race in its MultiMarginLoss backward kernel. The kernel splits a row of gradients among the threads of a block: thread 0 writes the gradient of the target class, and then every thread scales its part of the row. With no barrier in between, the thread that owns the target class may scale a stale value. The bug had already been reported and fixed upstream, independently of us, in PyTorch 2.9.0. It makes a useful sanity check: a real bug, confirmed by the PyTorch developers, that SentryWard finds on its own.

// one block per row; thread t owns columns t, t + blockDim, ...
for each of my columns i ≠ target:
    gradInput[i] = h(i)                   // 0 if the margin holds
    buffer[t] -= h(i)
__syncthreads()
if t == 0:
    gradInput[target] = sum(buffer)       // thread 0 writes the target entry
__syncthreads()                           // missing; PyTorch 2.9.0 adds it
for each of my columns i:
    gradInput[i] *= gradOutput            // the owner of target scales it

TileLang: a buffer reused too early. Our second example comes from a compiler. TileLang turns tile-level Python into GPU kernels and pipelines the loads automatically. With two pipeline stages, tiles \(k\) and \(k + 2\) share a buffer, so the copy of tile \(k + 2\) must wait until the multiplication of tile \(k\) has finished reading. The planner orders the copy after the MMA instruction, but the tensor core executes that instruction asynchronously and keeps reading the buffer until a later wait. The copy can therefore overwrite operands in the middle of a multiplication, and SentryWard points to exactly that write and that read.

# TileLang program
for k in T.Pipelined(num_tiles, num_stages=2):
    T.copy(A[k], A_shared)
    T.copy(B[k], B_shared)
    T.tcgen05_gemm(A_shared, B_shared, C_tmem, mbar=mbar)
    T.mbarrier_wait_parity(mbar, k % 2)

// generated loop body, iteration k, stage s = k % 2
tcgen05.mma(acc += sA[s] * sB[s])         // the tensor core reads stage s
tcgen05.commit(mbar)
__syncthreads()                           // does not wait for the tensor core
// the copies of tile k + 2 overwrite stage s
cp.async(sA[s] ← A[k + 2])
cp.async(sB[s] ← B[k + 2])
wait(mbar, k % 2)                         // MMA k is known to be done only here

CUTLASS: a signal sent too early. Our third example is a close relative of the running example. In CUTLASS’s Blackwell attention kernel, the softmax warpgroup writes row statistics to tensor memory and then tells the correction warpgroup that they are ready. But the write is asynchronous, and the signal goes out without waiting for it with tcgen05.wait::st. The correction warpgroup may then read the statistics before they land.

// softmax warpgroup, once per tile of keys
tcgen05.st(stats ← old_max, new_max)
tcgen05.wait::st()                        // missing
arrive(stats_ready)                       // tells the correction warpgroup
...
tcgen05.st(P ← probabilities)
tcgen05.wait::st()                        // here the kernel does wait
arrive(p_ready)                           // tells the MMA warp

// correction warpgroup
wait(stats_ready, phase)
r = tcgen05.ld(stats)                     // may read stale statistics
scale = exp(r.old_max - r.new_max)

Removing redundant synchronization

Because SentryWard checks every schedule, it can also identify synchronization that is unnecessary: if a kernel still verifies after we remove a synchronization operation, that operation is redundant. We apply this test greedily to each verified kernel, one operation at a time, and keep each removal that passes it.

We tried this on 44 kernels from our benchmark, each at two input sizes: the inputs of our examples, and larger inputs at which every pipeline buffer is reused (Figure 14). At the example inputs, 48.6% of the synchronization operations we tried turned out to be unnecessary, and removing them made 35 of the kernels faster on a B200, with a median reduction in kernel time of 7.5%. At the larger inputs, 42.4% were unnecessary, 37 kernels got faster, and the median reduction was 3.0%. Larger inputs thus leave less to remove, and a reduction found at one input may be wrong at another: at the larger inputs, SentryWard rejects 35 of the 44 reductions found at the example inputs, and 34 of those hang or fault on a B200. To double check, we also ran random tests: every reduced kernel produced exactly the same output as the original, over 500,000 launches at the example inputs and 20,000 at the larger ones.

Future directions

• Symbolic input shapes. SentryWard currently fixes the problem sizes and the launch configuration. With symbolic shapes, one proof would cover all sizes.
• Data-dependent control flow. Branches and loop bounds may currently depend only on the launch configuration. Supporting branches on tensor data would cover many more kernels.
• Weak memory model. SentryWard currently assumes that a write is visible to all threads once it happens: it models the ordering that barriers and asynchronous completion provide, but not fences. Supporting the full PTX memory model would cover kernels that synchronize with fences.
• Floating-point semantics. Numerics matter in LLM training and inference. Low precision loses accuracy, large values overflow, and different summation orders give different results, for example across batch sizes or between training and inference. Extending SentryWard from real arithmetic to floating-point semantics would help reason about these issues.

← Back to the project overview