high performance computing on graphics processing units: hgpu.org

A heterogeneous computing system is a system composed of different types of computing units. SYCL is a software development framework with which programs can be developed for such systems. It uses the concept of kernels, where a kernel executes code inside it in parallel, and different kernels can be executed concurrently on multiple computing units. These concurrent executions of kernels and their contents means that the set of possible program behaviours can be of considerable size, which makes it easy for developers to overlook problems which only occur in a few possible program behaviours. To solve this, formal verification can be performed to ensure a program’s correctness. However, at the time of writing, there do not seem to exist any formal verification tools for SYCL programs. The VerCors toolset, which enables users perform deductive verification on programs, supports reasoning about parallel and concurrent constructs. This makes VerCors suitable for verification of programs written for heterogeneous systems. Moreover, it aims to be language-independent, such that support for new languages can be added without redesigning the entire toolset. In this thesis, it is investigated how the VerCors toolset could be extended to enable users to formally verify a subset of programs written in SYCL. This subset consists of programs that can contain two kinds of kernel definitions, data sharing between devices and the host, and declarations of data in the various address spaces of computing units. For each feature in this subset, this thesis describes its semantics and discusses in detail how these semantics are encoded into VerCors, and what considerations had to be made to facilitate the construction and soundness of these encodings. Finally, the efforts taken to ensure the soundness of the encoding and the usefulness of the supported SYCL subset are discussed.