Paper Info
Title
GPUVerify: a verifier for GPU kernels
Abstract
We present a technique for verifying race- and divergence-freedom 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.
Year
DOI
Venue
2012
10.1145/2384616.2384625
OOPSLA
Keywords
Field
DocType
automatic verification,gpu kernel,sdv semantics,kernel verification,cuda source code,data race detection,program verification,gpu programming,practical verification tool,novel formal operational semantics,verification,concurrency
Kernel (linear algebra),Operational semantics,Programming language,Source code,Concurrency,Computer science,CUDA,Parallel computing,Code generation,Theoretical computer science,Loop invariant,General-purpose computing on graphics processing units
Conference
Volume
Issue
ISSN
47
10
0362-1340
Citations 
PageRank 
References 
51
1.80
19
Authors
5
Name
Order
Citations
PageRank
Adam Betts125113.81
Nathan Chong21857.91
Alastair Donaldson31485.79
Shaz Qadeer43257239.11
Paul Thomson51225.85