Title
Verifying GPU kernels by test amplification
Abstract
We present a novel technique for verifying properties of data parallel GPU programs via test amplification. The key insight behind our work is that we can use the technique of static information flow to amplify the result of a single test execution over the set of all inputs and interleavings that affect the property being verified. We empirically demonstrate the effectiveness of test amplification for verifying race-freedom and determinism over a large number of standard GPU kernels, by showing that the result of verifying a single dynamic execution can be amplified over the massive space of possible data inputs and thread interleavings.
Year
DOI
Venue
2012
10.1145/2254064.2254110
PLDI
Keywords
Field
DocType
novel technique,verifying race-freedom,data parallel gpu program,standard gpu kernel,test amplification,thread interleavings,single test execution,verifying gpu kernel,possible data input,single dynamic execution,verifying property,gpu programming,determinism,information flow
Information flow (information theory),Programming language,CUDA,Determinism,Computer science,Parallel computing,Thread (computing),Real-time computing,Theoretical computer science,Test execution
Conference
Volume
Issue
ISSN
47
6
0362-1340
Citations 
PageRank 
References 
27
0.94
26
Authors
6
Name
Order
Citations
PageRank
Alan Leung1683.61
Manish Gupta2270.94
Yuvraj Agarwal31327102.62
Rajesh K. Gupta44570390.84
Ranjit Jhala52183111.68
Sorin Lerner698163.89