Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs (2008)

Dataflow analysis for concurrent programs is a problem of critical importance but, unfortunately, also an undecidable one. A key obstacle is to determine precisely how dataflow facts at a location in a given thread could be affected by operations of other threads.This problem, in turn, boils down to pairwise reachability, i.e., given program locations c <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> and c <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> in two threads T <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> and T <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> , respectively, determining whether c1 and c2 are simultaneously reachable in the presence of constraints imposed by synchronization primitives. Unfortunately, pairwise reachability is undecidable for most synchronization primitives. However, we leverage the surprising result that the closely related problem of parameterized pairwise reachability of c <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> and c <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> , i.e., whether for some n <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> and n <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> , c <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> and c <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> are simultaneously reachable in the program T <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> n <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1||</sub> T <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> n <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> comprised of n <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> copies of T <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sub> and n <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> copies of T <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sub> ,is not only decidable for many primitives, but efficiently so. Although parameterization makes pairwise reachability tractable it may over-approximate the set of pairwise reachable locations and can, therefore, be looked upon as an abstraction technique.Where as abstract interpretation is used for control and data abstractions, we propose the use of parameterization as an abstraction for concurrency. Leveraging abstract interpretation in conjunction with parameterization allows us to lift two desirable properties of sequential dataflow analysis to the concurrent domain, i.e., precision and scalability.