Visible to the public A Decision Procedure for Deadlock-Free Routing in Wormhole Networks

TitleA Decision Procedure for Deadlock-Free Routing in Wormhole Networks
Publication TypeJournal Article
Year of Publication2014
AuthorsVerbeek, F., Schmaltz, J.
JournalParallel and Distributed Systems, IEEE Transactions on
Date PublishedAug
Keywordsadaptive routing function, automatic verification, co-NP-complete problem, communication network design, Communication networks, computational complexity, computer networks, deadlock freedom, deadlock-free routing, deadlocks, decision procedure, Design methodology, formal methods, Grippers, integer programming, Linear programming, necessary condition, Network topology, Routing, routing functions, Routing protocols, sufficient condition, Switches, System recovery, telecommunication network routing, telecommunication network topology, Topology, torus topologies, wormhole networks, wormhole switching technique

Deadlock freedom is a key challenge in the design of communication networks. Wormhole switching is a popular switching technique, which is also prone to deadlocks. Deadlock analysis of routing functions is a manual and complex task. We propose an algorithm that automatically proves routing functions deadlock-free or outputs a minimal counter-example explaining the source of the deadlock. Our algorithm is the first to automatically check a necessary and sufficient condition for deadlock-free routing. We illustrate its efficiency in a complex adaptive routing function for torus topologies. Results are encouraging. Deciding deadlock freedom is co-NP-Complete for wormhole networks. Nevertheless, our tool proves a 13 x 13 torus deadlock-free within seconds. Finding minimal deadlocks is more difficult. Our tool needs four minutes to find a minimal deadlock in a 11 x 11 torus while it needs nine hours for a 12 x 12 network.

Citation Key6564261