Title: Flow-Sensitive Composition of Thread-Modular Abstract Interpretation,
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.