WG211/M15Donaldson

Title: Translation Validation for Data Race-Freedom of OpenCL Code Generated by a Parallelising Compiler

Alastair Donaldson, leader of Imperial's Multicore Programming Group ([1])

Abstract:

The CARP EU project led to the development of GPUVerify, a static verification tool that is capable of providing data race-freedom of OpenCL and CUDA computational kernels. To deal with programs that contain loops, GPUVerify must either be provided with loop invariants by the user, or must try to guess loop invariants. In both cases, verification is sound: provided or guessed loop invariants are not trusted; their truth is checked automatically as part of the verification process.

CARP also led to a new high-level language, PENCIL, that allows accelerator programs to be written in a cleaned-up dialect of C, restricted to enable aggressive auto-parallelising compilation in the polyhedral model. The CARP team at ENS/INRIA designed a PENCIL->OpenCL compiler, and the Imperial team were keen to try verifying race-freedom of the generated code using GPUVerify. However, code generated by polyhedral compilers typically contains deep loop nests, and automatically inferring suitable invariants for these loop nests proved challenging.

We managed to manually figure out required invariants for some example generated kernels, and explained the form of these invariants to the ENS/INRIA compiler team. The compiler team realised that the compiler, internally, has all the requisite information necessary to generate these sorts of invariants. We have thus investigated a setup where, from a PENCIL program, the PENCIL->OpenCL compiler generates optimized OpenCL code, together with invariants characterising the argument that the code is data race-free. GPUVerify does not trust this "certificate" of race-freedom: it checks whether the invariants really do hold, and if they do, it uses them to try to prove race-freedom of the generated code.

Using this setup we have been able to verify race-freedom of a large set of kernels generated from the Polybench suite, and in the process we found two bugs in the compiler that meant that generated code could exhibit data races.

In the talk, I will provide an overview of this work, running some demos to show the process in action.