Towards Unified Analysis of GPU Consistency

GPUs reorder memory operations far more freely than CPUs, and although Nvidia and Khronos have published formal memory models for PTX and Vulkan, the only tools that could check code against them handled straight-line pseudo-assembly of a few instructions, one model each, no loops, no liveness — this paper rewrites both models in the .cat language, adds GPU notions like scopes, proxies and availability, plugs them into the Dartagnan bounded model checker with a front end for real SPIR-V, verifies real spin locks and an inter-workgroup barrier with over a hundred events in seconds to minutes, and along the way finds two bugs in Nvidia's PTX tool and one in the Vulkan model itself.

The argument in one glance

Problem

GPU memory models are formal now, but nobody can check real code against them

After thirty years CPU consistency is well understood and well tooled. GPUs are not: they reorder aggressively, they add memory scopes, non-coherent caches called proxies, and cache-control flags, and until recently their guarantees were folklore. Nvidia formalized PTX and Khronos formalized Vulkan, so precise answers exist. But reading those models takes rare expertise, and the tools shipped with them handle only tiny straight-line tests.
What people did

Alloy prototypes shipped with each model

Both the PTX mixed-proxy model and the Vulkan model come with an Alloy specification and a small checker that decides whether a given litmus test outcome is allowed. Researchers had also written earlier .cat models of GPU fragments, but their tool support was discontinued.
Why it fell short

Straight-line only, one model per tool, no liveness, and exponential blow-up

The Alloy tools accept pseudo-assembly with no control flow, so no spin loops, no real kernels. Each is tied to one model version; PTX 6.0 has no tool at all. Neither can detect a thread that spins forever. And Alloy search grows exponentially: the PTX tool runs out of memory past about 50 events and the Vulkan tool past about 20. The paper also found that the PTX 7.5 tool defined morally-strong wrongly and allowed out-of-thin-air behaviors its own model forbids.
This paper's idea

One language, one checker, three models, real code

The authors extend the .cat memory-model language with GPU features, new base relations for scopes, same-virtual-address, barrier and fence synchronization, and new event tags for proxies, storage classes and availability or visibility, and write PTX 6.0, PTX 7.5 and Vulkan in it. They integrate all three into Dartagnan, a bounded model checker that encodes program plus model as an SMT formula, adding relation-analysis bounds and encodings for every new relation, a liveness check for spin loops, and three front ends including real SPIR-V assembly. The result checks safety, liveness and data-race freedom, supports 776 litmus tests where the Alloy tools support 343, scales linearly where Alloy scales exponentially, and verifies real locks and the XF inter-workgroup barrier, proving that every barrier and scope in them is necessary. Validation also exposed a bug in the Vulkan model where two atomic read-modify-writes could read the same value.

Why this problem is worth solving

The paper opens with a small OpenCL kernel, the portable XF barrier, that lets threads in different workgroups synchronize: leaders in workgroup zero spin on flags set by a representative of each follower workgroup, everyone meets on a control barrier, and the leaders release their followers. The original implementation used plain loads and stores and, on real hardware, could hang and race; making the accesses atomic with release-acquire semantics was known empirically to fix it. What nobody could do was prove that the atomic version is correct, or that none of its barriers can be weakened. Section 6 of the paper does both, automatically.

The stakes reach past academic barriers. The paper reproduces a real Mesa NIR compiler bug: seeing a spin loop with no memory barrier inside it, the compiler deleted the loop as side-effect-free, breaking a message-passing pattern that Vulkan’s model guarantees. Agreeing that this was unsound was hard partly because the model was under-specified and partly because the engineers misread its guarantees. It reproduces a work-stealing deque used on GPUs that was buggy until fences were added, and a libcu++ ticket mutex that carries an unnecessary acquire on its ticket increment. A

consistency model

A specification of which values a read may return in a concurrent program, defined by the reorderings and visibility rules the hardware or language permits.

answers all of these questions precisely, but only if a tool can apply it to the code as written.

What people did before, and where it broke

