University of Utah
School of Computing
Home People Research Admissions Site Map  

PUG PUG - Prover of User GPU programs

About PUG

Interest in Graphical Processing Units (GPUs) is skyrocketing due to their potential to yield spectacular performance on many important computing applications. Unfortunately, writing such efficient GPU kernels requires painstaking manual optimization effort which is very error prone. We contribute the first comprehensive symbolic verifier for kernels written in CUDA C. Called the 'Prover of User GPU programs (PUG)', our tool efficiently and automatically analyzes real-world kernels using Satisfiability Modulo Theories (SMT) tools, detecting bugs such as data races, incorrectly synchronized barriers, and wrong results. PUG's innovative ideas include an efficient approach to symbolically encode thread interleavings, exact analysis for correct barrier placement, special methods for avoiding interleaving generation, dividing up the analysis over barrier intervals, and handling loops through three approaches: loop normalization, overapproximation, and invariant finding. PUG has analyzed over a hundred CUDA kernels from public distributions and in-house projects, finding bugs as well as subtle undocumented assumptions.




Version - 0.1


Version - 0.2


Version - 0.3 (we are porting this version to GKLEE)

Links to Tools and Related Work

PUG uses the following compilers, libraries, solvers and other tools: Major components of PUG are being merged into GKLEE to address the syntax parsing problem and gain better performance.

School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT 84112 *

Last updated on 01/03/2012