Proof Pearl: A formal proof of Dally&Seitz necessary and sufficient condition for deadlock-free routing in interconnection networks

Freek Verbeek and Julien Schmaltz

Abstract

Avoiding deadlock is crucial to interconnection networks. In '87, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel dependency graph is acyclic. We formally define and prove a slightly different condition from which the original condition of Dally and Seitz can be derived. Dally and Seitz prove that a deadlock situation induces cyclic dependencies by reductio ad absurdum. In contrast we introduce the notion of a waiting graph from which we explicitly construct such a cyclic dependency from a deadlock situation. Moreover, our proof is structured in such a way that it only depends on a small set of proof obligations associated to arbitrary routing functions and switching policies. Discharging these proof obligations is sufficient  to instantiate our condition for deadlock-free routing on particular networks.Our condition and its proof have been formalized using the ACL2 theorem proving system.

Supporting Materials (ACL2 files)



.tar.gz archive here.

Pre-Print


A preliminary version of the paper can be found here.