Analyzing the communication topology of concurrent programs

Abstract

Concurrent languages present complex problems for program analysis. Existing analyses are either imprecise, exponential, or apply only to languages with statically-allocated processes and channels. We present a new polynomial-time analysis using abstract interpret ation that addresses the general problem of determining the communication topology of programs in a subset of Concurrent ML with arbitrary data structures, recursive higher-order functions, dynamic processor allocation, dynamic channel creation, and synchronous message-passing operations transmit and receive. The analysis addresses the following question: Whtch occurrences o~transmit can match whzch occurrences of receive? The notion of occurrence is formalized as a control path in a small-step semantics, which provides a powerful basis for distinguishing recursive communication topologies. The analysis is relational, in that it relates pairs of processes, and non-rmi~orm, in that it distinguishes between iterations in an infinite recursive communication pattern. The results are thus precise enough to aid processor allocation, scheduling, and sequentialization on both uniprocessors and multiprocessors.