Alpinist: An Annotation-Aware GPU Program Optimizer

Ömer Şakar; Mohsen Safari; Marieke Huisman; Anton Wijs

doi:10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer

Ömer Şakar (Corresponding author)
, Mohsen Safari
, Marieke Huisman
, Anton Wijs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

8 Citations (Scopus)

2 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II
Editors	Dana Fisman, Grigore Rosu
Place of Publication	Cham
Publisher	Springer
Pages	332-352
Number of pages	21
ISBN (Electronic)	978-3-030-99527-0
ISBN (Print)	978-3-030-99526-3
DOIs	https://doi.org/10.1007/978-3-030-99527-0_18
Publication status	Published - 30 Mar 2022
Event	28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022 - Munich, Germany Duration: 2 Apr 2022 → 7 Apr 2022

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	13244
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022
Country/Territory	Germany
City	Munich
Period	2/04/22 → 7/04/22

Funding

★ This work is supported by NWO grant 639.023.710 for the Mercedes project and by NWO TTW grant 17249 for the ChEOPS project

Keywords

Annotation-aware
Deductive verification
GPU
Optimization
Program transformation

Access to Document

10.1007/978-3-030-99527-0_18

pdfFinal published version, 550 KBLicence: CC BY

Cite this

Şakar, Ö., Safari, M., Huisman, M., & Wijs, A. (2022). Alpinist: An Annotation-Aware GPU Program Optimizer. In D. Fisman, & G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II (pp. 332-352). (Lecture Notes in Computer Science (LNCS); Vol. 13244). Springer. https://doi.org/10.1007/978-3-030-99527-0_18

Şakar, Ömer ; Safari, Mohsen ; Huisman, Marieke et al. / Alpinist : An Annotation-Aware GPU Program Optimizer. Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. editor / Dana Fisman ; Grigore Rosu. Cham : Springer, 2022. pp. 332-352 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{9ac597c60f144b4c960f31596ee1f021,

title = "Alpinist: An Annotation-Aware GPU Program Optimizer",

abstract = "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.",

keywords = "Annotation-aware, Deductive verification, GPU, Optimization, Program transformation",

author = "{\"O}mer {\c S}akar and Mohsen Safari and Marieke Huisman and Anton Wijs",

year = "2022",

month = mar,

day = "30",

doi = "10.1007/978-3-030-99527-0\_18",

language = "English",

isbn = "978-3-030-99526-3",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "332--352",

editor = "Dana Fisman and Grigore Rosu",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022 ; Conference date: 02-04-2022 Through 07-04-2022",

}

Şakar, Ö, Safari, M, Huisman, M & Wijs, A 2022, Alpinist: An Annotation-Aware GPU Program Optimizer. in D Fisman & G Rosu (eds), Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. Lecture Notes in Computer Science (LNCS), vol. 13244, Springer, Cham, pp. 332-352, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, 2/04/22. https://doi.org/10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer. / Şakar, Ömer (Corresponding author); Safari, Mohsen; Huisman, Marieke et al.
Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. ed. / Dana Fisman; Grigore Rosu. Cham: Springer, 2022. p. 332-352 (Lecture Notes in Computer Science (LNCS); Vol. 13244).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Alpinist

T2 - 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022

AU - Şakar, Ömer

AU - Safari, Mohsen

AU - Huisman, Marieke

AU - Wijs, Anton

PY - 2022/3/30

Y1 - 2022/3/30

N2 - 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.

AB - 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.

KW - Annotation-aware

KW - Deductive verification

KW - GPU

KW - Optimization

KW - Program transformation

UR - https://www.scopus.com/pages/publications/85128715847

U2 - 10.1007/978-3-030-99527-0_18

DO - 10.1007/978-3-030-99527-0_18

M3 - Conference contribution

AN - SCOPUS:85128715847

SN - 978-3-030-99526-3

T3 - Lecture Notes in Computer Science (LNCS)

SP - 332

EP - 352

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Fisman, Dana

A2 - Rosu, Grigore

PB - Springer

CY - Cham

Y2 - 2 April 2022 through 7 April 2022

ER -

Şakar Ö, Safari M, Huisman M, Wijs A. Alpinist: An Annotation-Aware GPU Program Optimizer. In Fisman D, Rosu G, editors, Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. Cham: Springer. 2022. p. 332-352. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this