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 (Corresponderende auteur)
, Mohsen Safari
, Marieke Huisman
, Anton Wijs

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

8 Citaten (Scopus)

7 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Titel	Tools and Algorithms for the Construction and Analysis of Systems
Subtitel	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
Redacteuren	Dana Fisman, Grigore Rosu
Plaats van productie	Cham
Uitgeverij	Springer
Pagina's	332-352
Aantal pagina's	21
ISBN van elektronische versie	978-3-030-99527-0
ISBN van geprinte versie	978-3-030-99526-3
DOI's	https://doi.org/10.1007/978-3-030-99527-0_18
Status	Gepubliceerd - 30 mrt. 2022
Evenement	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, Duitsland Duur: 2 apr. 2022 → 7 apr. 2022

Publicatie series

Naam	Lecture Notes in Computer Science (LNCS)
Volume	13244
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Congres

Congres	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
Land/Regio	Duitsland
Stad	Munich
Periode	2/04/22 → 7/04/22

Financiering

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

Toegang tot document

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

pdfDefinitieve gepubliceerde versie, 550 KBLicentie: CC BY

Andere bestanden en links

Link naar publicatie in Scopus

Citeer dit

Şakar, Ö., Safari, M., Huisman, M., & Wijs, A. (2022). Alpinist: An Annotation-Aware GPU Program Optimizer. In D. Fisman, & G. Rosu (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 (blz. 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. redacteur / Dana Fisman ; Grigore Rosu. Cham : Springer, 2022. blz. 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 (reds.), 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, blz. 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, Duitsland, 2/04/22. https://doi.org/10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer. / Şakar, Ömer (Corresponderende auteur); 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. reds. / Dana Fisman; Grigore Rosu. Cham: Springer, 2022. blz. 332-352 (Lecture Notes in Computer Science (LNCS); Vol. 13244).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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, redacteurs, 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. blz. 332-352. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer

Samenvatting

Publicatie series

Congres

Financiering

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit