Paper Info
Title
Scalable SMT-based verification of GPU kernel functions
Abstract
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, bank conflicts, and wrong results. PUG's innovative ideas include a novel 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.
Year
DOI
Venue
2010
10.1145/1882291.1882320
SIGSOFT FSE
Keywords
Field
DocType
hundred cuda kernel,satisfiability modulo theories,gpu kernel function,cuda c.,user gpu program,invariant finding,exact analysis,barrier interval,scalable smt-based verification,graphical processing units,correct barrier placement,efficient gpu kernel,gpu programming,concurrency,formal verification,kernel function
CUDA,Concurrency,Computer science,Parallel computing,Theoretical computer science,Thread (computing),Gas meter prover,Kernel (statistics),Formal verification,Scalability,Satisfiability modulo theories
Conference
Citations 
PageRank 
References 
60
2.58
10
Authors
2
Name
Order
Citations
PageRank
Guodong Li123231.77
Ganesh Gopalakrishnan21619130.11