Alloy tools for PTX 7.5 and Vulkan. Decide allowed outcomes of litmus tests written in pseudo-assembly. Where it broke. No control flow at all, so no loops and no real programs; one tool per model, with PTX 6.0 unsupported and the PTX parser tied to 7.5; no liveness; exponential search that exhausts memory at a few dozen events. The PTX 7.5 tool also mis-defined morally-strong and permitted out-of-thin-air results, both reported by the authors.
Earlier .cat models of GPU fragments. Formalized subsets of PTX, OpenCL and HSA in the language used for CPU models. Where it broke. They predate scopes as used today, omit proxies and cache control, and their tooling was discontinued; herd7 dropped PTX support.
GPUVerify. A static analyzer for data races in GPU kernels. Where it broke. It supports strong atomics only, not the relaxed atomics real GPU APIs now rely on, and it reports false positives even with strong accesses, flagging a race inside the critical section of a compare-and-swap lock.
Empirical litmus campaigns such as GPUHarbor. Run thousands of tests on real hardware. Where it broke. They test a small set of common weak patterns and their mutants, not GPU-specific features like address spaces, aliasing and cache control, and they observe rather than prove.
The gap. No tool could take a real GPU program with loops, choose among the vendors’ formal models, and decide safety, liveness and race freedom at a scale of a hundred or more events.

Where the work sits

From a GPU program and a model to a verdict

Program new

A litmus test in PTX or Vulkan syntax, or real SPIR-V assembly compiled from OpenCL with clspv; may contain loops, barriers and atomics.
↓ →
Model in .cat new

PTX 6.0, PTX 7.5 with proxies, or Vulkan, written in the extended .cat with GPU relations and tags.
↓ →
Relation analysis new

Compute lower and upper bounds for every base relation, including the new scope, barrier, fence and virtual-address relations, and propagate to derived relations.
↓ →
SMT encoding new

Encode events, base relations, and the model's axioms as a formula; partial coherence for PTX via clocks.
↓ →
Solver

An off-the-shelf SMT solver searches for a behavior violating the property.
↓ →
Verdict new

Safety (exists or forall), data-race freedom per the model, or liveness of spin loops.

Dartagnan already handled CPU models this way; the new boxes are what GPU support required. Bounded means loops are unrolled to a chosen depth.

The idea

Models as relations and axioms. In the

.cat language

A domain-specific language for consistency models: define sets of events and relations over them, then state axioms that relations must be acyclic, irreflexive or empty.

, a program execution is a graph of events, reads, writes, fences, barriers, joined by base relations: program order, reads-from, coherence order, same-location. A model derives new relations by union, intersection, composition and inverse, and states axioms. A behavior is allowed if it satisfies every axiom. The same language describes x86, Arm, Power and the Linux kernel, which is exactly why the authors chose it over Alloy: two GPU models in one language can be compared feature by feature.

What GPUs add. The paper extends .cat in two directions. New base relations capture structure that CPUs lack: sr and scta for events within reach of a given

scope

A level of the GPU memory hierarchy that a set of threads can synchronize through: a compute-thread array or workgroup, the device, or the whole system.

, ssg, swg and sqf for Vulkan’s subgroup, workgroup and queue-family scopes, ssw for system-synchronizes-with, syncbar and sync_barrier for control barriers sharing an identifier, sync_fence for morally-strong sequentially consistent fences, and vloc for accesses to the same virtual address through the same reference. New event tags mark acquire, release and relaxed atomics; PTX

proxies

A path to memory with its own cache: generic, texture, surface or constant in PTX; two accesses through different proxies may see different values until a proxy fence.

GEN, TEX, SUR, CON and the ALIAS fence between them; Vulkan storage classes SC0 and SC1 and their semantics; and Vulkan’s

availability and visibility

Vulkan cache-control flags: a write must be made available to a cache level, and a read must have visibility of it, before release-acquire ordering alone guarantees observation.

flags AV, VIS and their device-scope forms.

