University of Utah
Search
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.

 

Publications

 

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 * pug-dev@cs.utah.edu
Disclaimer

Last updated on 01/03/2012