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 interpretation 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 transmitand receive. The analysis addresses the following question: Which occurrences of transmit can match which 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-uniform, in that it distinguishes between iterations in an i...