page 2  (19 pages)
to previous section1
3to next section

1 Parallel Composition

VLSI is an example of parallel programming as Chuck Seitz asserts. The success of VLSI is due in part to a hierarchy of interfaces for composing circuits: from composing transistors to form memory units, to composing microprocessors to form multicomputers. A designer putting transistors together has to be concerned with issues such as parasitic capacitance. A designer putting microprocessors together works with a more restrictive interface that does not deal with such details; the interface is such that a microprocessor behaves as a microprocessor regardless of the circuits to which it is connected. Composing transistors and composing microprocessors are both instances of parallel composition; the interfaces between transistors is different from the interfaces between microprocessors, and therefore, the ways of reasoning about compositions of transistors is different from the ways of reasoning about compositions of microprocessors.

What is the analogy to composing processes? There are situations where we may want to employ flexible interfaces between concurrent processes and other situations in which we want to use more restrictive interfaces between processes. In general, more restrictive interfaces allow for simpler proof techniques and more flexible interfaces can provide more efficiency. We propose a notation and methods of reasoning about programs that allow programmers to design different kinds of interfaces between concurrent processes. Programmers can balance flexibility on the one hand with ease of reasoning on the other, in designing their own interfaces.

A very flexible interface between concurrent processes is where processes share variables, and use atomicity and await commands [OG76]; in this case methods of reasoning are based on non-interference [OG76] or temporal logic and its derivatives [Pnu81, CM88, Lam91]. More restrictive interfaces and specifications allow us to use the powerful specification-conjunction rule for reasoning about parallel composition.
Consider a simple example that illustrates the problem of interfaces between concurrent processes.

Example The process p:

do x = ! x := x+2 [] x = 1 ! x := -1 od