Toward a Theory of Maximally Concurrent Programs


To appear at Nineteenth Annual ACM SIGACT-SIGOPS Symposium on PRINCIPLES OF DISTRIBUTED COMPUTING (PODC 2000), Portland, Oregon, 16-19 July 2000


Typically, program design involves constructing a program, P, that implements a given specification, S, that is, the set of executions of P is a subset of the set of executions satisfying S. In many cases, we seek a P that not only implements S but for which the set of executions of P and S are identical. Then, every execution satisfying the specification is a possible execution of the program; we call P maximal for the specification S. We argue in this paper that traditional specifications of concurrent programs are incomplete without some maximality requirement because they can often be implemented in a sequential fashion. Additionally, a maximal solution can be refined to a variety of programs each appropriate for execution on a different computing platform. We suggest a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for many non-trivial examples. The method may also serve as a guide in constructing maximal programs.