Imperial College London
Portrait Picture

ProfessorAlastairDonaldson

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

+44 (0)20 7594 8266alastair.donaldson Website

 
 
//

Location

 

422Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Betts:2015:10.1145/2743017,
author = {Betts, A and Chong, N and Donaldson, AF and Ketema, J and Qadeer, S and Thomson, P and Wickerson, J},
doi = {10.1145/2743017},
journal = {ACM Transactions on Programming Languages and Systems},
pages = {1--49},
title = {The design and implementation of a verification technique for GPU Kernels},
url = {http://dx.doi.org/10.1145/2743017},
volume = {37},
year = {2015}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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 <i>synchronous, delayed visibility (SDV)</i> 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.
AU  - Betts,A
AU  - Chong,N
AU  - Donaldson,AF
AU  - Ketema,J
AU  - Qadeer,S
AU  - Thomson,P
AU  - Wickerson,J
DO  - 10.1145/2743017
EP  - 49
PY  - 2015///
SN  - 1558-4593
SP  - 1
TI  - The design and implementation of a verification technique for GPU Kernels
T2  - ACM Transactions on Programming Languages and Systems
UR  - http://dx.doi.org/10.1145/2743017
UR  - https://dl.acm.org/doi/10.1145/2743017
UR  - http://hdl.handle.net/10044/1/32067
VL  - 37
ER  -
Download