A formal model of message blocking and deadlock resolution in interconnection networks

This paper presents a theoretical model of resource allocations and dependencies in wormhole and virtual cut-through interconnection networks. This model allows various types of message blocking to be described precisely, including deadlock. The model distinguishes between messages involved in deadlock and those simply dependent upon deadlock, thus establishing a framework for evaluating the accuracy and correctness of deadlock detection mechanisms. The paper also identifies the necessary and sufficient conditions for the occurrence and resolution of deadlock in interconnection networks, thus providing efficiency and correctness criteria for deadlock resolution mechanisms. Theorems derived from the model are related to various routing algorithms which are based on deadlock recovery