Flow-Sensitive Composition of Thread-Modular Abstract Interpretation

TL;DR

This paper introduces a flow-sensitive, constraint-based static analysis method for concurrent programs that improves accuracy over flow-insensitive approaches by efficiently modeling inter-thread data flow causality.

Contribution

It presents a novel compositional and flow-sensitive analysis framework using lightweight constraints and a Datalog engine, enhancing precision and scalability in thread-modular abstract interpretation.

Findings

More accurate than existing flow-insensitive analyzers

Scalable and efficient with off-the-shelf Datalog engine

Effective on large benchmark suite

Abstract

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.