Deadlock Free Specification Based on Local Process Properties

摘要

We present a design methodology for the construction of parallel programs that is deadlock free, Provided that the "components" of the program are constructed according to a set of locally applied rules. In our model, a parallel program is a set of processes and a set of events. Each event is shared by two processes only and each process progresses cyclically. Events are distinguished as input and output events with respect to their two participating processes. On each cycle a process must complete all output events that it offers to the environment, be prepared to accept any, and accept at least one, of its input events before completing any computations and starting a new cycle. We show that however the events are distributed among the processes, the program is deadlock free. Using this model we can construct libraries of constituent processes that do not require any global analysis to establish freedom from deadlock when they are used to construct complete parallel programs.