UTFacultiesBMSEventsPhD Defence Mohsen Safari | Correct Optimized GPU Programs

PhD Defence Mohsen Safari | Correct Optimized GPU Programs

Correct Optimized GPU Programs

The PhD defence of Mohsen Safari will take place (partly) online and can be followed by a live stream.

Mohsen Safari is a PhD student in the research group Formal Methods and Tools. Supervisor is prof.dr. M. Huisman from the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS).

This thesis contributes to the development of correct optimized GPU programs using deductive verification techniques. GPUs are many-core co-processors and their programming model enables programmers to develop massively parallel programs.

GPU programs are widely used in industry and, in particular, in High Performance Computing (HPC) environments. Even though we may achieve better performance by developing GPU programs (in contrast to sequential CPU programs), it may provide risks for program correctness. In the development of GPU programs, typically programmers first implement a naive implementation of an algorithm on a GPU. The goal of this naive version is to establish a base for potential optimizations, as it is easier to validate such an unoptimized program.

Then, they apply multiple GPU specific optimizations to efficiently benefit from the underlying resources. As a result, they implement a new version each time according to an optimization, with the goal of outperforming the previous versions. However, each new optimization might introduce non-trivial errors to the program.

Therefore, the goal of this thesis is to guarantee that the optimized versions of GPU programs remain correct during the development of GPU programs. This thesis leverages deductive verification techniques to prove data-race freedom and functional correctness of some complicated GPU programs. To show this, we use VerCors, which is a program verifier for concurrent programs based on permission based separation logic. The verification techniques and reasoning patterns that are discussed to verify different parallel algorithms can be beneficial to apply to other algorithms. Moreover, the thesis introduces a technique to automatically apply GPU optimizations to a verified program, and to guarantee that provability of correctness is preserved during such optimizations. As a result, this thesis shows how to develop correct optimized GPU programs.