Formal methods for GPU Software Development and Verification using Ada SPARK: Experiences from Applications in Aerospace

Dr Leonidas Kosmidis

Senior Researcher, Barcelona Supercomputing Center (BSC)


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...

About Dr Leonidas Kosmidis

Dr. Leonidas Kosmidis is a Senior Researcher at the Barcelona Supercomputing Center (BSC) and Faculty Member at the Universitat Politècnica de Catalunya (UPC). He is leading the research on embedded GPUs and accelerators for safety critical systems, both at hardware and system software level within the CAOS (Computer Architecture/Operating Systems) group at BSC.
Dr. Kosmidis is the recipient of the RISC-V Educator of the Year Award in 2019 from the RISC-V Foundation and an Honourable Mention for the EuroSyS Roger Needham PhD Award in 2018, which is awarded to the best PhD thesis in Europe in the area of Systems. He is the Principal Investigator of several projects funded by the European Space Agency (ESA) such as the GPU4S (GPU for Space), "Formal Methods for GPUs", and the Horizon Europe METASAT project funded by the European Commission, as well as projects funded by industry such as the Airbus Defence and Space, which focus on the adoption of GPUs in space and avionics systems, including their certification. He is also participating in several standardisation efforts regarding GPU programming in safety critical systems within Khronos, in Vulkan SC and SYCL SC, as well as an external expert for the revision of the ECSS standards ECSS-E-ST-20-40 and ECSS-Q-ST-60-02C on ASIC, FPGA and IP Core developments.

Sponsored by

Official Media Partners

Supported by