Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-38176
Titel: | An abstract interpretation for SPMD divergence on reducible control flow graphs |
VerfasserIn: | Rosemann, Julian Moll, Simon Hack, Sebastian |
Sprache: | Englisch |
Titel: | Proceedings of the ACM on Programming Languages |
Bandnummer: | 5 |
Heft: | POPL |
Seiten: | 1-31 |
Verlag/Plattform: | Association for Computing Machinery |
Erscheinungsjahr: | 2021 |
Freie Schlagwörter: | Divergence Analysis Vectorization Binding Time Hyper-Property Dependence Non-Interference Abstract Interpretation |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Konferenzbeitrag (in einem Konferenzband / InProceedings erschienener Beitrag) |
Abstract: | Vectorizing compilers employ divergence analysis to detect at which program point a specific variable is uniform, i.e. has the same value on all SPMD threads that execute this program point. They exploit uniformity to retain branching to counter branch divergence and defer computations to scalar processor units. Divergence is a hyper-property and is closely related to non-interference and binding time. There exist several divergence, binding time, and non-interference analyses already but they either sacrifice precision or make significant restrictions to the syntactical structure of the program in order to achieve soundness. In this paper, we present the first abstract interpretation for uniformity that is general enough to be applicable to reducible CFGs and, at the same time, more precise than other analyses that achieve at least the same generality. Our analysis comes with a correctness proof that is to a large part mechanized in Coq. Our experimental evaluation shows that the compile time and the precision of our analysis is on par with LLVM’s default divergence analysis that is only sound on more restricted CFGs. At the same time, our analysis is faster and achieves better precision than a state-of-the-art non-interference analysis that is sound and at least as general as our analysis. |
DOI der Erstveröffentlichung: | 10.1145/3434312 |
URL der Erstveröffentlichung: | https://dl.acm.org/doi/10.1145/3434312 |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-381760 hdl:20.500.11880/34467 http://dx.doi.org/10.22028/D291-38176 |
ISSN: | 2475-1421 |
Datum des Eintrags: | 23-Nov-2022 |
Bezeichnung des in Beziehung stehenden Objekts: | Supplemental Material |
In Beziehung stehendes Objekt: | https://dl.acm.org/action/downloadSupplement?doi=10.1145%2F3434312&file=popl21main-p206-p-archive.zip |
Bemerkung/Hinweis: | Proceedings of the ACM on Programming Languages 2021, 5(POPL), 31 |
Fakultät: | MI - Fakultät für Mathematik und Informatik |
Fachrichtung: | MI - Informatik |
Professur: | MI - Prof. Dr. Sebastian Hack |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
3434312.pdf | 369,99 kB | Adobe PDF | Öffnen/Anzeigen |
Diese Ressource wurde unter folgender Copyright-Bestimmung veröffentlicht: Lizenz von Creative Commons