
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Freek Verbeek, Julien Schmaltz, "On Necessary and Sufficient Conditions for DeadlockFree Routing in Wormhole Networks," IEEE Transactions on Parallel and Distributed Systems, vol. 22, no. 12, pp. 20222032, December, 2011.  
BibTex  x  
@article{ 10.1109/TPDS.2011.60, author = {Freek Verbeek and Julien Schmaltz}, title = {On Necessary and Sufficient Conditions for DeadlockFree Routing in Wormhole Networks}, journal ={IEEE Transactions on Parallel and Distributed Systems}, volume = {22}, number = {12}, issn = {10459219}, year = {2011}, pages = {20222032}, doi = {http://doi.ieeecomputersociety.org/10.1109/TPDS.2011.60}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Parallel and Distributed Systems TI  On Necessary and Sufficient Conditions for DeadlockFree Routing in Wormhole Networks IS  12 SN  10459219 SP2022 EP2032 EPD  20222032 A1  Freek Verbeek, A1  Julien Schmaltz, PY  2011 KW  Formal models KW  communication networks KW  deadlocks KW  routing protocols KW  mechanical verification. VL  22 JA  IEEE Transactions on Parallel and Distributed Systems ER   
[1] W. Dally and C. Seitz, "DeadlockFree Message Routing in Multiprocessor Interconnection Networks," IEEE Trans. Computers, vol. C36, no. 5, pp. 547553, May 1987.
[2] J. Duato, "A Necessary and Sufficient Condition for DeadlockFree Adaptive Routing in Wormhole Networks," IEEE Trans. Parallel and Distributed Systems, vol. 6, no. 10, pp. 10551067, Oct. 1995.
[3] P.E. Berman, L. Gravano, G.D. Pifarré, and J.L.C. Sanz, "Adaptive Deadlock and LivelockFree Routing with All Minimal Paths in Torus Networks," Proc. Fourth Ann. ACM Symp. Parallel Algorithms and Architectures (SPAA '92), pp. 312, 1992.
[4] W. Dally and H. Aoki, "DeadlockFree Adaptive Routing in Multicomputer Networks Using Virtual Channels," IEEE Trans. Parallel and Distributed Systems, vol. 4, no. 4, pp. 466475, 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. 351360, 1993.
[6] C.J. Glass and L.M. Ni, "The Turn Model for Adaptive Routing," J. ACM, vol. 41, no. 5, pp. 874902, 1994.
[7] A.A. Chien and J.H. Kim, "PlanarAdaptive Routing: LowCost Adaptive Networks for Multiprocessors," J. ACM, vol. 42, no. 1, pp. 91123, 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 NetworkBased Parallel Computing (CANPC '97). pp. 4660, 1997.
[9] J. Duato, "A New Theory of DeadlockFree Adaptive Routing in Wormhole Networks," IEEE Trans. Parallel and Distributed Systems, vol. 4, no. 12, pp. 13201331, Dec. 1993.
[10] L. Schwiebert and D. Jayashima, "A Necessary and Sufficient Condition for DeadockFree Wormhole Routing," J. Parallel and Distributed Computing, vol. 32, pp. 103117, 1996.
[11] E. Fleury and P. Fraigniaud, "A General Theory for Deadlock Avoidance in WormholeRouted Networks," IEEE Trans. Parallel and Distributed Systems, vol. 9, no. 7, pp. 626638, July 1998.
[12] S. Taktak, E. Encrenaz, and J.L. Desbarbieux, "A Polynomial Algorithm to Prove DeadlockFreeness of Wormhole Networks," Proc. 18th Euromicro Int'l Conf. Parallel, Distributed and NetworkBased Computing (PDP '10), Feb. 2010.
[13] F. Verbeek and J. Schmaltz, "A Comment on 'A Necessary and Sufficient Condition for DeadlockFree Adaptive Routing in Wormhole Networks,'" IEEE Trans. Parallel and Distributed Systems, vol. 22, no. 10, pp. 17751776, Oct. 2011.
[14] M. Kaufmann, P. Manolios, and J.S. Moore, "ACL2 ComputerAided Reasoning: An Approach," 2000.
[15] F. Verbeek and J. Schmaltz, "Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for DeadlockFree Routing in Interconnection Networks," J. Automated Reasoning, online first, Springer, 2011, DOI: 10.1007/s108170109206x.
[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 StoreandForward Networks DeadlockFree," Proc. 19th Int'l Euromicro Conf. Parallel, Distributed and NetworkBased 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. 411430, 2006.
[21] A. Fox, "Formal Specification and Verification of ARM6," Proc. 16th Int'l Conf. Theorem Provers in HigherOrder Logics (TPHOLs '03), D. Basin and B. Wolff, eds., pp. 2440, 2003.
[22] W. Hunt, "Mechanical Mathematical Methods for Microprocessor Verification," Proc. Int'l Conf. Computer Aided Verification (CAV '04), pp. 523533, 2004.
[23] D. Russinoff, "A Mechanically Checked Proof of IEEE Compliance of a Register Transfer Level Specification of the AMDK7 FloatingPoint Multiplication, Division and Square Root Instructions," London Math. Soc. J. Computation and Math., vol. 1, pp. 148200, Dec. 1998.
[24] W. Hunt and S. Swords, "Centaur Technology Media Unit Verification," Proc. Int'l Conf. Computer Aided Verification (CAV '09), pp. 353367, 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. 325339, 2001.
[26] J. Harrison, "FloatingPoint Verification," J. Universal Computer Science, vol. 13, no. 5, pp. 629638, 2007.
[27] J. Schmaltz and D. Borrione, "A Functional Formalization of On Chip Communications," Formal Aspects of Computing, vol. 20, pp. 241258, 2008.
[28] G. Klein, R. Huuck, and B. Schlich, "Operating System Verification," J. Automated Reasoning, vol. 42, nos. 24, pp. 123124, 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. 411428, 1989.
[30] T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for HigherOrder 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. 748752, June 1992.
[32] Y. Bertot, "A Short Presentation of Coq," Proc. 21st Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '08), pp. 1216, 2008.
[33] M. Gordon, "HOL: A Proof Generating System for HigherOrder Logic," VLSI Specification, Verification and Synthesis, G. Birthwislte and P. Subrahmanyam, eds., pp. 73128, 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. 6066, 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 NetworksonChips: Deadlock and Evacuation," Proc. Design, Automation and Test in Europe (DATE '10) Conf., pp. 17011706, Mar. 2010.
[37] F. Verbeek and J. Schmaltz, "Proof Pearl: A Formal Proof of Duato's Condition for DeadlockFree Adaptive Networks," Proc. Interactive Theorem Proving (ITP '10), pp. 6782, Springer, July 2010.