Racer finds hidden bugs in gpu kernels with symbolic checking
Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking
Symbolic ComputationArtificial Intelligence
Summary
Modern GPU programs often have many versions written for different hardware and purposes, and each new version needs to produce the same results as the old one. Normally, people test them by running a few examples and comparing results, but this can miss subtle bugs that hide inside normal-looking outputs. The authors made Racer, a tool that analyzes GPU programs using math symbols instead of just examples. It checks if two versions always produce exactly the same outputs, which helps find errors that regular testing would miss.
What this means in practice
- •For gpu kernel developers: Verify that optimized GPU kernels are functionally equivalent to references across all inputs to catch subtle bugs missed by conventional testing.
- •For compiler engineers: Use Racer to ensure that code transformations and optimizations preserve exact program behavior on GPUs, improving reliability of generated code.
Authors
Tuan Truong Vu, Cheng Tan
Abstract
GPU kernels are critical to the performance of today's AI services, yet the same operators are rewritten repeatedly: for each GPU generation, numeric format, serving regime, and kernel language. Every rewrite must preserve the function computed by the implementation it replaces. Today, this obligation depends almost entirely on differential testing: run the new kernel and a trusted reference on randomly sampled tensors, then compare their outputs within a tolerance. This approach has blind spots that additional test cases cannot eliminate. For example, a logical bug may produce an error smaller than the tolerance required to accommodate a correct optimized kernel. We propose symbolic equivalence checking, which executes a kernel and its reference on symbolic inputs, turning each output cell into an exact algebraic expression, and then checks whether the paired expressions agree for all inputs. Because these expressions are exact, symbolic equivalence checking distinguishes floating-point error from logical bugs, while a single check covers the entire input space. We implement Racer, a PTX-level symbolic equivalence checking engine, with three techniques that make this approach practical for production kernels: (1) Shape Reduction to control checking cost, (2) a lockstep CTA scheduler to handle concurrency, and (3) idiom templates with exact numeric refutation for otherwise inconclusive results. Across 2,408 production kernels from 41 collection targets, Racer found 82 real bugs in 23 libraries, including 76 previously unknown bugs and 41 confirmed so far.