Correct Optimized GPU Programs

Mohsen Safari

Research output: ThesisPhD Thesis - Research UT, graduation UT

79 Downloads (Pure)


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.
Original languageEnglish
QualificationDoctor of Philosophy
Awarding Institution
  • University of Twente
  • Huisman, Marieke, Supervisor
Award date6 Jul 2022
Place of PublicationEnschede
Print ISBNs978-90-365-5342-1
Publication statusPublished - 5 Apr 2022


Dive into the research topics of 'Correct Optimized GPU Programs'. Together they form a unique fingerprint.

Cite this