Graphics Processing Units (GPUs) are increasingly considered for use in safety-critical systems, thanks to their high performance capabilities, to satisfy the increasing data processing needs of next generation systems. However, software development for massively parallel GPUs is more challenging than sequential CPU code. GPUs have a different address space than CPUs, and it is the programmer’s responsibility to manage explicit memory allocations and transfers through low-level, error prone operations using pointers. Moreover, parallel programming can lead to data races. These issues can challenge the certification of GPU software.

Formal methods such as the ones provided by Ada SPARK have been used for long time in CPU code to prevent programming mistakes and prove the absence of runtime errors. In this presentation, I will describe our experience at BSC using AdaCore's GNAT for CUDA toolchain which is currently in closed beta, in the context of the European Space Agency (ESA)-funded project "Formal Methods for GPU Software Development and Verification". The tool allows the development of Safety Critical GPU code for NVIDIA GPUs in Ada and SPARK instead of CUDA. We show how Ada SPARK can prevent common GPU programming mistakes and can prove the absence of runtime errors such as numeric overflows or underflows, division by 0 as well as buffer overflows due to the pointer usage. We studied the strengths and limitations of the current version of the tools, as well as how the programmer can guide the tools to maximise their detection capabilities.

A major contribution of our work is the development of a programming methodology that conveys information from the host to the GPU code and vice versa, so that the prover has enough information to check the consistency between these two software parts. We demonstrate our methodology by porting the open source GPU4S Bench (GPU for space) benchmarking suite [1][2][3] to Ada SPARK [4], achieving up to silver SPARK adoption level, while showing that gold is also possible. Notably, just porting to SPARK (stone level), was enough to eliminate two software defects detected later in the C/CUDA version of a benchmark. All our project developments are released as open-source, serving as a demonstrator of the tool capabilities and as learning resources for future developments. Despite the fact that the AdaCore GPU compiler is still under development and some GPU features are not yet available, our work demonstrates that Ada SPARK is a viable method to prove the correctness of GPU software for high assurance systems.

[1] I. Rodriguez et al, GPU4S Bench: Design and Implementation of an Open GPU Benchmarking Suite for Space On-board Processing, UPC Technical Report 2019

[2] D. Steenari et al, OBPMark and GPU4S Bench repository, https://obpmark.github.io

[3] D. Steenari el .al, OBPMark (On-Board Processing Benchmarks) - Open Source Computational Performance Benchmarks for Space Applications, 2nd European Workshop on On-Board Data Processing (OBDP) 2021

[4] D. Aspetakis, GPU4S Bench Ada SPARK, https://gitlab.bsc.es/dimitris...

Download Slides