Deterministic Parallel Fixpoint Computation

TL;DR

This paper introduces a deterministic parallel fixpoint computation algorithm using weak partial order, significantly improving the scalability and speed of static program analysis with abstract interpretation.

Contribution

It presents a novel parallel algorithm for fixpoint computation based on weak partial order, extending the IKOS abstract interpreter with demonstrated performance gains.

Findings

PIKOS achieves up to 10.97x speedup on 16 cores.

The algorithm constructs weak partial orders in almost-linear time.

Parallel analysis scales well on large program suite.

Abstract

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.