Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

1. Borrione, D., Helmy, A., Pierre, L., Schmaltz, J.: A formal approach to the verification of networks on chip. In: EURASIP Journal on Embedded Systems, 2009(Article ID 548324), 14 pp. doi:10.1155/2009/548324 (2009)

2. Boyer, R.S., Strother Moore, J.: The addition of bounded quantification and partial functions to a computational logic and its theorem prover. J. Autom. Reason. 4(2), 117–172 (1988)

   Article  MATH  Google Scholar 

3. Boyer, R.S., Strother Moore, J.: A Computation Logic Handbook. Academic Press (1988)

4. Chen, R.C.: Deadlock prevention in message switched networks. In: ACM 74: Proceedings of the 1974 Annual Conference, pp. 306–310. ACM, New York, NY, USA (1974)

   Chapter  Google Scholar 

5. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press and McGraw Hill (1990)

6. Dally, W.J., Seitz, C.L.: Deadlock-free message routing in multiprocessor interconnection networks. IEEE Trans. Comput. 36(5), 547–553 (1987)

   Article  MATH  Google Scholar 

7. Dally, W.J., Towles, B.: Principles and Practices of Interconnection Networks. Morgan Kaufmann (2004)

8. Duato, J.: A necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks. IEEE Trans. Parallel Distrib. Syst. 6(10), 1055–1067 (1995)

   Article  Google Scholar 

9. Duato, J., Yalamanchili, S., Ni, L.: Interconnection Networks: an Engineering Approach. IEEE Computer Society Press, Los Alamitos, CA, USA (1997)

   Google Scholar 

10. Fleury, E., Fraigniaud, P.: A general theory for deadlock avoidance in wormhole-routed networks. IEEE Trans. Parallel Distrib. Syst. 9(7), 626–638 (1998)

    Article  Google Scholar 

11. Kaufmann, M., Strother Moore, J.: An industrial strengh theorem prover of a logic based on common lisp. IEEE Trans. Softw. Eng. 23(4), 203–213 (1997)

    Article  Google Scholar 

12. Kaufmann, M., Strother Moore, J.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161–203 (1997)

    Article  Google Scholar 

13. Kaufmann, M., Manolios, P., Strother Moore, J.: ACL2 Computer-Aided Reasoning: an Approach. Kluwer Academic Press (2000)

14. Manolios, P., Strother Moore, J.: Partial functions in ACL2. J. Autom. Reason. 31(2), 107–127 (2003)

    Article  MATH  Google Scholar 

15. Ni, L.M., Mckinley, P.K.: A survey of wormhole routing techniques in direct networks. IEEE Comput. 26, 62–76 (1993)

    Article  Google Scholar 

16. Ray, S.: Quantification in tail-recursive function definitions. In: Manolios, P., Wilding, M. (eds.) Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2006). ACM International Conference Series, vol. 205, pp. 95–98. ACM, Seattle, WA (2006)

    Chapter  Google Scholar 

17. Schmaltz, J., Borrione, D.: Towards a formal theory of on chip communications in the ACL2 logic. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, part of FloC’06, 14–15 August 2006. ACM, Seattle, WA (2006)

    Google Scholar 

18. Schmaltz, J., Borrione, D.: A functional formalization of on chip communications. Form. Asp. Comput. 20, 241–258 (2008)

    Article  MATH  Google Scholar 

19. Schwiebert, L., Jayasimha, D.N.: A universal proof technique for deadlock-free routing in interconnection networks. In: 7th Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 175–184 (1995)

20. Verbeek, F., Schmaltz, J.: Formal validation of deadlock prevention in networks-on-chips. In: Ray, S., Russinoff, D. (eds.) Eighth International Workshop on the ACL2 Theorem Prover and its Application, pp. 135–145, 11–12 May 2009. Northeastern University, Boston MA, USA. ACM (2009)

21. Verbeek, F., Schmaltz, J.: Formal specification of networks-on-chips: deadlock and evacuation. In: Proc. of Design, Automation, and Test in Europe (DATE’10), pp. 1701–1706 (2010)

Download references