Abstract
Avoiding message dependent deadlocks in communication fabrics is critical for modern microarchitectures. If discovered late in the design cycle, deadlocks lead to missed project deadlines and suboptimal design decisions. One approach to avoid this problem is to get high level of confidence on an early microarchitectural model. However, formal proofs of liveness even on abstract models are hard due to large number of queues and distributed control. In this work we address liveness verification of communication fabrics described in the form of high-level microarchitectural models which use a small set of well-defined primitives. We prove that under certain realistic restrictions, deadlock freedom can be reduced to unsatisfiability of a system of Boolean equations. Using this approach, we have automatically verified liveness of several non-trivial models (derived from industrial microarchitectures), where state-of-the-art model checkers failed and pen and paper proofs were either tedious or unknown.
This is a preview of subscription content, log in via an institution to check access.
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
NuSMV home page, http://nusmv.irst.itc.it/
Barkaoui, K., Dutheillet, C., Haddad, S.: An efficient algorithm for finding structural deadlocks in colored Petri nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 69–88. Springer, Heidelberg (1993)
Berkeley Logic Synthesis and Verification Group: ABC: A system for sequential synthesis and verification, http://www.eecs.berkeley.edu/~alanmi/abc/
Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science 66(2), 160–177 (2002)
Chatterjee, S., Kishinevsky, M.: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 321–338. Springer, Heidelberg (2010)
Chatterjee, S., Kishinevsky, M., Ogras, U.Y.: Quick formal modeling of communication fabrics to enable verification. In: Proc. IEEE High Level Design Validation and Test Workshop (HLDVT), pp. 42–49 (2010)
Dally, W., Towles, B.: Principles and Practices of Interconnection Networks. Morgan Kaufmann, San Francisco (2004)
Duato, J.: A necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks. IEEE Trans. Paral. Distrib. Syst. 6(10), 1055–1067 (1995)
Gebremichael, B., Vaandrager, F.W., Zhang, M., Goossens, K.G.W., Rijpkema, E., Rădulescu, A.: Deadlock prevention in the æthereal protocol. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 345–348. Springer, Heidelberg (2005)
Ghafari, N., Gurfinkel, A., Klarlund, N., Trefler, R.J.: Algorithmic analysis of piecewise fifo systems. In: FMCAD, pp. 45–52 (2007)
Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V.: Proving that non-blocking algorithms don’t block. In: POPL 2009: Proc. of Symp. on Principles of Prog. Lang., pp. 16–28. ACM, New York (2009)
Hansson, A., Goossens, K., Rădulescu, A.: Avoiding message-dependent deadlock in network-based systems on chip. VLSI Design 2007 (May 2007)
Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for pipelined machines using web refinement. ACM Trans. Des. Autom. Electron. Syst. 13(3), 1–19 (2008)
McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 342–345. Springer, Heidelberg (1999)
Taktak, S., Desbarbieux, J.L., Encrenaz, E.: A tool for automatic detection of deadlock in wormhole networks on chip. ACM Trans. Design Autom. Electr. Syst. 13(1) (1995)
Verbeek, F., Schmaltz, J.: Formal specification of networks-on-chips: deadlock and evacuation. In: DATE 2010, pp. 1701–1706 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gotmanov, A., Chatterjee, S., Kishinevsky, M. (2011). Verifying Deadlock-Freedom of Communication Fabrics. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-18275-4_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18274-7
Online ISBN: 978-3-642-18275-4
eBook Packages: Computer ScienceComputer Science (R0)