Parameterized Verification of GPU Kernel Programs

Guodong Li, Ganesh Gopalakrishnan
Fujitsu Labs of America, Sunnyvale, CA
Multicore and GPU Programming Models, Languages and Compilers Workshop (IPDPS workshops), 2012


   title={Parameterized Verification of GPU Kernel Programs},

   author={Li, Guodong and Gopalakrishnan, Ganesh},



Download Download (PDF)   View View   Source Source   



We present an automated symbolic verifier for checking the functional correctness of GPGPU kernels parametrically, for an arbitrary number of threads. Our tool PUGpara checks the functional equivalence of a kernel and its optimized versions, helping debug errors introduced during memory coalescing and bank conflict elimination related optimizations. Key features of our work include: (1) a symbolic method to encode a comparative assertion across two kernel versions, and (2) techniques to overcome SMT solver restrictions through overapproximations, yielding an efficient bug-hunting method.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: