Subscribe

Issue No.12 - December (2011 vol.22)

pp: 2022-2032

Freek Verbeek , Radboud University Nijmegen, Nijmegen

Julien Schmaltz , Open University of the Netherlands, Nijmegen

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TPDS.2011.60

ABSTRACT

Wormhole switching is a popular switching technique in interconnection networks. This technique is also prone to deadlocks. Adaptive routing algorithms provide alternative paths that can be used to escape congested areas and prevent some deadlocks to occur. If not designed carefully, these new paths may as well introduce deadlocks. A successful solution to deadlock prevention is to constrain the routing function such that it does not introduce any deadlock. Many necessary and sufficient conditions for deadlock-free routing have been proposed. The definition and the proof of these conditions are complex and error-prone. These conditions are often counterintuitive and difficult to understand. Moreover, they are not static, as they all require the analysis of configurations, i.e., the network state. The contribution of this paper is twofold. We present the first static necessary and sufficient condition for deadlock-free routing in wormhole networks. Our condition is much simpler and requires less assumptions than all previous ones. It is formally proven correct using an automated proof assistant. In particular, our condition applies to incoherent routing functions which was considered an open problem. Second, we prove the deadlock decision problem co-NP-complete for wormhole networks.

INDEX TERMS

Formal models, communication networks, deadlocks, routing protocols, mechanical verification.

CITATION

Freek Verbeek, Julien Schmaltz, "On Necessary and Sufficient Conditions for Deadlock-Free Routing in Wormhole Networks",

*IEEE Transactions on Parallel & Distributed Systems*, vol.22, no. 12, pp. 2022-2032, December 2011, doi:10.1109/TPDS.2011.60REFERENCES

