Parameterized Verification of GPU Kernel Programs

Author

Li, Guodong ; Gopalakrishnan, Ganesh

Author_Institution

Fujitsu Labs. of America, Sunnyvale, CA, USA

fYear

2012

fDate

21-25 May 2012

Firstpage

2450

Lastpage

2459

Abstract

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.

Keywords

computability; formal verification; graphics processing units; program debugging; GPGPU; GPU kernel program; SMT solver restriction; automated symbolic verifier; bank conflict elimination related optimization; bug-hunting method; functional correctness; functional equivalence; parameterized verification; Arrays; Computer bugs; Graphics processing unit; Instruction sets; Kernel; Optimization; Schedules; Correctness of Optimizations; Formal Verification; GPU Programming; Parameterized Reasoning; Satisfiability Modulo Theories (SMT); Symbolic Analysis;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Processing Symposium Workshops & PhD Forum (IPDPSW), 2012 IEEE 26th International

Conference_Location

Shanghai

Print_ISBN

978-1-4673-0974-5

Type

conf

DOI

10.1109/IPDPSW.2012.302

Filename

6270617