Scalable SMT-based verification of GPU kernel functions

Guodong Li, Ganesh Gopalakrishnan
School of Computing, University of Utah, UT, USA
In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (2010), pp. 187-196


   title={Scalable SMT-Based Verification of GPU Kernel Functions},

   author={Li, G. and Gopalakrishnan, G.},

   booktitle={18th ACM SIGSOFT Symposium on the Foundations of Software Engineering (SIGSOFT FSE)},



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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: