一句话：提出弱偏序 WPO 与确定性并行不动点算法，并通过 Pikos 在抽象解释中获得显著加速。
抽象解释将静态程序分析归约为逼近方程组的最小不动点计算，现有主流方法采用基于弱拓扑序（WTO）的顺序算法。本文提出弱偏序（WPO）概念，旨在实现确定性的并行不动点计算，并给出几乎线性时间的 WPO 构造算法。作者实现了 Pikos——顺序抽象解释器 IKOS 的确定性并行扩展。在 1017 个 C 程序上的评估表明：使用 4 核时相对 IKOS 平均加速 2.06 倍、最高 3.63 倍；使用 16 核时最高加速 10.97 倍。这表明 WPO 能在保持确定性的同时有效提升抽象解释的并行可扩展性。
Abstract interpretation is a general framework for expressing static program analyses. It reduces the problem of extracting properties of a program to computing an approximation of the least fixpoint of a system of equations. The de facto approach for computing this approximation uses a sequential algorithm based on weak topological order (WTO). This paper presents a deterministic parallel algorithm for fixpoint computation by introducing the notion of weak partial order (WPO). We present an algorithm for constructing a WPO in almost-linear time. Finally, we describe Pikos, our deterministic parallel abstract interpreter, which extends the sequential abstract interpreter IKOS. We evaluate the performance and scalability of Pikos on a suite of 1017 C programs. When using 4 cores, Pikos achieves an average speedup of 2.06x over IKOS, with a maximum speedup of 3.63x. When using 16 cores, Pikos achieves a maximum speedup of 10.97x.
@article{paperbot546,
title = {Deterministic parallel fixpoint computation},
author = {Sung Kook Kim and Arnaud J. Venet and Aditya V. Thakur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371082}
}