Maximally Concurrent Programs
Rajeev Joshi, Jayadev Misra · Formal Aspects of Computing · 2000
Abstract. Typically, program design involves constructing a program P that implements a given specification S ; that is, the set ${\overline P}$ of executions of P is a subset of the set ${\overline S}$ of executions satisfying S . In many cases, we seek a program P that not only implements S , but for which ${\overline P}$ = ${\overline S}$ . Then, every execution satisfying the specification is a possible execution of the program; we then call P maximal for the specification S . We argue that maximality is an important criterion in the context of designing concurrent programs because it disallows implementations that do not exhibit enough concurrency. In addition, a maximal solution can serve as a basis for deriving a variety of implementations, each appropriate for execution on a specific computing platform. This paper also describes 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 several non-trivial examples. The method may also serve as a guide in constructing maximal programs.