PTX in .cat. Two things distinguish PTX. First, coherence is not a total order over writes to a location: two weak writes are ordered only if morally strong or causally related, so two other threads may observe them in opposite orders, the paper’s Figure 6. The authors relax .cat’s notion of a well-defined execution so co can be partial for PTX, with transitivity enforced explicitly. Second, morally-strong, only informally described by Nvidia, gets a formal definition: two operations are morally strong if they are in program order or both strong and in a common scope, if they use the same proxy, and if as memory operations they overlap completely. Proxy-aware causality then says that operations over the same proxy get the ordinary PTX guarantees, and crossing proxies requires the matching proxy fence.

Vulkan in .cat. Vulkan defines one base relation per inner scope and intersects each with the events whose scope tag is large enough. Its happens-before is not transitive: a chain of release-acquire edges through a third thread does not by itself guarantee that the last reader sees the first write; an availability-visibility chain, requiring a semav annotation on the intermediate release, is needed. This makes Vulkan resemble HRF-indirect models, where threads synchronize indirectly through a third party at different scopes. Data races are defined the way C11 does: two accesses to a location, one a write, not mutually-ordered atomics and not location-ordered, are flagged, and a racy program is undefined. Weak writes that PTX merely leaves unordered are, in Vulkan, a race.

Making it scale. Dartagnan’s relation analysis computes for each relation a lower bound, pairs definitely related, and an upper bound, pairs possibly related, so only the difference needs an SMT variable. For the new static relations, scope membership, same-CTA, barrier identifiers, both bounds are computed from the source: threads are related if their declared scopes match and they are visible to each other at that scope. For vloc, a field-sensitive Andersen alias analysis decides must- and may-alias. sync_fence has an empty lower bound and an upper bound of all sequentially consistent fences; it is encoded as a partial order with clock variables, total within each CTA. PTX’s partial co is likewise encoded with clocks rather than a total order.

Liveness. A spin loop that reads the coherence-maximal write of its location and still does not exit can never be helped by its own thread. If every other thread is also spinning or finished, no write will ever arrive: a liveness violation. Dartagnan finds these under a forward-progress assumption that every enabled thread is eventually scheduled, which real GPUs do not strictly promise, so a “no violation” verdict is not a guarantee, but every reported violation is real.

Tracing a check on the XF barrier

Is the atomic XF barrier correct, and is every barrier needed?

Follows Section 6 and Table 7. The barrier is compiled from OpenCL to SPIR-V with clspv, then checked under the Vulkan .cat model. A 3.3 grid means 3 threads per workgroup, 3 workgroups: 9 threads.

Step 1 of 6

Compile and parse

The OpenCL kernel of Figure 1, with atomic flags and CLK_GLOBAL_MEM_FENCE control barriers, is compiled by clspv to SPIR-V and disassembled. Dartagnan's SPIR-V front end produces a program with three workgroups of three threads: a leader group and two follower groups, each with a representative. Loops are unrolled to a bound.

grid 3.3 | threads 9 | events 457 after unrolling | model: spirv.cat (Vulkan)

Why it works

One language exposes the real differences. Writing PTX and Vulkan side by side in .cat, rather than in two Alloy specifications with different vocabularies, makes their agreements and disagreements explicit: same virtual-address concept, same scope idea, but partial versus total coherence, unordered weak writes versus races, transitive versus non-transitive happens-before.
Bounds shrink the formula. Almost every new GPU relation is static: whether two events share a scope, a barrier identifier or a virtual address is known from the source. Because their lower and upper bounds coincide, they cost no solver variables, and the SMT formula stays close to the size of a CPU model’s.
Clocks handle partial orders. PTX’s non-total coherence and the partial sync_fence order would be awkward as Boolean pair variables; an integer clock per event encodes “ordered before” compactly and lets the solver leave unrelated pairs unordered.
Real front ends make real code reachable. Supporting SPIR-V, with control flow and loops unrolled to a bound, is what lets the tool check compiled OpenCL locks and barriers rather than hand-written straight-line fragments.
Co-maximality gives a sound liveness test. A spinning read of the latest write that still does not exit cannot be rescued by any future write if no thread can progress, so every violation reported is genuine even though absence is not proven.

