2017/09/28 by Markus Kusano, Chao Wang, Kusano, Markus +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1709.10116
openalex publication_date 2017/09/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We propose a constraint-based flow-sensitive static analysis for concurrent programs by iteratively composing thread-modular abstract interpreters via the use of a system of lightweight constraints. Our method is compositional in that it first applies sequential abstract interpreters to individual threads and then composes their results. It is flow-sensitive in that the causality ordering of interferences (flow of data from global writes to reads) is modeled by a system of constraints. These interference constraints are lightweight since they only refer to the execution order of program statements as opposed to their numerical properties: they can be decided efficiently using an off-the-shelf Datalog engine. Our new method has the advantage of being more accurate than existing, flow-insensitive, static analyzers while remaining scalable and providing the expected soundness and termination guarantees even for programs with unbounded data. We implemented our method and evaluated it on a large number of benchmarks, demonstrating its effectiveness at increasing the accuracy of thread-modular abstract interpretation.