一句话：提出首个适用于可归约 CFG 的 SPMD 均匀性抽象解释，精度与 LLVM 默认分析相当且带 Coq 机械化正确性证明。
向量化编译器依赖发散性分析判断变量在 SPMD 线程间是否均匀，以抑制分支发散并把计算延迟到标量单元。发散性是超属性，与非干扰和绑定时间密切相关。已有分析或牺牲精度，或为保证可靠性而严格限制程序语法结构。本文提出首个适用于可归约控制流图的均匀性抽象解释，其通用性足以覆盖可归约 CFG，同时比达到同等通用性的分析更精确。作者给出正确性证明，并大部分在 Coq 中机械化。实验表明，其编译时间与精度和 LLVM 默认发散性分析相当，而后者仅在更受限的 CFG 上可靠；与一个可靠且至少同等通用的最新非干扰分析相比，本分析更快且精度更高。
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.
@article{paperbot1166,
title = {An abstract interpretation for SPMD divergence on reducible control flow graphs},
author = {Julian Rosemann and Simon Moll and Sebastian Hack},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434312}
}