Flow sensitive composition of thread modular abstract interpretation
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.
SIGSOFT FSE