Scalable Automatic Verification of GPU Kernels

Until relatively recently the processing speed of computer systems increased at an exponential rate. Each year it was possible to use computers to solve computational problems that the previous year were out of reach. Around 2005, physical limits stopped this trend: it became infeasible to increase the clock rate of a processor without consuming an exorbitant amount of energy. To counter this, processor manufacturers have since aimed to provide increased performance by designing "multicore" processors, which consist of two or more processing units on a chip. Many computational tasks are parallelisable, in which case they can be distributed across the cores of a multicore processor.

Recently there has been a trend towards "many-core" processors, with hundreds or thousands of processing elements. For highly parallel applications, many-core processors can offer a massive speedup. The most readily available many-core processors are graphics processing units (GPUs) from companies such as NVIDIA, AMD, Intel, ARM and Imagination Technologies. GPUs were originally designed to accelerate graphical computations, but have become sufficiently general purpose for accelerating computational tasks in a variety of domains, including financial analysis, medical imaging, media processing and simulation.

GPUs are programmed by writing a "kernel" function, a program which will be executed by hundreds or thousands of threads running in parallel on the GPU. Parallel threads can communicate using shared memory, and synchronise using barrier statements. Writing correct GPU kernels is more challenging than writing sequential software due to two main problems: data races and barrier divergence. A data race occurs when two GPU threads access a shared memory location, at least one of the threads modifies this location, and no barrier statement separates the accesses. Data races almost always signify bugs in the kernel and lead to nondeterministic behaviour. Barrier divergence occurs when distinct threads reach different barrier statements in the kernel, and leads to deadlock.

Because GPUs are becoming widely used for general purpose software development, there is an urgent need for analysis techniques to help GPU programmers write correct code. Techniques to analyse GPU kernels with respect to data races and barrier divergence would significantly speed up the GPU software development process, leading to shorter time-to-market for GPU-accelerated applications.

In this project we plan to design formal techniques for verifying race- and divergence-freedom for GPU kernels. To be adopted and trusted by industrial practitioners our techniques must be highly automatic, scalable, and based on rigorous semantic foundations.

We plan to achieve these aims by developing a rigorous GPU memory model specification, and a formal semantics for GPU kernel execution that makes no assumptions about the structure of the kernel to be analysed. Based on these semantic foundations, we will design a verification technique that aims to prove absence of data races and barrier divergence by generating a "contract" for the kernel: a machine-checkable proof that kernel execution cannot lead to these defects. Contract-based verification is modular - each kernel procedure is analysed separately - and thus scalable. We will design a template-based contract generation method that captures domain-specific knowledge about common GPU programming idioms. This will allow efficient verification of GPU kernels that use typical data access patterns. For more intricate kernels that implement highly optimised algorithms, we will design a method based on Craig interpolation. This method will construct a proof of race- and divergence-freedom up to a bounded execution depth, and then attempt to extract a general contract from this proof.

Throughout, we will evaluate our methods using open source and industrial GPU kernels, including kernels provided by our industrial collaborators.

Full achievement of our proposed research objectives has the potential for wide industrial, economic, academic and societal impact.

Major GPU vendors including NVIDIA, AMD, ARM, Imagination Technologies and Intel support the OpenCL programming model which we target in our proposed research. Each vendor supplies an OpenCL distribution consisting of software development tools geared towards their specific devices. Our proposed approach aims for highly automatic and scalable verification techniques suitable for analysing OpenCL kernels, thus GPU vendor tools could be significantly enhanced with formal analysis components based on our novel research. As well as GPU vendors, our research has potential for high impact on companies specialising in software development tools, e.g. Codeplay Software: these companies could exploit the semantic foundations and verification algorithms we will publish, allowing them to build high value GPU kernel analysers. Because ARM, Imagination Technologies and Codeplay Software are all based in the UK, this industrial impact could lead to significant economic benefit nationally.

Our methods have the potential for impact on software developers who write code for GPUs. In particular, GPUs are widely used in the video games industry. Our advanced analysis techniques allow early identification of GPU kernel defects, which has the potential to speed up video game development, reducing time to market. This is significant economically: video games were highlighted in the last UK budget as a key area for economic growth.

To be successful, our research will require breakthroughs in formal semantics for concurrent programs, and in automatic techniques for contract generation. These are both active research areas nationally and internationally, so these breakthroughs will lead to new methods that can be exploited and extended by a large body of researchers. We elaborate more on this in the Academic Beneficiaries section.

GPU-accelerated software is becoming widely used by society: at one extreme GPUs are embedded in modern mobile phones, at the other, GPUs are being employed to accelerate algorithms in safety critical domains such as medical imaging. Society's increasing dependence on many-core accelerated software means that robustness of such software is essential. The techniques we propose here directly address robustness concerns: our methods will assist in the development of highly reliable GPU-accelerated software, and thus has the potential for significant societal impact.