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.