State space reduction in abstract interpretation of parallel programs

Traditional compiler techniques operating on control flow graphs are not adequate for analyzing parallel programs where data can flow from one node to another through the shared memory, even though the nodes are not related by control flow edges. Abstract interpretation provides a general and unified framework for program analyses, and can be applied to parallel programs without much difficulty. However, the state space explosion problem in abstract interpretation of parallel programs must be relieved in order to make compile-time analyses practical. Although abstract interpretation itself provides an excellent mechanism for state space reduction by state abstraction, lower precision analysis often results from taking a higher degree of abstraction. In this paper, we present state space reduction that preserves analysis precision by eliminating redundant interleavings, based on Valmari´s (1990) stubborn set method. We also propose an iterative algorithm for analyzing programs with pointers and closures, in which knowledge about shared locations required by existing methods is not available. The proposed algorithm has been implemented, and we discuss preliminary results of the implementation