Deadlock analysis in networks of communicating processes

We use the failures model of CSP to describe the behaviour of a class of networks of communicating processes. This model is well suited to reasoning about the deadlock potential of networks. We introduce a number of simple conditions on networks which aid deadlock analysis either by localizing the analysis required for a proof of deadlock-freedom or by restricting the circumstances in which deadlock could occur. In particular, we formulate some simple theorems which characterize the states in which deadlock can occur, and use them to prove some theorems on the absence of global deadlock in systems. We identify a special class of unidirectional networks and develop specialized results on their deadlock-freedom. We develop more general methods based on (at most) pairwise local deadlock analysis in networks, applicable to the large class of conflict-free networks. We introduce a methodology for proving deadlock-freedom in a large network by decomposing it into subnetworks which can be analysed separately. A variety of examples is given to show the utility of these results. We compare our work with earlier work by several other authors, and make some suggestions for future research.S.D. Brookes received a B.A. in mathematics (1978) and a D.Phil. in computer science (1983), both from Oxford University. His D. Phil supervisor was C.A.R. Hoare. He moved to Carnegie Mellon University in 1981, initially as a Research Computer Scientist and then (1984–1990) as an Assistant Professor in the School of Computer Science at CMU. He is currently an Associate Professor of Computer Science at CMU. His research interests include the mathematical foundations of programming languages, the theory of parallel and sequential computation, programming methodology, programming language design, and the development of semantically based logics for reasoning about program behavior.A.W. Roscoe received a B.A. in mathematics (1978) and a D.Phil. in computer science (1982), both from Oxford University. His D. Phil supervisor was C.A.R. Hoare. He was formerly a Junior Research Fellow at St Edmund Hall, Oxford (1980–1982) and the IBM Research Fellow of the Royal Society (1982–1983). Since 1983 he has been a University Lecturer in Computation at Oxford and a Fellow of University College. His research interests include the theory of parallel computing and its applications (e.g., to VLSI design), domain theory, distributed databases, general topology and the theory of image processing.This research was supported in part by funds from the Computer Science Department of Carnegie Mellon University, and by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 4976, monitored by the Air Force Avionics Laboratory under Contract F33615-87-C-1499. A.W. Roscoe gratefully acknowledges support by ONR Grant N00014-87-G-0242. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the offical policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the US Government.