What it costs

Bounded, not unbounded. Loops are unrolled to a chosen depth, so the checker verifies the program up to that bound and a given test harness; it does not prove an algorithm for all inputs or thread counts.
Progress is assumed. GPUs do not promise that every enabled thread is eventually scheduled, so a liveness verdict of “safe” can be a false negative.
Liveness ignores scopes. The liveness encoding uses coherence without scope information, so a spin loop reading a co-maximal write from out of scope is treated as a violation even though such operations should not synchronize; none of the validation tests hit this, and moving liveness into .cat is future work.
Static references only. vloc is encoded as a static relation because only static memory references are supported; dynamic aliasing through computed addresses is not modeled.
Feature coverage of real kernels is partial. Of GPUVerify’s 486 OpenCL kernels, 225 failed to compile with clspv, 84 were trivially race-free after dead-code removal, and of the remaining 177 Dartagnan could verify 66; the rest use floating point or other unsupported features. Exchange-based spin loops are excluded from liveness because they make coherence not prefix-finite.
Correct programs are slower to verify than buggy ones. Proving the XF barrier correct takes 13.6 seconds and the test-and-test-and-set lock 65.6 seconds, because the solver must exhaust the space; bugs surface in one to three seconds.

The evaluation

All experiments ran on an 11th-generation Intel Core i5-1135G7 at 2.4 GHz with 16 GB of RAM. The litmus suite collects the original tests shipped with both Alloy models, the tests from the PTX formalization papers, the examples in this paper, common weak patterns, and 73 forward-progress tests ported from GPUHarbor: 179 PTX tests without proxies, 129 with proxies, and 289 Vulkan tests.

Litmus tests supported: Dartagnan versus the Alloy-based tools (Table 5)

Property	Alloy tool	Dartagnan
PTX 6.0: safety / liveness / DRF, tests, ms per test
PTX 7.5 with proxies
Vulkan
Scaling with thread count (MP, SB, LB, IRIW)
Bugs found during validation		—

For every test both tools support, verdicts agree, which is the paper's validation of its .cat translations. Against GPUVerify on 66 compiled OpenCL kernels (Table 6), Dartagnan averages 1,679 ms per kernel versus 1,172 ms, agrees on 59, matches source-code comments where GPUVerify contradicts them in 4 of the 7 disagreements, and cannot yet check barrier divergence in 2.Underlined values explain themselves when clicked.

Table 7 is the paper’s claim to real code: three lock implementations (compare-and-swap, ticket, test-and-test-and-set) and the XF barrier, written in OpenCL, compiled to SPIR-V, and checked for safety, liveness and races under Vulkan. All four are correct with release-acquire barriers at device scope, in 14 to 66 seconds. Weakening any acquire or release to relaxed produces a bug in about two seconds. Keeping the orderings but shrinking scope from device to workgroup is correct when all threads share a workgroup (a 4.1 grid) and incorrect when they do not (4.2), because instructions cannot synchronize across a scope they do not cover. The XF barrier needs at least two workgroups to be meaningful and is verified correct with three workgroups of three threads, 457 events.

In an actual implementation

Three bugs the models catch

The NIR compiler bug (Figure 10 and 11): a thread spins on a flag with an acquire barrier inside the loop; hoisting the barrier out of the loop is sound under Vulkan, but the compiler then saw a barrier-free spin loop and deleted it, allowing stale data. The ABP work-stealing deque (Figure 12): without a fence between writing the task and incrementing the tail index, PTX does not order the two weak writes, so a thief can read the new index and the old task; adding the fences makes the behavior forbidden, which Dartagnan confirms under PTX. The libcu++ ticket mutex (Figure 13): it is correct, but its atomic ticket increment is acquire when relaxed suffices, and the tool shows the relaxation preserves mutual exclusion, an optimization developers avoid by hand because the corner cases are hard to enumerate.

