Skip to main content

GPUVerify: a technique for formal verification of GPU kernels

Alastair Donaldson ( Imperial College London )

I will report on recent work in the Multicore Programming Group at Imperial on the verification of data parallel programs. The principal focus of the talk will be on GPUVerify, a verification technique and tool for GPU kernels written in OpenCL and CUDA. This project started when I was a Visiting Researcher at MSR during 2011, and has evolved into a now fairly usable tool which we are pushing to GPU programmers. GPUVerify achieves scalability by transforming a massively parallel GPU kernel into a sequential program that can be checked using existing theorem-proving based tools such as Microsoft's Boogie. I will describe how this transformation works, discuss practical issues associated with building a tool chain that can operate directly on OpenCL and CUDA source code, and describe recent developments related to improving the efficiency of invariant inference. For an introduction to GPUVerify see:



Speaker bio

Alastair Donaldson is a Lecturer in the Department of Computing at Imperial College London. His research interests include automated techniques for analysing concurrent software, with the aim of improving software reliability, and programming models for multi- and many-core architectures that aid in productive development of efficient software. He is the Scientific Coordinator of CARP: Correct and Efficient Accelerator Programming, an FP7 project involving many key European players in the field of accelerated computing, and is the main designer of GPUVerify, a verification technique and tool for automatic analysis of GPU kernels written in OpenCL and CUDA. In addition, his research group is supported by EPSRC, and by industrial funding from ARM and Intel. Before joining Imperial, Donaldson was (in reverse chronological order) a Visiting Researcher at Microsoft Research, Redmond, USA, an EPSRC Postdoctoral Research Fellow at the University of Oxford, and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow.



Share this: