Parameterized verification of GPU kernel programs

Update Item Information
Publication Type pre-print
School or College College of Engineering
Department Computing, School of
Creator Gopalakrishnan, Ganesh
Other Author Li, Guodong
Title Parameterized verification of GPU kernel programs
Date 2012-01-01
Description We present an automated symbolic verifier for checking the functional correctness of GPGPU kernels parametrically, for an arbitrary number of threads. Our tool PUG 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.
Type Text
Publisher Institute of Electrical and Electronics Engineers (IEEE)
Volume 2012
First Page 2450
Last Page 2359
Dissertation Institution University of Utah
Language eng
Bibliographic Citation Li, G., & Gopalakrishnan, G. (2012). Parameterized verification of GPU kernel programs. Proceedings of the 2012 IEEE 26th International Parallel and Distributed Processing Symposium Workshops, IPDPSW 2012, art. no. 6270617, 2450-9.
Rights Management (c) 2012 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
Format Medium application/pdf
Format Extent 475,487 bytes
Identifier uspace,18017
ARK ark:/87278/s61r788z
Setname ir_uspace
ID 708205
Reference URL https://collections.lib.utah.edu/ark:/87278/s61r788z