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.