Software model checking for GPGPUs
|
Supervisor |
|
|
Suitable for |
Abstract
Modern graphics processing units consists of hundreds of processing cores, potentially providing high performance for parallel applications. The scope of modern GPUs goes beyond graphics, leading to the term "general purpose GPUS" (GPGPUs). Open Compute Language (OpenCL) is a new programming language geared towards programming a system comprised of a host processor with several accelerator devices, such as GPGPUs. OpenCL aims to be portable yet low-level, allowing high-performance code to run on a range of devices. The language is being widely adopted by industry, with implementations available from Apple, NVIDIA, AMD and IBM. The low-level nature of OpenCL means that OpenCL programs are especially error-prone - there is potential for errors related to the movement of memory between distinct levels of the memory hierarchy; such errors are not relevant to software operating on shared-memory processors. There is an urgent need for automated verification techniques to analyse GPGPU software written in OpenCL. The project would involve extending the CBMC and SatAbs model checkers (created by Daniel Kroening, and maintained by the Formal Verification group at Oxford) to deal with the OpenCL language. Initially, this would involve modifications to the front-end of the model checkers, after which the tools could be evaluated on a range of example applications. After this, there would be scope for optimizing the model checkers to take advantage of domain-specific features of OpenCL and typical GPGPU software.Background needed: Strong programming skills, basic knowledge of model checking techniques.