# Deterministic Parallel Fixpoint Computation

arXiv: https://arxiv.org/abs/1909.05951 · HTML: https://mlsanity.com/paper/1909.05951/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Sep 2019.

## Built on by (most cited first, 1 of 1)

- [A Variant of Concurrent Constraint Programming on GPU](https://mlsanity.com/paper/2207.12116/) (2022)

## Abstract (arXiv)

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.