13806

The Design and Implementation of a Verification Technique for GPU Kernels

Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, John Wickerson
Imperial College London
Programming Languages and Systems (TOPLAS), 2015

@article{betts2015design,

   title={The Design and Implementation of a Verification Technique for GPU Kernels},

   author={BETTS, ADAM and CHONG, NATHAN and DONALDSON, ALASTAIR F and KETEMA, JEROEN and QADEER, SHAZ and THOMSON, PAUL and WICKERSON, JOHN},

   year={2015}

}

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

Package:

970

views

We present a technique for the formal verification of GPU kernels, addressing two classes of correctness properties: data races and barrier divergence. Our approach is founded on a novel formal operational semantics for GPU kernels termed synchronous, delayed visibility (SDV) semantics, which captures the execution of a GPU kernel by multiple groups of threads. The SDV semantics provides operational definitions for barrier divergence and for both inter- and intra-group data races. We build on the semantics to develop a method for reducing the task of verifying a massively parallel GPU kernel to that of verifying a sequential program. This completely avoids the need to reason about thread interleavings, and allows existing techniques for sequential program verification to be leveraged. We describe an efficient encoding of data race detection and propose a method for automatically inferring the loop invariants that are required for verification. We have implemented these techniques as a practical verification tool, GPUVerify, that can be applied directly to OpenCL and CUDA source code. We evaluate GPUVerify with respect to a set of 162 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.
VN:F [1.9.22_1171]
Rating: 5.0/5 (1 vote cast)
The Design and Implementation of a Verification Technique for GPU Kernels, 5.0 out of 5 based on 1 rating

* * *

* * *

HGPU group © 2010-2017 hgpu.org

All rights belong to the respective authors

Contact us: