Proof pearl : a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks

F. Verbeek, J. Schmaltz

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)

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 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.
Original languageEnglish
Pages (from-to)419-439
Number of pages21
JournalJournal of Automated Reasoning
Volume48
Issue number4
DOIs
Publication statusPublished - 2012
Externally publishedYes

Fingerprint Dive into the research topics of 'Proof pearl : a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks'. Together they form a unique fingerprint.

Cite this