7661

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

@article{li2012parameterized,

   title={Parameterized Verification of GPU Kernel Programs},

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

   year={2012}

}

Download Download (PDF)   View View   Source Source   

788

views

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-2017 hgpu.org

All rights belong to the respective authors

Contact us: