Source-linked AI summary
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt, Gabriel Ebner, Abhinav Jangda, Madan Musuvathi, Tyler Sorensen
TL;DR
Tolerance-based testing leaves optimized GPU kernels difficult to trust. RESOLVE combines determinism testing, concurrency reduction, and formal proof; evaluation uncovered synchronization faults and previously unreported mega-kernel issues.
Problem
Method
Results
RESOLVE caught 92 injected synchronization faults and exposed four previously unreported issues in production mega-kernels, including two clear bugs.
Source: §8 · p. 12Takeaways & Limitations
RESOLVE supports validation of optimizations beyond the verifier’s direct semantic coverage by extending formal reasoning to kernels it cannot verify directly.
Source: §1 · p. 2, §8 · p. 12Binary instrumentation cannot expose asynchronous-load races, intra-warp races, or conflicts between CTAs never resident simultaneously; a clean campaign does not prove race freedom.
Source: §3.1 · p. 5, §6.2 · p. 9
Abstract
from arXiv · showhide
AI systems can now write and optimize production GPU kernels, but validating them remains an important challenge. Evaluating the kernel on a few random inputs and checking that its outputs match a trusted reference kernel within numeric tolerances is not sufficient: races can cause nondeterministic behavior that fails to manifest in tests, and numeric tolerances can hide bugs and cause false positives even after extensive calibration. To address this challenge, we present RESOLVE, which combines testing and formal verification to build a comprehensive kernel validation pipeline. It operates in three steps: First, it tests for nondeterminism using binary instrumentation that perturbs execution timing to expose races. Second, an agent rewrites the candidate and reference kernels to obtain "reduced-concurrency" versions that are simpler to analyze but still produce bitwise-identical outputs in all tests. Third, the reduced kernels are formally analyzed in the F*/Pulse framework and prove that they perform the same computation on real numbers. This sidesteps the need for numeric tolerances. We show that RESOLVE can validate a broad selection of kernels using KernelBench, and prove equivalence across fused GEMMs in three state-of-the-art frameworks and languages: CUTLASS, Triton, and Gluon. It also analyzes mega-kernels, notoriously difficult to validate, and finds four previously unreported issues, including two clear bugs. We show that agents can use RESOLVE to repair the issues, with minimal performance impact, highlighting that agents can optimize aggressively when they can rigorously check their results.
1 Introduction
RESOLVE addresses kernel validation challenges by pairing schedule-perturbation testing with reduced-concurrency kernels and formal proofs. Its evaluation finds errors missed by tolerance-based testing and validates repairs with little performance impact.
1 Introduction
- Reference-based testing can miss rare schedule-dependent races, while numerical tolerances can conceal bugs or reject valid floating-point optimizations.Direct formal verification is also constrained by verifier semantic coverage of modern GPU features.Source: §1 · p. 1
- Agents reduce concurrency in candidate and reference kernels while preserving each original’s bitwise behavior, bringing the programs within the verifier’s semantic coverage.RESOLVE checks repeated-run determinism and bitwise equivalence between each reduced kernel and its original.Source: §1 · p. 2
- Binary instrumentation perturbs scheduling-relevant operations to expose nondeterminism across languages and frameworks, without requiring source code.A lightweight memory analysis focuses perturbations on GPU scopes and regions with potentially conflicting accesses.Source: §1 · p. 2
- Agents translate the reduced kernels into Kuiper and prove both satisfy an algebraic specification derived from the trusted reference alone.The candidate therefore cannot influence the criterion used to judge it; the proof allows valid floating-point reorderings that change numerical results.Source: §1 · p. 2
- RESOLVE combines exact bitwise testing with formal verification, assigning concurrency correctness and functional correctness different validation techniques.Agents generate reductions, translations, specifications, and proofs, but their outputs must pass bitwise tests or formal proof checking.Source: §1 · pp. 1–2
- RESOLVE found four previously unreported mega-kernel issues, including two clear bugs, and repairs changed performance by less than 2% on three of four.The evaluation also identified two incorrect KernelBench candidates despite their passing the benchmark’s existing tolerance-based tests.Source: §1 · p. 2
2 GPU Background and Setup
The background explains GPU execution and memory hierarchies, the growing complexity of fused kernels, and why races and floating-point behavior complicate validation. The setup fixes kernel shapes and uses seeded, diverse test inputs and repeated executions.
2 GPU Background and Setup
- GPU kernels execute threads in warps, cooperative thread arrays, and grids, with registers, CTA-local shared memory, and device-wide global memory.Newer hardware adds a cluster level between a CTA and the grid.Source: §2 · pp. 2–3
- Triton, Gluon, and CUTLASS expose different levels of control, while SASS is the common NVIDIA binary foundation across languages and vendor libraries.Triton works over tiles; Gluon exposes layouts and memory movement; CUTLASS provides tuned C++ matrix-multiply building blocks.Source: §2 · p. 3
- Fusing operations reduces global-memory round trips but increases concurrency, while races and floating-point reordering can make outcomes schedule-dependent or bitwise different.The background describes synchronization at warp, CTA, and grid scopes and notes that reductions, fast-math, and tensor-core computation can change rounding.Source: §2 · p. 3
- The study assumes fixed tensor shapes, which makes each kernel issue a fixed number of memory accesses that can be traced and replayed under different schedules.ML kernels are often tuned or recompiled for the shapes they will actually process.Source: §2 · p. 3
2.1 RESOLVE Kernel Bench and Kernel Executors
- RESOLVE’s benchmark pairs KernelBench kernels with optimized candidates, and its executor hashes all memory after repeated runs for equality comparisons.Seeded inputs span ten per-operation distribution families, including degenerate values, awkward magnitudes, cancellation, and control-flow cases.Source: §2.1 · p. 3
3 Testing for Determinism
RESOLVE requires deterministic outputs and uses timing perturbations targeted by binary traces to test for schedule-dependent behavior. Its three-pass characterization narrows testing to possible conflicts, while leaving specific blind spots.
3 Testing for Determinism
- The determinism tester treats each kernel as a black box and checks whether the same input produces the same output on every run.RESOLVE delays selected memory operations and compares the perturbed output bitwise against an unperturbed run.Source: §3 · p. 3, §3.1 · p. 4
- Requiring determinism can reject correct kernels with legitimate nondeterminism, such as floating-point reductions whose atomicAdd order varies.Only one of 100 RKB kernels used floating-point atomicAdd; the others appeared deterministic on inspection and testing.Source: §3 · p. 4
3.1 Characterization
- Counting, tracing, and perturbation target possible conflicts; this reduces median RKB kernel test time to 88 seconds.The first pass counts memory accesses, the second locates potential conflicts, and the third inserts delays.Source: §3.1 · pp. 4–5
- Figure 2 spans roughly four orders of magnitude in memory-reference events per RKB problem, with most between 10^8 and 10^10 and the largest above 10^11.P31 and P32 have zero such events and are excluded from the figure.Source: Figure 2 · p. 4, §3.1 · p. 4
- 41 of 100 RKB kernels had no traced potential conflicts, 59 had shared-memory conflicts within a block, and 8 also had global-memory conflicts across blocks.All four issues found in the mega-kernels were at the global-memory, across-block scope.Source: Figure 3 · p. 5, §3.1 · p. 5
- A clean campaign is not proof of race freedom: binary-level perturbation cannot reach asynchronous loads, intra-warp interleavings, or conflicts between nonresident CTAs.The authors characterize surviving the campaign as language-agnostic, black-box evidence of deterministic behavior.Source: §3.1 · p. 5
4 Reduction
RESOLVE reduces deterministic kernels to simpler versions that are easier to verify while preserving each original's bitwise behavior on tested inputs. The reduction removes concurrency where possible but retains the minimum required by certain hardware instructions.
4 Reduction
- Reducing concurrency addresses the verifier's difficulty modeling asynchronous copies, TMA, producer-consumer pipelines, and their coordinating barriers.The paper identifies formalization of these constructs and their synchronization corner cases as lagging behind hardware.Source: §4 · p. 5
- If candidate and reference outputs already agree bitwise on every test, RESOLVE stops without reduction or proof; 15 of 100 RKB pairs did so.In that case, the candidate has been tested to compute a function matching the reference.Source: §4 · p. 5
- Concurrency constructs such as barriers, atomics, cooperative launches, and warp primitives are rejected; splitting a fused kernel into multiple launches is allowed.The reduction minimizes concurrency rather than launch count, and repeated statements should become loops or shared functions.Source: §4 · pp. 5–6
- The reduction usually reaches a single thread, but retains a single warp for tensor-core instructions and four warps for Hopper warpgroup instructions.The minimum concurrency is set by the instruction; Kuiper provides real-number semantics for these instructions.Source: §4 · p. 6
- A reduction is accepted only when it reproduces its original kernel's output bitwise on every tested input, without tolerance or normalization.Accepted reductions produce simplified programs that a verifier can reasonably handle.Source: §4 · p. 6
5 Proof
RESOLVE connects reduced kernels to verified programs through bitwise testing, then proves both satisfy a common, tightly defined specification over the reals. This can accept bitwise-different implementations of the same algebraic computation, but not every numerically close approximation.
5 Proof
- The proof reasons about the real-valued algebraic expression rather than requiring floating-point outputs to be exactly equal or merely within a chosen tolerance.The Kuiper approximation relation lets differently ordered floating-point operations be related to the same real expression.Source: §5 · p. 6
- The proof stage links each reduced kernel to a bit-equivalent Kuiper implementation, then proves both Kuiper programs satisfy a common functional specification.The specification is derived from the trusted reference alone, and the candidate cannot influence it.Source: §5 · pp. 6–7, Figure 4 · p. 7
- RESOLVE rejects some practically close approximations when their idealized real-number results differ, such as degree-10 and degree-11 Taylor series for e^x.The authors identify concrete error budgets as possible future work for handling such optimizations.Source: §5 · pp. 6–7
- A shared specification is insufficient if it is weak: the real-number output must be precisely defined, and automated checks for tightness remain future work.The authors use human review to validate specification tightness.Source: §5 · p. 7
- Both programs satisfying the same tight specification establishes that the candidate computes the function defined by the reference, even when their output bits differ.The specification must precisely define the real-number result; the authors ask agents to construct tight specifications and use human review to validate them.Source: §5 · p. 7
6 Evaluation
RESOLVE was evaluated on KernelBench candidates, fused MLP kernels, and production mega-kernels. It found incorrect kernels and nondeterministic behavior, validated fused implementations, and supported repairs, with coverage limited by unsupported operations and reduction capabilities.
6 Evaluation
- The determinism tester is designed for tight-loop use, while agent-driven reduction, specification, and proof are slower and costlier in a pipeline intended to run without human interaction.Specification and proof took four times as long as reduction and consumed more than a hundred times the tokens.Source: §6 · p. 7, §6.2 · p. 8
6.1 Setup
- The KernelBench study carried 14 of the 85 remaining candidates through the full workflow after drawing two samples from each input distribution; the authors describe this choice as keeping the study tractable.Baselines were PyTorch eager-mode kernels assumed deterministic, with informal tester runs corroborating that assumption.Source: §6.1 · p. 7, §6.2 · p. 8
6.2 KernelBench Level 1
- Two of 17 KernelBench candidates classified by determinism testing were empty kernels that passed the benchmark’s tolerance tests, while 11 of 14 full-workflow cases completed verification.The two incorrect candidates were an elementwise ELU and a hardtanh; every specification used in the completed proofs was inspected and found tight.Source: §6.2 · p. 8, Table 1 · p. 8
- The full workflow could not complete for all KernelBench cases: inline PTX operations lacked Kuiper wrappers in two, and a Taylor-approximated sigmoid could not be proved algebraically equivalent.The sigmoid result does not establish that the candidate is buggy; assessing such approximations requires numerical-tolerance reasoning, which RESOLVE does not provide.Source: §6.2 · p. 8
- The determinism tester flagged 92 of 143 synchronization mutants; 28 misses had races that never changed the final value, while 20 placed conflicts within one warp.Three other misses affected code that never ran; the in-warp cases were beyond the reach of the binary instrumentation used.Source: §6.2 · p. 9
- At 100 million trace records, the conflict inventory was complete and unchanged at 200 and 400 million, while tracing time continued to rise; two CTAs found every indicator in this suite.The default budget is 200 million records, one step beyond inventory saturation.Source: §6.2 · p. 9, Figure 5 · p. 9
6.3 A Fused MLP Kernel
- RESOLVE established equivalence of all three fused MLP variants against the PyTorch reference; Gluon and Triton were bitwise identical, so only Gluon needed specification and proof.Determinism testing took several times longer than for RKB kernels because the MLPs ran at deployed-model sizes, with more memory traffic to trace.Source: §6.3 · pp. 9–10, Table 3 · p. 10
6.4 Mega-Kernels
- Across three mega-kernels, RESOLVE found four root causes—two clear LUCE bugs and two capacity-dependent routing behaviors whose bug status remains open—and agents repaired the issues.The two LUCE repairs were marginally faster, FlashMoE’s repair cost under 1%, and FastMoE’s cost 10%.Source: §6.4 · pp. 10–11
7 Related Work
Prior work offers distinct ways to reason about race freedom, determinism, optimization, and GPU semantics, but each has limits for highly optimized kernels. RESOLVE instead tests binaries under perturbation and verifies reduced programs against a shared specification.
Determinism and race freedom
- Data-race freedom supports sequentially consistent reasoning, while determinism also supports schedule-independent reasoning and has been checked at runtime.Determinism checking also has a history in Cilk, and type systems can guarantee it statically on CPUs and GPUs [20].Source: §7 · p. 11
- Lipton reduction and sequentialization provide complete guarantees but require source code, whereas RESOLVE perturbs binaries and observes outputs.The approach applies to compiled kernels from Gluon and CUTLASS; the paper also reports mutants that escape detection.Source: §7 · p. 11
Verified optimizers
- CompCert verifies a compiler and Exo restricts schedules to semantics-preserving transformations, while translation validation checks individual optimizations or substitutions.RESOLVE instead derives a specification for each problem and verifies both programs against it.Source: §7 · p. 11
- RESOLVE checks each problem individually and uses a separate equivalence notion by deriving a natural specification that both programs must satisfy.This contrasts with approaches that check whether an optimizer preserves equivalence between its input and output.Source: §7 · p. 11
GPU semantics
- GPU formal semantics often lag hardware, and scoped data-race freedom covers only programs that respect the scopes [29, 16].RESOLVE’s determinism tester does not require formal models of each hardware feature, but Kuiper still needs semantics for features used in reduced kernels, blocking some thread-local operations [32].Source: §7 · pp. 11–12
8 Conclusion
RESOLVE combines testing, reduction, and proof to validate optimized GPU kernels across languages and frameworks. It caught synchronization faults and previously unreported production issues in its evaluation.
8 Conclusion
- 92 injected synchronization faults were caught, and RESOLVE found four previously unreported production mega-kernel issues, including two clear bugs.The evaluation also covered 31 KernelBench Level 1 kernels, three fused MLP implementations in CUTLASS, Triton, and Gluon, and a mixture-of-experts kernel.Source: §8 · p. 12