Prof. Marieke Huisman (University of Twente, the Netherlands)
VerCors and Alpinist: correctness of GPU applications throughout the development cycle
GPU programs are widely used in industry. They make use of special hardware, supporting massive parallelism. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. The VerCors program verifier, a verifier for concurrent software, has been tailored to reason about such GPU programs, and in this talk I will explain how this is done, and discuss various GPU case studies that have been verified with VerCors.
However, to obtain the best performance, a typical development process of a GPU application involves the manual or semi-automatic application of optimizations prior to compiling the code. Keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. Therefore, this talk also introduces Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.