Static Deadlock Analysis for CSP-type Communications

. We present two tests for analyzing deadlock for a class of communicating sequential processes. The tests can be used for deadlock detection in parallel and distributed programs at compile time, or for debugging purposes at run time. They can also be used in conjunction with an algorithm we have for constructing valid execution traces for this class. Introduction Distributed systems, high-level software designs, software for parallel processors, and communications protocols can be specified as collections of communicating processes. It is very hard to analyze software for such systems, whether it is expressed abstractly (`specifications') or concretely (`code'). We focus on finite-state analysis techniques for specifications or code involving communicating processes. Because of length constraints, we omit proofs from this paper. The proofs can be found in [LS92b] and our monograph that will be published soon in the Springer-Verlag Lecture Notes in Computer Science series [LS94]. Our ..