- [1] W. Dally and C. Seitz, "Deadlock-Free Message Routing in Multiprocessor Interconnection Networks,"
IEEE Trans. Computers, vol. C-36, no. 5, pp. 547-553, May 1987.- [2] J. Duato, "A Necessary and Sufficient Condition for Deadlock-Free Adaptive Routing in Wormhole Networks,"
IEEE Trans. Parallel and Distributed Systems, vol. 6, no. 10, pp. 1055-1067, Oct. 1995.- [3] P.E. Berman, L. Gravano, G.D. Pifarré, and J.L.C. Sanz, "Adaptive Deadlock- and Livelock-Free Routing with All Minimal Paths in Torus Networks,"
Proc. Fourth Ann. ACM Symp. Parallel Algorithms and Architectures (SPAA '92), pp. 3-12, 1992.- [4] W. Dally and H. Aoki, "Deadlock-Free Adaptive Routing in Multicomputer Networks Using Virtual Channels,"
IEEE Trans. Parallel and Distributed Systems, vol. 4, no. 4, pp. 466-475, Apr. 1993.- [5] R.V. Boppana and S. Chalasani, "A Comparison of Adaptive Wormhole Routing Algorithms,"
ACM SIGARCH Computer Architecture News, vol. 21, no. 2, pp. 351-360, 1993.- [6] C.J. Glass and L.M. Ni, "The Turn Model for Adaptive Routing,"
J. ACM, vol. 41, no. 5, pp. 874-902, 1994.- [7] A.A. Chien and J.H. Kim, "Planar-Adaptive Routing: Low-Cost Adaptive Networks for Multiprocessors,"
J. ACM, vol. 42, no. 1, pp. 91-123, 1995.- [8] F. Silla, M.P. Malumbres, A. Robles, P. López, and J. Duato, "Efficient Adaptive Routing in Networks of Workstations with Irregular Topology,"
Proc. First Int'l Workshop Comm. and Architectural Support for Network-Based Parallel Computing (CANPC '97). pp. 46-60, 1997.- [9] J. Duato, "A New Theory of Deadlock-Free Adaptive Routing in Wormhole Networks,"
IEEE Trans. Parallel and Distributed Systems, vol. 4, no. 12, pp. 1320-1331, Dec. 1993.- [10] L. Schwiebert and D. Jayashima, "A Necessary and Sufficient Condition for Deadock-Free Wormhole Routing,"
J. Parallel and Distributed Computing, vol. 32, pp. 103-117, 1996.- [11] E. Fleury and P. Fraigniaud, "A General Theory for Deadlock Avoidance in Wormhole-Routed Networks,"
IEEE Trans. Parallel and Distributed Systems, vol. 9, no. 7, pp. 626-638, July 1998.- [12] S. Taktak, E. Encrenaz, and J.-L. Desbarbieux, "A Polynomial Algorithm to Prove Deadlock-Freeness of Wormhole Networks,"
Proc. 18th Euromicro Int'l Conf. Parallel, Distributed and Network-Based Computing (PDP '10), Feb. 2010.- [13] F. Verbeek and J. Schmaltz, "A Comment on 'A Necessary and Sufficient Condition for Deadlock-Free Adaptive Routing in Wormhole Networks,'"
IEEE Trans. Parallel and Distributed Systems, vol. 22, no. 10, pp. 1775-1776, Oct. 2011.- [14] M. Kaufmann, P. Manolios, and J.S. Moore, "ACL2 Computer-Aided Reasoning: An Approach," 2000.
- [15] F. Verbeek and J. Schmaltz, "Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks,"
J. Automated Reasoning, online first, Springer, 2011, DOI: 10.1007/s10817-010-9206-x. - [16] J. Duato, S. Yalamanchili, and L. Ni,
Interconnection Networks: An Engineering Approach. Morgan Kaufmann Publishers, 2003.- [17] T. Cormen, C. Leiserson, and R. Rivest,
Introduction to Algorithms. MIT Press and McGraw Hill, 1990.- [18] F. Verbeek and J. Schmaltz, "A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free,"
Proc. 19th Int'l Euromicro Conf. Parallel, Distributed and Network-Based Processing, http://www.cs.ru.nl/~julien/Julien_at_Nijmegen ps_df_algo.html, 2011.- [19] T. Hales, "Flyspeck Project," http://www.math.pitt.edu/thalesflyspeck/, 2010.
- [20] S. Beyer, C. Jacobi, D. Kröning, D. Leinenbach, and W.J. Paul, "Putting It All Together—Formal Verification of the VAMP,"
Int'l J. Software Tools for Technology Transfer, vol. 8, nos. 4/5, pp. 411-430, 2006.- [21] A. Fox, "Formal Specification and Verification of ARM6,"
Proc. 16th Int'l Conf. Theorem Provers in Higher-Order Logics (TPHOLs '03), D. Basin and B. Wolff, eds., pp. 24-40, 2003.- [22] W. Hunt, "Mechanical Mathematical Methods for Microprocessor Verification,"
Proc. Int'l Conf. Computer Aided Verification (CAV '04), pp. 523-533, 2004.- [23] D. Russinoff, "A Mechanically Checked Proof of IEEE Compliance of a Register Transfer Level Specification of the AMD-K7 Floating-Point Multiplication, Division and Square Root Instructions,"
London Math. Soc. J. Computation and Math., vol. 1, pp. 148-200, Dec. 1998.- [24] W. Hunt and S. Swords, "Centaur Technology Media Unit Verification,"
Proc. Int'l Conf. Computer Aided Verification (CAV '09), pp. 353-367, 2009.- [25] C. Berg and C. Jacobi, "Formal Verification of the VAMP Floating Point Unit,"
Proc. 11th Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME), pp. 325-339, 2001.- [26] J. Harrison, "Floating-Point Verification,"
J. Universal Computer Science, vol. 13, no. 5, pp. 629-638, 2007.- [27] J. Schmaltz and D. Borrione, "A Functional Formalization of On Chip Communications,"
Formal Aspects of Computing, vol. 20, pp. 241-258, 2008.- [28] G. Klein, R. Huuck, and B. Schlich, "Operating System Verification,"
J. Automated Reasoning, vol. 42, nos. 2-4, pp. 123-124, 2009.- [29] W. Bevier, W. Hunt, J.S. Moore, and W. Young, "An Approach to Systems Verification,"
J. Automated Reasoning, vol. 5, no. 4, pp. 411-428, 1989.- [30] T. Nipkow, L. Paulson, and M. Wenzel,
Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002.- [31] S. Owre, J. Rushby, and N. Shankar, "PVS: A Prototype Verification System,"
Proc. 11th Int'l Conf. Automated Deduction (CADE '92), D. Kapur, ed., vol. 607, pp. 748-752, June 1992.- [32] Y. Bertot, "A Short Presentation of Coq,"
Proc. 21st Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '08), pp. 12-16, 2008.- [33] M. Gordon, "HOL: A Proof Generating System for Higher-Order Logic,"
VLSI Specification, Verification and Synthesis, G. Birthwislte and P. Subrahmanyam, eds., pp. 73-128, Kluwer Academic Publishers, 1987.- [34] J. Harrison, "HOL Light: An Overview,"
Proc. 22nd Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '09), pp. 60-66, 2009.- [35] D. Borrione, A. Helmy, L. Pierre, and J. Schmaltz, "A Formal Approach to the Verification of Networks on Chip,"
EURASIP J. Embedded Systems, vol. 2009, p. 14, 2009, doi:10.1155/2009/548324. - [36] F. Verbeek and J. Schmaltz, "Formal Specification of Networks-on-Chips: Deadlock and Evacuation,"
Proc. Design, Automation and Test in Europe (DATE '10) Conf., pp. 1701-1706, Mar. 2010.- [37] F. Verbeek and J. Schmaltz, "Proof Pearl: A Formal Proof of Duato's Condition for Deadlock-Free Adaptive Networks,"
Proc. Interactive Theorem Proving (ITP '10), pp. 67-82, Springer, July 2010. |