Computer Science Department
School of Computer Science, Carnegie Mellon University


Deadlock Analysis in Networks of Communicating Processes


Stephen D. Brookes, Andrew W. Roscoe oot Oxford University, Programming Research Group

October 1984/January 1985 oot To Appear in: Proceedings of Advanced NATO Study Institute on Logics and Models for Verification and Specification of Concurrent Systems , La Colle-sur-Loup, October 1984, Springer Verlag Lecture Notes in Computer Science, 1985.

We use the failures model of Communicating Sequential Processes to describe the behavior of a simple class of networks of communicating processes. This model is well suited to reasoning about the deadlock behavior of processes, and we demonstrate this fact by proving some results which help in the analysis of deadlock in networks. 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 certain classes of systems. Some examples are given to show the utility of these results.

20 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by