Şakar, Ömer; Safari, Mohsen; Huisman, Marieke; Wijs, Anton (2021): Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer). Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/16938556.v1

Software

x choose version: version 2 - 2021-11-26 (latest)

• Computer Software

Annotation-aware, Deductive verification, GPU, Optimization, Program transformation

Apache-2.0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Ömer Şakar , Mohsen Safari , Marieke Huisman , Anton Wijs

Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer) submitted to TACAS '22 conference. For a full description on how to use the artifact, please see the README.txt file. The artifact contains the Alpinist tool, all its dependencies and documentation for the VerCors tool.

Abstract of the paper:
GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone.
This paper 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.

• 2021-11-22 first online, published, posted

4TU.ResearchData

• ChEOPS (NWO TTW grant 17249)
• Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science
Eindhoven University of Technology, Department of Mathematics and Computer Science