UniAna: Using Abstract Interpretation to Analyze the Uniformity of Variables

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.
This website accompanies our POPL'21 paper An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs. There are Coq proofs to establish the soundness of our uniformity analysis on GitHub and its documentation can be found here. The analysis is also implemented in LLVM.

Publication

Conferences

An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs - POPL 2021
Rosemann, J., Moll, S. and Hack, S.
Principles of Programming Languages, 2021. [url] [bib]

@conference{RSH:popl21,
   author = {Julian Rosemann and Simon Moll and Sebastian Hack},
   title = {An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs},
   year = 2021,
   month = january,
   url = {https://compilers.cs.uni-saarland.de/papers/uniana_preprint.pdf},
   booktitle = {Principles of Programming Languages},
   booktitle_short = {POPL},
 }

Compiler Design Lab

UniAna: Using Abstract Interpretation to Analyze the Uniformity of Variables

Publication

Conferences

People