Paper Info
Title
Interleaving and lock-step semantics for analysis and verification of GPU kernels
Abstract
We study semantics of GPU kernels -- the parallel programs that run on Graphics Processing Units (GPUs). We provide a novel lock-step execution semantics for GPU kernels represented by arbitrary reducible control flow graphs and compare this semantics with a traditional interleaving semantics. We show for terminating kernels that either both semantics compute identical results or both behave erroneously. The result induces a method that allows GPU kernels with arbitrary reducible control flow graphs to be verified via transformation to a sequential program that employs predicated execution. We implemented this method in the GPUVerify tool and experimentally evaluated it by comparing the tool with the previous version of the tool based on a similar method for structured programs, i.e., where control is organised using if and while statements. The evaluation was based on a set of 163 open source and commercial GPU kernels. Among these kernels, 42 exhibit unstructured control flow which our novel method can handle fully automatically, but the previous method could not. Overall the generality of the new method comes at a modest price: Verification across our benchmark set was 2.25 times slower overall; however, the median slow down across all kernels was 0.77, indicating that our novel technique yielded faster analysis in many cases.
Year
DOI
Venue
2013
10.1007/978-3-642-37036-6_16
ESOP
Keywords
Field
DocType
novel method,gpu kernel,unstructured control flow,arbitrary reducible control flow,traditional interleaving semantics,previous method,novel lock-step execution semantics,commercial gpu kernel,new method,lock-step semantics,similar method
Graphics,Local outlier factor,Programming language,Lock (computer science),Computer science,Control flow,Parallel computing,Theoretical computer science,While loop,Semantics,Interleaving,Generality
Conference
Volume
ISSN
Citations 
7792
0302-9743
14
PageRank 
References 
Authors
0.62
15
4
Name
Order
Citations
PageRank
Peter Collingbourne1965.33
Alastair F. Donaldson266152.35
Jeroen Ketema316013.52
Shaz Qadeer43257239.11