Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer
Imperial College London
22nd European Symposium on Programming (ESOP 2013), 2013


   title={Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels},

   author={Collingbourne, P. and Donaldson, A.F. and Ketema, J. and Qadeer, S.},



Download Download (PDF)   View View   Source Source   Source codes Source codes




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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: