Deterministic Parallel Fixpoint Computation

Kim, Sung Kook and Venet, Arnaud J. and Thakur, Aditya V.
Proc. ACM Program. Lang. (POPL) , 2020

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.

PDF     ACM©    

@article{POPL2020,
  author = {Kim, Sung Kook and Venet, Arnaud J. and Thakur, Aditya V.},
  title = {Deterministic Parallel Fixpoint Computation},
  journal = {Proc. ACM Program. Lang.},
  volume = {4},
  number = {POPL},
  year = {2020},
  month = jan,
  pages = {14:1--14:33},
  articleno = {14},
  numpages = {33},
  publisher = {ACM},
  doi = {10.1145/3371082}
}