Using SPIN model checker to statically find or prove the absence of deadlocks in CuTe DSL kernels on NVIDIA B200, and presenting a proof-of-concept github.com/cheshire/cute2promela lowering from CuTe to SPIN.
Synchronization bugs in GPU kernels are hard to debug. When a barrier deadlocks, the hardware yields no stack trace, and no error code until the benchmark times out. Hence each iteration of the debug loop starts to potentially cost tens of minutes.
As we’ve worked on FlashInfer MLSYS Challenge (our solution took 1st place in the mixture-of-experts track), we had to iterate on a persistent fused mixture-of-experts kernel for DeepSeek-V3, written in CUTLASS’s CuTe DSL for an NVIDIA B200 and stitched together from FF1, SwiGLU, and FF2 stages across clusters of CTAs. The pipeline is coordinated via mbarriers in shared memory, peer-CTA mbarriers reached via mapa
-translated DSMEM pointers, and GMEM atomic counters across clusters. A bug in any of those can potentially result in a deadlock, which is hard to debug, especially when GPUs are only available via Modal.
As my background is in formal verification, I wanted to try to instead encode the synchronization model in Promela DSL and check them with the SPIN model checker. This would not only shorten the iteration cycle, but also deterministically either demonstrate a counterexample to the desired property (e.g. a deadlock) or prove that no such interleaving exists.
Short Primer: Blackwell Synchronization Primitives #
Let’s start with an overview of Blackwell synchronization primitives we would have to model.
An mbarrier is a 64-bit hardware object that lives in shared memory. Its bits hold a current arrival count, a pre-declared expected count, and a single-bit phase. You allocate it like any SMEM variable, then have one thread initialize it with the expected count; from that point on, the hardware treats it as a small state machine with two transitions:
Arrive. Any thread can callmbarrier_arrive
on the barrier. The hardware atomically increments the arrival count. If the new count equals expected, the barriercompletes: the count resets, the phase bit flips. Otherwise the call returns and the thread continues.Wait. A thread that callsmbarrier_wait(phase=P)
stalls until the barrier’s phase differs fromP
. Since the phase only changes on completion, this means “wait until the barrier completes one more time after I last looked”.
The single-bit phase is what makes mbarriers reusable. The first time you arrive-and-wait, you wait on phase 0; after completion, the barrier is at phase 1 and ready for the next round; you wait on phase 1; and so on. A persistent kernel that does N iterations of arrive-then-wait has to flip its expected-phase tracking each iteration. Get the flipping wrong and an iteration deadlocks.
mbarrier in CuTe DSL
In CuTe DSL, every mbarrier op is one of a small handful of calls:
Initialization. Barriers are allocated in static SMEM and initialized with their expected arrival count. One elected thread per cluster does this, and a fence makes the initialization visible before anyone arrives.
Local arrive. A thread drops one count on a barrier in its own CTA’s SMEM.
TMA arrive-and-expect-tx. A variant used by TMA producers: the barrier accumulates bytes rather than arrivals, and completes when the expected byte count has landed. Typically followed by an async copy that names the barrier and a wait on the same barrier.
Phase wait. A consumer blocks until the barrier’s phase differs from the value it last saw.
Cross-CTA arrive. The B200 cluster lets two CTAs share each other’s shared memory through a DSMEM window. To arrive on a peer CTA’s mbarrier, the local SMEM pointer is translated through mapa.shared::cluster
to the peer’s view of the same allocation, and the arrive lands on that translated address.
From the peer’s perspective, that arrive lands in their count the same way a local arrive would. The hardware handles the address translation and the count update; no software protocol is involved.
Cross-cluster: GMEM atomic counter. Clusters can’t share SMEM, only GMEM. When a producer in one cluster needs to hand off to a consumer in another, the DeepGEMM idiom is an int32 GMEM counter: the producer does atomic_add(counter, 1, sem="release", scope="gpu")
when it finishes, and the consumer spins on atomic_load(counter, sem="acquire", scope="gpu")
until the count reaches expected. sem="acquire"
/"release"
is the C11 ordering pair: stores before the release are visible after the matching acquire. scope="gpu"
is the part that’s easy to get wrong — on Blackwell, ordering and scope are orthogonal, and the scope decides how far the visibility actually propagates. cta
, cluster
, gpu
, and sys
form a hierarchy; pick one too small and the consumer reads stale GMEM even though the producer’s atomic completed. Case 2 below works through the bug class this opens up.
Fences. A handful of variants order things that don’t order themselves. The one we would use is fence_view_async_shared
: it makes synchronous SMEM stores visible to subsequent async consumers (in our case, the mbarrier wait that gates a downstream SMEM read). Other call sites use fence_proxy("async.shared", space="cta")
, the inverse direction (async producers, sync consumers). Fences are cheap at runtime; forgetting them produces the same intermittently-stale reads that scope errors do, and the bug is invisible to SPIN unless the visibility constraint is encoded in the model.
A motivating kernel #
For a running example we’ll use a two-CTA Jacobi smoother on a 256-cell array of float32
. Each CTA owns 128 cells in its own SMEM and repeatedly applies the 3-point average
new[i] = (old[i-1] + old[i] + old[i+1]) / 3
across the whole array. Interior cells only touch the owning CTA’s SMEM. The cells at the boundary — cell 127 of CTA 0 and cell 0 of CTA 1 — need one value from the peer CTA, which is exchanged through cluster DSMEM once per iteration. After N rounds the array relaxes toward the linear interpolation between its two endpoints; concretely, the kernel does something visible. What we care about for the rest of the post is its synchronization skeleton, which is the same as the cross-CTA exchange in our MoE kernel.
Each iteration brings the barrier’s arrival count to 256 (every one of the 128 threads in each CTA arrives once locally and once on its peer), at which point the hardware resets the count and flips the phase bit. A thread that called mbarrier_wait
with the previous phase value unblocks, XORs its own tracked phase
for the next round, and the next wait fires when the barrier’s phase flips again. That single-bit phase, threaded through a per-thread XOR each iteration, is the only thing keeping consecutive rounds distinguishable.
Whether this is correct is not obvious from reading. The phase tracking is one register; the XOR is one line; the expected count was set once at init. If we replace the phase
argument on the mbarrier_wait
line with a literal cutlass.Int32(0)
(the bug we had in our MoE kernel!) the code would work at small iteration counts because the phase only matters from iteration 2 onward, but would deadlock in larger ones:
$ modal run repro.py --mode correct --iters 30
=== mode=correct iters=30 ===
GPU: NVIDIA B200
Launching grid=(2,) num_ctas=2 threads/CTA=128 EXPECTED=256
COMPLETED in 0.507s. done_ctr=2 (expect 2)
PASS mode=correct iters=30
ROUND-TRIP: 5.3s wall (incl. Modal launch overhead)
$ modal run repro.py --mode buggy --iters 1
=== mode=buggy iters=1 ===
COMPLETED in 0.538s. done_ctr=2 (expect 2)
PASS mode=buggy iters=1
$ modal run repro.py --mode buggy --iters 5
=== mode=buggy iters=5 ===
Launching grid=(2,) num_ctas=2 threads/CTA=128 EXPECTED=256
(GPU never returns)
...
Task's current input hit its timeout of 300s
modal.exception.FunctionTimeoutError
The model-checking side: SPIN and Promela #
SPIN is a model checker for concurrent systems, and Promela (Process Meta-Language) is the input DSL. You describe a finite set of communicating processes and the properties they should obey, and SPIN compiles a C verifier that exhaustively enumerates the reachable state space. If a property fails, it gives back a concrete interleaving as a counterexample. If the search completes, no interleaving within the model violates the property.
Processes and the init
block
A proctype
is a process template, and the run
construct spawns an instance. Everything starts from the init
block, which spawns the rest:
This launches eight Thread
processes. They share global state and interleave at the level of individual Promela statements. SPIN would explore every legal interleaving.
atomic { ... }
An atomic
block executes without interleaving. A single mbarrier arrive
is one PTX instruction, so wrapping its count/phase update in atomic
is exact:
inline
An inline
is a textual macro — like a C #define
, but multi-statement and arity-checked. We use it for primitives like do_arrive
and do_wait
so the proctype body reads like the kernel.
if
/fi
with guards
Promela’s if
is Dijkstra-style: a list of guarded statements, any one of which may fire if its guard is true. If multiple guards are open, SPIN picks any of them non-deterministically, and explores both. The :: else
branch fires only if no other guard is possible.
do
/od
Same as if
but loops, with break
to exit:
Guards as waits
Inside an atomic
, a false guard blocks the proctype until it becomes true. Promela has no separate “wait” statement; you just write the condition:
A thread that hits do_wait
sits there until mbar_phase[cta]
differs from expected_phase
. Some other thread’s arrive flips the phase, the guard opens, and the proctype proceeds.
LTL: the property language
SPIN takes safety and liveness properties as Linear Temporal Logic formulas. The LTL subset we use is:
[] P
“always P”. Safety: P holds in every reachable state. Use for invariants like “no data race”.<> P
“eventually P”. Liveness: P holds insomefuture state of every infinite execution. Use for “the protocol eventually completes”.[]<> P
“always eventually”, i.e. infinitely often. Use for fairness-style claims.<>[] P
“eventually permanently”. Use for “eventually the system stabilizes”.
Our standard deadlock-freedom claim:
Internally, SPIN compiles an LTL property into a never claim, a Büchi automaton (an automaton over infinite words, accepting by visiting an accepting state infinitely often) that accepts exactly the executions that violate the property. If SPIN finds an accepting run of the never claim, that run is the counterexample. When the violation is a safety invariant [] P
, SPIN compiles it into the never-claim !(!P)
and prints assertion violated !(!P)
on a hit. There’s no actual assert()
in the source, the doubly-negated form is the literal text of the never-claim whose witness SPIN found.
Running the verifier
The compile-and-run sequence is always three commands:
$ spin -a model.pml # generate pan.c (the C verifier)
$ cc -O2 -o pan pan.c # build it
$ ./pan -a # run; -a enables acceptance-cycle / liveness search
A handful of flags matter. -a
is what you almost always want: safety, assertions, and LTL liveness (including the acceptance cycles that show up as deadlocks). -l
checks non-progress cycles instead and needs cc -DNP
at build time.
Lowering the kernel to Promela #
Once you know what to keep and what to drop, the translation from the running example to Promela is fairly mechanical. The per-thread loop in the kernel maps directly to a proctype Thread
in Promela:
CuTe DSL kernel (per thread)
Promela proctype
The substitutions, primitive by primitive:
**Hardware mbarrier (64-bit word in SMEM packing arrival count, expected count, and phase)**→ two Promela ints,mbar_count[NCTAS]
andmbar_phase[NCTAS]
, plus a constantEXPECTED_ARRIVALS
. The hardware atomicity is preserved by wrapping every update inatomic { }
.→ thembarrier_arrive(ptr)
arrive(cta)
inline shown earlier. Increment the count atomically; if it hits expected, reset to 0 and flip phase.→mbarrier_wait(ptr, P)
atomic { mbar_phase[cta] != P -> skip; }
. A guarded atomic that blocks the proctype until the phase differs.Peer arrive via→ the samemapa_shared_cluster + mbarrier_txn(ARRIVE)
arrive
primitive, on the peer’s array slot. The model captures the protocol, not the address translation;mapa
is a deterministic function that picks which CTA’s mbarrier gets incremented, so we encode it directly asarrive(peer)
.128 threads per CTA→ 4 proctypes per CTA. For this protocol the correctness doesn’t change with width; shrinking the count keeps the state space tractable.~30 tile iterations→ITERS = 3
. Three is the smallest count that exercises phase parity (iter 0 waits on phase 0, iter 1 on phase 1, iter 2 on phase 0 again). A model with fewer iterations would pass over the phase-flip-back-to-zero bug without seeing it.Persistent loop→do :: iter < ITERS -> ...; iter++ :: else -> break od
.
Note that the modelling drops most of the code, as only synchronization primitives and calculation affecting control flow influence liveness.
$ spin -a kernel_model.pml && cc -O2 -o pan pan.c && ./pan -a
ltl all_done: <> (((iters_completed[0]==4)) && ((iters_completed[1]==4)))
State-vector 248 byte, depth reached 387, errors: 0
830628 states, stored (1.66126e+06 visited)
3735761 states, matched
5397017 transitions (= visited+matched)
pan: elapsed time 2.07 seconds
pan: rate 802539.13 states/second
What SPIN can check #
Safety: P never becomes false. Use for invariants like “no data race” or “the consumer never reads before the producer published”. SPIN proves these by depth-first search; on success the full reachable state space has been visited. On failure SPIN gives one offending state and the path to it.[] P
.Liveness: P eventually holds on every infinite execution. Use for “the protocol completes”. Failure looks different from safety: SPIN finds an<> P
.acceptance cycle, an infinite loop in the state graph that never satisfies P, which would manifest as the deadlock.Fairness: P happens infinitely often, assuming the scheduler is weakly fair to every proctype. Worth reaching for when a counterexample involves a thread that’s simply never scheduled, fairness lets you distinguish a real protocol break from one that only fails under an adversarial scheduler.[]<> P
, with-f
.
How fast does this blow up?
State-space size is exponential in the protocol dimensions you choose. We swept the correct Promela model of the running example across iteration counts (TILES_PER_CTA
, i.e. N_ITERS
) and thread counts (THREADS_PER_CTA
); the numbers below come from one laptop run, with the bottom row added from the standalone three-iteration baseline:
TILES THREADS/CTA states stored transitions wall
1 2 1,137 5,476 <0.01s
1 3 22,082 123,937 0.04s
1 4 416,831 2,564,578 0.95s
1 5 7,701,536 50,393,599 23s
2 2 4,424 21,907 0.01s
2 3 196,051 1,117,014 0.38s
2 4 9,500,414 58,705,617 26s
3 4 18,583,997 114,846,660 52s (baseline)
Adding a thread per CTA multiplies states by roughly 20×. The (3, 4) row is the full verification baseline used in the case studies and is included for context; the rows above it are a clean sweep at smaller sizes. The protocol’s shape (phase parity, count-to-expected, peer arrive via mapa) is exercised the same way at 2×4×3 as at 2×128×30 — the bug class doesn’t need 128 threads to manifest. Width-invariance holds for the phase-flip family; for racier bug classes (the no-race variant from earlier) shrinking the thread count can hide the violation. When in doubt, scale up until the verifier struggles, then back off.
Case 1: the hardcoded-phase deadlock #
In the running example, the variant we shipped first had the wait line written like this:
buggy — what we shipped
correct — what we wanted
At small iteration counts the kernel only does one round per CTA, so the phase never matters and the bug works by luck. At larger counts (roughly 30 tile iterations per cluster in production) the mbarrier’s phase has flipped twice by the second iteration, is back to 0, and the hardcoded wait(0)
blocks forever.
In the corresponding Promela models, the buggy and correct variants differ in exactly one argument: do_wait(cta, 0)
(buggy) vs do_wait(cta, my_phase)
with my_phase ^= 1
after (correct). The lowering section above shows the full proctype; what we care about here is what the verifier reports.
What SPIN says
On the buggy model:
$ spin -a mbar_protocol_bug.pml && cc -O2 -o pan pan.c && ./pan -a
ltl all_done: <> (((iters_completed[0]==4)) && ((iters_completed[1]==4)))
pan:1: acceptance cycle (at depth 305)
pan: wrote mbar_protocol_bug.pml.trail
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (all_done)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
State-vector 244 byte, depth reached 306, errors: 1
99 states, stored
99 transitions (= stored+matched)
pan: elapsed time 0 seconds
Replaying the trail with spin -t -p mbar_protocol_bug.pml
ends in the state that explains the deadlock:
$ spin -t -p mbar_protocol_bug.pml (tail)
303: proc 1 (Thread:1) line 26 [mbar_count[peer] = (mbar_count[peer]+1)]
304: proc 1 (Thread:1) line 31 [else]
305: proc 1 (Thread:1) line 31 [(1)]
<<<<<START OF CYCLE>>>>>
spin: trail ends after 307 steps
#processes: 6
mbar_count[0] = 1
mbar_count[1] = 1
mbar_phase[0] = 0
mbar_phase[1] = 0
iters_completed[0] = 0
iters_completed[1] = 3
307: proc 5 (Thread:1) line 36 (state 27) // stuck in do_wait(cta, 0)
307: proc 4 (Thread:1) line 36 (state 27)
307: proc 3 (Thread:1) line 36 (state 27)
307: proc 2 (Thread:1) line 36 (state 27)
307: proc 1 (Thread:1) line 36 (state 27)
On the fixed model:
$ spin -a mbar_protocol.pml && cc -O2 -o pan pan.c && ./pan -a
ltl all_done: <> (((iters_completed[0]==4)) && ((iters_completed[1]==4)))
Full statespace search for:
never claim + (all_done)
acceptance cycles + (fairness disabled)
State-vector 272 byte, depth reached 547, errors: 0
18583997 states, stored (3.7168e+07 visited)
77678662 states, matched
1.1484666e+08 transitions (= visited+matched)
hash conflicts: 23239621 (resolved)
Stats on memory usage (in Megabytes):
5594.538 total actual memory usage
pan: elapsed time 52.4 seconds
pan: rate 708771.82 states/second
Case 2: the missing-acquire race #
Case 1 was within a single cluster of two CTAs, which share SMEM. A different protocol shows up when producer and consumer live in different clusters and coordinate through a GMEM atomic counter instead of an mbarrier.
To make this concrete, suppose we extend the Jacobi smoother to a small two-stage pipeline. A first set of producer clusters each smooths a separate array (one cluster per array) and writes the result to GMEM. A second consumer cluster, running afterward on the same GPU, reads the smoothed arrays and computes some summary (say, the sum of all of them). The producer and consumer never overlap in time logically, but they do execute concurrently from the hardware’s point of view: the consumer must observe each producer’s writes before reading them.
The DeepGEMM idiom for this is one int32 counter per produced array. When a producer finishes its array, it does an atomic release-add of 1 to its counter. The consumer spins on an acquire-load of the same counter until the count reaches the expected value, then reads the array. In CuTe DSL the consumer side is a one-line acquire-load loop:
The failure mode here is a silent race if the consumer reads without waiting. In Promela this is a safety property: [] (safety_violated == 0)
, with safety_violated
set when a consumer observes an array before the producer published it.
buggy — consumer reads without waiting
correct — consumer spins on the counter
SPIN’s response, both directions:
$ ./pan -a (buggy — consumer skips the wait)
ltl no_race: [] ((safety_violated==0))
pan:1: assertion violated !( !((safety_violated==0))) (at depth 34)
pan: wrote pipeline_protocol_bug.pml.trail
State-vector 112 byte, depth reached 34, errors: 1
12 states, stored
pan: elapsed time 0 seconds
$ ./pan -a (correct — consumer spins)
ltl all_consumed: <> ((consumed==2))
Full statespace search for:
never claim + (all_consumed)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
State-vector 104 byte, depth reached 92, errors: 0
1114 states, stored (2228 visited)
2057 states, matched
4285 transitions (= visited+matched)
pan: elapsed time 0 seconds
Towards automatic CuTe to Promela lowering #
Every model shown so far was hand-written (well, Claude-written) from CuTe DSL source. A natural follow-up question is whether a tool could read the kernel and emit Promela. The translation rules for individual primitives are mechanical, the main challenge is picking the subset of the kernel language to translate. We have implemented a simple proof-of-concept conversion library at github.com/cheshire/cute2promela repository.
The mechanical part: a pattern library
The CuTe DSL surface for synchronization is small. Roughly ten to fifteen call-site patterns cover everything in our codebase, and each maps to a fixed Promela fragment:
cute.arch.mbarrier_init(ptr, expected=N)
→ declareEXPECTED_ARRIVALS = N
, initializembar_count[slot] = 0
,mbar_phase[slot] = 0
.cute.arch.mbarrier_arrive(ptr)
→do_arrive(slot_of(ptr))
.cute.arch.mapa_shared_cluster(ptr, peer)
followed bymbarrier_arrive(remote, space="cluster")
→do_arrive(peer_slot)
, withpeer_slot
derived from the same allocation asptr
.cute.arch.mbarrier_wait(ptr, P)
→do_wait(slot_of(ptr), P)
; toggleP
per iteration as in the source.cute.arch.atomic_add(ctr, 1, sem="release", scope="gpu")
→atomic { counter[slot] += 1 }
.cute.arch.load(ctr, sem="acquire", scope="gpu")
in a spin loop with boundN
→atomic { counter[slot] >= N -> skip }
.
Using dataflow to pick translated subset
A standard backward slice from the sync call sites picks out exactly the lines a Promela model needs. The recipe is:
- Mark every statement whose op is a sync primitive (
mbarrier_*
, release/acquireatomic_*
, fences) or a cluster-topology call (mapa_shared_cluster
,cluster_rank_in_cluster
,thread_idx_x
,elect_one
) as a slice seed. - Close transitively backward through data dependences: a statement is kept if any of the values it defines is read by an already-kept statement.
- Everything else is datapath. Drop it.
To see what this produces on a kernel we’ve already discussed, we ran the slice on a hand-built IR for the Jacobi smoother from earlier. The IR has 29 statements; the slicer keeps 16 and drops 13. The complete output:
$ python scripts/slice_jacobi_to_promela.py
input statements : 29
slice kept : 16
slice dropped : 13
id kept op
-- ---- ----------------------------------------------------------------
0 yes my_cta = cluster_rank_in_cluster()
1 yes peer = 1 - my_cta
2 yes tid = thread_idx_x()
3 - cur = smem.alloc_array(...)
4 - nxt = smem.alloc_array(...)
5 yes halo = smem.alloc_array(...)
6 yes gate = smem.alloc_mbarrier()
7 yes elected = elect_one()
8 yes mbarrier_init(gate, expected=256)
9 yes mbarrier_init_fence()
10 - cur[tid] = arr_ptr[my_cta*HALF + tid]
11 yes phase = Int32(0)
12 yes is_tid0 = (tid == 0)
13 - my_edge = cur[HALF-1] if my_cta==0 else cur[0]
14 yes peer_halo = mapa_shared_cluster(halo, peer)
15 - peer_halo[0] = my_edge
16 yes fence_view_async_shared()
17 yes mbarrier_arrive(gate)
18 yes mbarrier_arrive_peer(gate, peer)
19 yes mbarrier_wait(gate, phase)
20 yes phase = phase ^ Int32(1)
21 - left = ... cur[tid-1] / halo[0] / cur[tid] ...
22 - right = ... cur[tid+1] / halo[0] / cur[tid] ...
23 - sum1 = left + cur[tid]
24 - sum2 = sum1 + right
25 - avg = sum2 / 3.0
26 - nxt[tid] = avg
27 - cur, nxt = nxt, cur
28 - arr_ptr[my_cta*HALF + tid] = cur[tid]
The slice doesn’t need any sync-specific reasoning, it is plain reverse reachability on a use-def graph, seeded from a list of names.
Two consequences worth naming:
Loop bounds tied to tensor dimensions don’t make it into the slice unless they gate sync. The persistent loop counter survives becausembarrier_wait
sits inside it; the inner stencil bounds don’t because they only gate the arithmetic. The lowering still has to pick a small concrete value for the surviving iteration count (3, in our case), but the slice tells it exactly which loops require that choice.Conditional sync is handled by the same mechanism. A warp-specialized region whose body contains anmbarrier_arrive
drags the warp-index test into the slice through the control dependence; a warp-specialized region whose body is pure compute is dropped wholesale. The slicer doesn’t need to know what warp specialization means, just that anif warp_idx == 2
guard defines a control value used by a kept statement.
A working proof of concept of the conversion pipeline is at github.com/cheshire/cute2promela: an ast
-based slicer and lowerer that takes the Jacobi smoother source from earlier as input, emits a Promela model, and round-trips through SPIN, and gets errors: 0
on the correct variant, an acceptance cycle on the hardcoded-phase variant. It supports a single protocol shape and isn’t a general-purpose CuTe analyzer; the “What this doesn’t do” section of the repo’s README is part of the design rather than a TODO.
Modeling rules #
Model the protocol shape, not the dimensions. 2 CTAs × 4 threads × 3 iters exercises the same interleavings as 2 CTAs × 128 threads × 30 iters. The bug class doesn’t depend on width; making the model wider trades verification time for nothing.Persistent kernels need at least three iterations. The hardcoded-phase bug only appears at iter 2. Models with fewer iterations pass without anything having been checked.Write the buggy twin alongside the correct model. Each*.pml
file gets a*_bug.pml
sibling that reintroduces the failure the model was built to rule out. It’s a regression test for the model itself: if SPIN stops finding the bug in the buggy file, the model has drifted and isn’t checking what we think it is.
Why not compute-sanitizer --tool synccheck #
?
compute-sanitizer
is a runtime tool: it instruments the kernel at launch and watches the execution that actually happens. It catches some real classes of warp-divergent barrier misuse, and when we’ve had a hang reproduce under it the diagnostic has been useful. It is not, however, a substitute for static checking: it requires hardware (and on many cloud and managed-GPU setups, additional permissions or a driver mode the platform doesn’t expose by default), only sees the one interleaving that the scheduler happened to take on that run, and finding no error under one launch is not evidence that other interleavings are safe.
References #
- Holzmann, G. J. (2003).
The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley. — Canonical reference for SPIN and Promela; covers the language, the verifier internals, and the LTL fragment in detail. - Holzmann, G. J. (1997). “The Model Checker SPIN”.
IEEE Transactions on Software Engineering23(5): 279–295.PDF— The original journal paper; freely available, much shorter than the book. - NVIDIA.
Parallel Thread Execution ISA,Parallel Synchronization and Communication Instructions. — Authoritative reference for
mbarrier.init
/arrive
/wait
/try_wait.parity
semantics, including the count + expected + phase state machine we model. - NVIDIA.
CUDA C++ Programming Guide,Thread Block Clusters. — Cluster semantics, DSMEM,mapa.shared::cluster
, and the cluster-scoped variants of mbarrier ops. - DeepSeek-AI.
DeepGEMM. — Source of the GMEM atomic-counter pattern used in Case 2 and discussed in the cross-cluster section. - NVIDIA.
Compute Sanitizer User Manual. — Documentation forcompute-sanitizer --tool synccheck
and the other runtime tools discussed in the “Why not compute-sanitizer?” section.
Conclusion #
We have shown how SPIN/Promela can be used for proving liveness properties, and presented a proof-of-concept tool for lowering from CuTe DSL to Promela automatically.