Deterministic Parallel Fixpoint Computation

September 12, 2019 · Entered Twilight · 🏛 Proc. ACM Program. Lang.

"Last commit was 5.0 years ago (≥5 year threshold)"

Evidence collected by the PWNC Scanner

Repo contents: CHANGES.md, Dockerfile, LICENSE.pdf, README.md, aws, benchmarks, extract_benchmarks.sh, generate_fig5.py, generate_fig6.py, generate_fig7.py, generate_fig8.py, generate_tab2.py, generate_tab3.py, install.sh, install_dependencies.sh, install_python_dependencies.sh, measure_speedup.sh, measure_tab3-aureport.sh, pikos, reproduce_all-8.sh, reproduce_rq1-4.sh, reproduce_tab2-4.sh, reproduce_tab2a-4.sh, reproduce_tab3-16.sh, results-paper, run_benchexec.sh, run_ikos.sh, run_pikos.sh, test1-4.sh, test2-16.sh, tools, update_speedup.py, xml

Authors Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur arXiv ID 1909.05951 Category cs.PL: Programming Languages Citations 10 Venue Proc. ACM Program. Lang. Repository https://github.com/95616ARG/pikos_popl2020 ⭐ 16 Last Checked 1 month ago

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.