Evaluation of the Ada-SPARK Language Effectiveness in Graphics Processing Units for Safety Critical Systems

Abstract

Modern safety critical systems require high levels of performance for the implementation of advanced functionalities, which are not possible with the simple conventional architectures currently used in them. Embedded General Purpose Graphics Processing Units (GPGPUs) are among the hardware technologies which can provide the high performance required in these domains. However, their massively parallel nature complicates the verification of their software and increases its cost because it usually involves code coverage through extensive human-driven testing. The Ada-SPARK language has traditionally been used in highly-critical environments for its formal verification capabilities and powerful type system. The use of such tools, especially those being backed up by theorem provers, has significantly lowered the amount of effort needed to validate functionality of safety-critical systems. In this work, we utilize AdaCore's CUDA backend for Ada ---currently in closed beta--- in conjunction with the SPARK language subset to assess the state of static verification for GPU kernels. We show how common programming mistakes in GPU kernels can be prevented, formulate a pattern for buffer overflow detection, and close with a few GPU case studies.