PUG - Prover of User GPU programs
|
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.2 based on Yices : (Static Checker)
|
Version - 0.3 (we are porting this version to GKLEE)
|
-
Version 0.3 based on Microsoft's Z3 : Static Checker, Property Checker, Equivalence Checker (reimplemented in the parameterized GKLEE)
-
Coming soon.
-
Coming soon.
-
Coming soon.
|
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
