Given a network of routing nodes, represented as a directed graph, we prove the following necessary and sufficient condition for the existence of deadlock-free message routing: The directed graph must contain two edge-disjoint directed trees rooted at the same node, one tree directed into the root node and the other directed away from the root node. While the sufficiency of this condition is known, its necessity, to the best of our knowledge, has not been previously recognized or proven. Although not directly applicable to the construction of deadlock-free routing schemes, this result provides a fundamental insight into the nature of deadlock-free networks and may lead to the development of improved tools for designing and verifying such schemes.
翻译:给定一个由路由节点组成的网络,其表示为有向图,我们证明了无死锁消息路由存在的一个充要条件:该有向图必须包含两棵以同一节点为根且边不相交的有向树,其中一棵树指向根节点,另一棵树从根节点指向外。尽管该条件的充分性已知,但据我们所知,其必要性此前并未被认识或证明。虽然这一结果不能直接应用于构建无死锁路由方案,但它为理解无死锁网络的基本性质提供了关键见解,并可能促进设计和验证此类方案的改进工具的开发。