Abstract
Deadlocks occur in interconnection networks as messages compete for free channels or empty buffers. Deadlocks are often associated with a circular wait between processes and resources. In the context of networks, Duato proved that for adaptive routing networks a cyclic dependency is not sufficient to create a deadlock. He proposed deadlock-free routing techniques allowing cyclic dependencies between channels or buffers. His work was a breakthrough. It was also counterintuitive and only a complex mathematical proof could convince his peers about the soundness of his theory. We define a necessary and sufficient condition that captures Duato’s intuition but that is more intuitive and leads to a simpler proof. However, our condition is logically equivalent to Duato’s one. We used the ACL2 theorem proving system to formalize our condition and its proof. In particular, we used two features of ACL2, namely the encapsulation principle and quantifiers, to perform an elegant formalization based on second order functions.
This research is supported by NWO/EW project Formal Validation of Deadlock Avoidance Mechanisms (FVDAM) under grant no. 612.064.811.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Stalling, W.: Operating Systems, Internals and Design Principles. Pearson Education International, London (2009)
Dally, W., Seitz, C.: Deadlock-free message routing in multiprocessor interconnection networks. IEEE Transactions on Computers (36), 547–553 (1987)
Duato, J.: A necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks. IEEE Transactions on Parallel and Distributed Systems 6(10), 1055–1067 (1995)
Duato, J., Yalamanchili, S., Ni, L.: Interconnection Networks, an engeneering approach. Morgan Kaufmann Publishers, San Francisco (2003)
Kaufmann, M., Manolios, P., Moore, J.S.: ACL2 Computer-Aided Reasoning: An Approach (2000)
Verbeek, F., Schmaltz, J.: Proof pearl: A formal proof of dally and seitz’ necessary and sufficient condition for deadlock-free routing in interconnection networks. J. Autom. Reasoning (2009) (submitted to publication), http://www.cs.ru.nl/~julien/Julien_at_Nijmegen/JAR09.html
Kaufmann, M., Manolios, P., Moore, J.S.: ACL2 Computer Aided Reasoning: An Approach. Kluwer Academic Press, Dordrecht (2000)
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), Seattle, WA, August 2006. ACM International Conference Series, vol. 205, pp. 95–98. ACM Press, New York (2006)
Kaufmann, M., Moore, J.S.: Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning 26(2), 161–203 (1997)
Verbeek, F., Schmaltz, J.: Formal specification of networks-on-chip: deadlock, livelock, and evacuation. In: Proceedings of Design, Automation & Test in Europe 2010 (DATE’10) (March 2010)
Misra, J., Chandy, K.: A distributed graph algorithm: knot detection. ACM Transactions on Programming Languages and Systems 4(4), 678–686 (1982)
Duato, J.: A necessary and sufficient condition for deadlock-free adaptive routing in cut-through and store-and-forward networks. IEEE Transactions on Parallel and Distributed Systems 7(8), 841–1067 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Verbeek, F., Schmaltz, J. (2010). A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-14052-5_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14051-8
Online ISBN: 978-3-642-14052-5
eBook Packages: Computer ScienceComputer Science (R0)