Report Number: CS-TR-70-172
Institution: Stanford University, Department of Computer Science
Title: Analysis of parallel systems
Author: Bredt, Thomas H.
Date: August 1970
Abstract: A formal analysis procedure for parallel computer systems is presented. The flow table model presented in an earlier paper [Stanford University Department of Computer Science report STAN-CS-70-160] is used to describe a system. Each component to the system is described by a completely specified fundamental-mode flow table. All delays in a parallel system are assumed to be finite. Component delays are assumed to be bounded and line delays unbounded. The concept of an output hazard is introduced to account for the effects of line delay and the lack of synchronization among components. Necessary and sufficient conditions for the absence of output hazards are given. The state of a parallel system is defined by the present internal state and input state of each component. The operation of the system is described by a system state graph which specifies all possible state transitions for a specified initial system state. A procedure for constructing the system state graph is given. The analysis procedure may be summarized as follows. A problem is stated in terms of restrictions on system operation. A parallel system is said to operate correctly with respect to the given problem if the associated restrictions are always satisfied. The restrictions specify either forbidden system states, which are never to be entered during the operation of the system, or forbidden system state sequences, which must never appear during system operation. The restrictions are tested by examining the system state graph. A parallel system for the two-process mutual exclusion problem is analyzed and the system is shown to operate correctly with respect to this problem. Finally, the conditions of determinacy and output functionality, which have been used in other models of parallel computing, are discussed as they relate to correct solutions to the mutual exclusion problem.
http://i.stanford.edu/pub/cstr/reports/cs/tr/70/172/CS-TR-70-172.pdf