Correct Optimized GPU Programs

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