Parameterized Verification of GPU Kernel Programs
Guodong Li, Ganesh Lalitha Gopalakrishnan · 2012
We present an automated symbolic verifier for checking the functional correctness of GPGPU kernels parametrically, for an arbitrary number of threads. Our tool 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 over-approximations, yielding an efficient bug-hunting method.