确定性并行不动点计算
Deterministic Parallel Fixpoint Computation
摘要：
抽象解释是表示静态程序分析的一般框架。它减少了提取程序属性的问题，计算方程组的最小不动点的近似。计算该近似值的实际方法使用基于弱拓扑序（WTO）的顺序算法。通过引入弱偏序的概念，提出了一种确定性的不动点并行算法。我们提出了一个算法，用于构建一个WPO在几乎线性的时间。最后，我们描述了PIKOS，我们的确定性并行抽象解释器，它扩展了顺序抽象解释器IKOS。我们评估的性能和可扩展性的PIKOS上的一套1017 C程序。当使用4个核心时，PIKOS实现了IKOS的2.06倍的平均加速比，最大加速比为3.63倍。当使用16核时，PIKOS实现了10.97倍的最大加速比。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
