Parameterized Verification of GPU Kernel Programs
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}
}
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.
May 26, 2012 by hgpu