Where this stops working

Everything is bounded model checking: results hold for the specific test harness, thread grid and loop depth checked, not for the algorithm in general. Liveness rests on a forward-progress assumption that GPU specifications do not commit to, so only violations, never their absence, should be trusted, and the liveness encoding currently ignores scopes. Only static memory references are supported, so kernels with computed addresses, floating point, or barrier-divergence concerns fall outside the tool, which is why only 66 of GPUVerify’s kernels could be checked. The models are validated against the vendors’ own litmus suites and examples, which the authors note is thinner than the large testing campaigns behind CPU models, and no litmus generator yet targets GPU-specific features like proxies and cache control.

Background

Why GPU models needed new words

A CPU model can assume that all cores see one coherent memory. GPUs break that assumption twice. Threads are grouped hierarchically, and synchronizing within a workgroup is far cheaper than across the device, so every atomic and fence carries a scope saying how far its guarantee reaches; an acquire at workgroup scope simply does not pair with a release from another workgroup. And graphics hardware routes texture, surface and constant memory through separate non-coherent caches, so the same address read through two paths, two proxies, can show two values until a proxy fence reconciles them. Vulkan adds a third twist: because it targets many vendors’ caches, it lets programs say explicitly when a write must be made available and when a read must be made visible, rather than assuming release-acquire does both. None of these has a CPU analogue, which is why .cat needed new base relations and tags before the GPU models could be written in it.

If you remember only three things

1. GPU consistency models from Nvidia (PTX) and Khronos (Vulkan) are formal but were usable only through Alloy prototypes that accept loop-free pseudo-assembly, handle one model each, cannot check liveness, and run out of memory beyond a few dozen events. Developers of GPU locks, barriers and compilers therefore worked from intuition, and the paper shows a compiler bug, a deque bug and an unnecessary fence that resulted.
2. The paper extends the .cat language with GPU base relations (scopes, same-virtual-address, barrier and fence synchronization) and event tags (proxies, storage classes, availability and visibility), writes PTX 6.0, PTX 7.5 and Vulkan in it, and integrates them into the Dartagnan bounded model checker with relation-analysis bounds, clock-based encodings for PTX's partial coherence, a co-maximality liveness check for spin loops, and front ends for PTX, Vulkan litmus syntax and real SPIR-V.
3. Dartagnan supports 776 litmus tests to the Alloy tools' 343, agrees on every shared test, scales linearly where Alloy scales exponentially, and verifies real compare-and-swap, ticket and test-and-set locks and the XF inter-workgroup barrier in seconds to about a minute, showing each barrier and scope is necessary. Validation found two bugs in the PTX 7.5 tool and one in the Vulkan model. Limits: bounded checking, an assumed progress model, scope-unaware liveness, static references only, and partial coverage of real kernels.

Check yourself

Check your understanding

1. What is a memory scope, and why does it matter for whether two atomics synchronize?
2. How does PTX coherence differ from CPU coherence, and how did the authors handle it in .cat?
3. Predict what happens if a Vulkan program relies on a chain of release-acquire edges through a third thread, with no availability flag on the intermediate release.
4. Why can Dartagnan report liveness violations but not guarantee liveness?
5. What did the validation reveal about the vendors' own tools and models?

Sources

The paper is “Towards Unified Analysis of GPU Consistency” by Haining Tong, Natalia Gavrilenko, Hernán Ponce de León and Keijo Heljanko, University of Helsinki, Huawei Dresden Research Center and Helsinki Institute for Information Technology, published at ASPLOS 2024, Volume 4, DOI 10.1145/3622781.3674174, under a Creative Commons Attribution licence. This explainer was written from the full text of the author-hosted copy, including its artifact appendix. Numbers are taken from Tables 5 to 7 and Figures 1 to 16. The Dartagnan tool and the .cat models for PTX 6.0, PTX 7.5 and Vulkan are open source at github.com/hernanponcedeleon/Dat3M, and the artifact is archived on Zenodo (record 12516539).