8122

GPUVerify: A Verifier for GPU Kernels

Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, Paul Thomson
Department of Computing, Imperial College London, UK
27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’12), 2012

@inproceedings{BettsCDQT_OOPSLA2012,

   title={GPUVerify}: a Verifier for {GPU} Kernels},

   author={Adam Betts and Nathan Chong and Alastair F. Donaldson and Shaz Qadeer and Paul Thomson},

   booktitle={Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’12)},

   publisher={ACM},

   year={2012}

}

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

Package:

1474

views

We present a technique for verifying race- and divergencefreedom of GPU kernels that are written in mainstream kernel programming languages such as OpenCL and CUDA. Our approach is founded on a novel formal operational semantics for GPU programming termed synchronous, delayed visibility (SDV) semantics. The SDV semantics provides a precise definition of barrier divergence in GPU kernels and allows kernel verification to be reduced to analysis of a sequential program, thereby completely avoiding the need to reason about thread interleavings, and allowing existing modular techniques for program verification to be leveraged. We describe an efficient encoding for data race detection and propose a method for automatically inferring loop invariants required for verification. We have implemented these techniques as a practical verification tool, GPUVerify, which can be applied directly to OpenCL and CUDA source code. We evaluate GPUVerify with respect to a set of 163 kernels drawn from public and commercial sources. Our evaluation demonstrates that GPUVerify is capable of efficient, automatic verification of a large number of real-world kernels.
Rating: 2.3. From 2 votes.
Please wait...

* * *

* * *

HGPU group © 2010-2017 hgpu.org

All rights belong to the respective authors

Contact us: