DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TPDS.2013.121
Julien Schmaltz , Open University of the Netherlands
Freek Verbeek , Open University of The Netherlands
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 13x13 torus deadlock-free within seconds. Finding deadlocks is more difficult. Our tool needs four minutes to find a minimal deadlock in a 11x11 torus while it needs nine hours for a 12x12 network.
System recovery, Routing, Grippers, Topology, Network topology, Design methodology, Switches, Routing protocols, Hardware, Integrated Circuits, Design Aids, Verification, Computer Systems Organization, Communication/Networking and Information Technology, Network Architecture and Design, Network communications, Network Protocols
Julien Schmaltz, Freek Verbeek, "A Decision Procedure for Deadlock-Free Routing in Wormhole Networks", IEEE Transactions on Parallel & Distributed Systems, vol. , no. , pp. 0, 5555, doi:10.1109/TPDS.2013.121