Verifying Data Parallel Programs Using Sequential Program Verification Technology

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. I will then briefly discuss our current thoughts about how the idea of using sequential verification technology to verify data parallel programs might be extended to other programming models, in particular OpenMP. For an introduction to GPUVerify check out this video: http://www.youtube.com/watch?v=l8ysBPV8OvA

Speaker Details

Alastair Donaldson is a Lecturer (Assistant Professor) 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.

Series:
Microsoft Research Talks
Date:
Speakers:
Alastair Donaldson
Affiliation:
Department of Computing

Series: Microsoft Research Talks