Formal Analysis Techniques for GPU Kernels (FAT-GPU) is a half-day tutorial on recent developments in the area of improving the reliability of GPU kernels. The focus will be the GPUVerify tool, developed at Imperial College London as part of the CARP EU project. The tutorial will cover how GPUVerify can be used for bug detection, proving absence of defects, and checking portability of GPU kernel code written in OpenCL and CUDA.
The tutorial will be practical, aimed at researchers and practitioners in the parallel programming community who have a reasonable background in GPU programming. The tutorial will not assume a background in formal verification or theoretical computer science.
This YouTube video on GPUVerify gives a flavour of the style of the tutorial (though the presenters at the tutorial are different, and will give their own take on the topic):
Schedule (on 21 January):
- 10:00-10:30 Brief overview of GPU programming, data races and barrier divergence
- 10:30-11:00 Demo of GPUVerify, showing how it can be used to analyse a variety of kernels, and illustrating the tool's strengths and weaknesses
- 11:00-11:30 Break
- 11:30-12:00 Details of the GPUVerify tool chain
- 12:00-12:30 Overview of the GPUVerify verification method, focussing on scalability to large numbers of threads
- 12:30-13:00 Showcase of ongoing work on the project, including formalisation of the OpenCL 2.0 memory model
Presenter: John Wickerson
John is a postdoctoral research associate working on how to reason rigorously about GPU programs. He is specifically interested in formalising the memory model defined by the OpenCL standard. In previous research, he has developed a diagrammatic proof system for separation logic, and has investigated the application of the rely/guarantee method to the verification of sequential modules.