cff-version: 1.2.0
abstract: "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. "
authors:
- family-names: Şakar
given-names: Ömer
orcid: "https://orcid.org/0000-0003-3457-5446"
- family-names: Safari
given-names: Mohsen
- family-names: Huisman
given-names: Marieke
orcid: "https://orcid.org/0000-0003-4467-072X"
- family-names: Wijs
given-names: Anton
title: "Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer)"
keywords:
version: 2
identifiers:
- type: doi
value: 10.4121/16938556.v2
license: Apache-2.0
date-released: 2021-11-26