TACAS-artifact-submission-109.zip (192.45 MB)
Download file

Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer)

Download (192.45 MB)
posted on 26.11.2021, 07:15 by Ömer ŞakarÖmer Şakar, Mohsen SafariMohsen Safari, Marieke HuismanMarieke Huisman, Anton WijsAnton 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.


ChEOPS (NWO TTW grant 17249)

Mercedes: Maximal Reliability of Concurrent and Distributed Software

Netherlands Organisation for Scientific Research

Find out more...





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

Usage metrics