Deadlock analysis in networks of communicating processes
Deadlock analysis in networks of communicating processes
复制标题
通信进程网络中的死锁分析
DOI：
10.1007/bf01784721
复制
发表时间：
1989
影响因子：
1.3
通讯作者：
A. W. Roscoe
中科院分区：
文献类型：
--
作者：
S. Brookes;A. W. Roscoe
我们使用CSP的故障模型来描述一类网络通信过程的行为。该模型非常适合于推理网络的死锁潜力。我们介绍了一些简单的条件，网络，帮助死锁分析本地化所需的分析证明死锁自由或限制的情况下，死锁可能发生。特别是，我们制定了一些简单的定理，描述的状态，死锁可能发生，并使用它们来证明一些定理的情况下，全球死锁的系统。我们确定了一类特殊的单向网络，并制定专门的结果，他们的死锁自由。我们开发了更一般的方法的基础上（最多）成对的局部死锁分析网络，适用于大类的无冲突网络。我们介绍了一种方法来证明死锁自由在一个大的网络分解成子网络，可以单独分析。给出了各种例子来说明这些结果的实用性。我们比较了我们的工作与其他几位作者的早期工作，并为未来的研究提出了一些建议。
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.