More Web Proxy on the site http://driver.im/

research-article

Automatic verification for deadlock in Networks-on-Chips with adaptive routing and wormhole switching

Authors:

Julien SchmaltzAuthors Info & Claims

NOCS '11: Proceedings of the Fifth ACM/IEEE International Symposium on Networks-on-Chip

Pages 25 - 32

https://doi.org/10.1145/1999946.1999951

Published: 01 May 2011 Publication History

Abstract

Wormhole switching is a switching technique nowadays commonly used in networks-on-chips (NoCs). It is efficient but prone to deadlock. The design of a deadlock-free adaptive routing function constitutes an important challenge. We present a novel algorithm for the automatic verification that a routing function is deadlock-free in wormhole networks. A sufficient condition for deadlock-free routing and an associated algorithm are defined. The algorithm is proven complete for the condition. The condition, the algorithm, and the correctness theorem have been formalized and checked in the logic of the ACL2 interactive theorem proving system. The algorithm has a time complexity in O(N³), where N denotes the number of nodes in the network. This outperforms the previous solution of Taktak et al. by one degree. Experimental results confirm the high efficiency of our algorithm. This paper presents a formally proven correct algorithm that detects deadlocks in a 2D-mesh with about 4000 nodes and 15000 channels within seconds.

References

[1]

L. Benini and G. D. Micheli. Networks on Chips: A New SoC Paradigm. Computer, 35(1):70--78, 2002.

Digital Library

[2]

E. Bolotin, I. Cidon, R. Ginosar, and A. Kolodny. Qnoc: Qos architecture and design process for network on chip. Journal of Systems Architecture, 50(2--3):105--128, 2004.

Digital Library

[3]

M. Coppola, S. Curaba, M. Grammatikakis, G. Maruccia, and F. Papariello. OCCN: A network-on-chip modeling and simulation framework. In DATE, pages 174--179, 2004.

Digital Library

[4]

M. Coppola, M. Grammatikakis, R. Locatelli, G. Mariuccia, and L. Pieralisi. Design of interconnect processing units Spidergon STNoC. CRC Press, 2009.

Digital Library

[5]

W. J. Dally and B. Towles. Route packets, not wires: on-chip interconnection networks. In Proceedings of the Design Automation Conference, pages 684--689, Las Vegas, NV, 2001.

Digital Library

[6]

J. Duato. 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.

Digital Library

[7]

J. Duato, S. Yalamanchili, and N. Lionel. Interconnection Networks: An Engineering Approach. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002.

Digital Library

[8]

E. Fleury and P. Fraigniaud. A general theory for deadlock avoidance in wormhole-routed networks. IEEE Transactions on Parallel and Distributed Systems, 9(7):626--638, 1998.

Digital Library

[9]

C. J. Glass and L. M. Ni. The turn model for adaptive routing. Journal of the ACM, 41(5):874--902, 1994.

Digital Library

[10]

K. Goossens, J. Dielissen, and A. Rădulescu. The Æthereal network on chip: Concepts, architectures, and implementations. IEEE Design and Test of Computers, 22(5):21--31, Sept.-Oct. 2005.

Digital Library

[11]

F. Karim, A. Nguyen, and S. Dey. An interconnect architecture for networking systems on chips. IEEE Micro, 22(5):36--45, 2002.

Digital Library

[12]

M. Kaufmann, P. Manolios, and J. S. Moore. ACL2 Computer-Aided Reasoning: An Approach, 2000.

Digital Library

[13]

G. D. Micheli and L. Benini. Networks on Chips: Technology and Tools (Systems on Silicon). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2006.

Digital Library

[14]

F. Moraes, N. Calazans, A. Mello, L. Möller, and L. Ost. Hermes: an infrastructure for low area overhead packet-switching networks on chip. Integration, the VLSI Journal, 38(1):69--93, 2004.

Digital Library

[15]

L. Ni and P. McKinley. A survey of wormhole routing techniques in direct networks. IEEE Computer, 26:62--76, 1993.

Digital Library

[16]

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

Digital Library

[17]

S. Taktak, J.-L. Desbarbieux, and E. Encrenaz. A tool for automatic detection of deadlock in wormhole networks on chip. ACM Transactions on Design Automation of Electronic Systems, 13(1), January 2008.

Digital Library

[18]

S. Taktak, E. Encrenaz, and J.-L. Desbarbieux. A polynomial algorithm to prove deadlock-freeness of wormhole networks. In 18th Euromicro International Conference on Parallel, Distributed and Network-Based Computing (PDP'10), February 2010.

Digital Library

[19]

F. Verbeek. A fast and verified algorithm for proving store-and-forward networks deadlock-free. In Proceedings of the 19th International Euromicro Conference on Parallel, Distributed and Network-based Processing (PDP), 2011.

Digital Library

[20]

F. Verbeek and J. Schmaltz. A comment on "a necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks". IEEE Transactions on Parallel and Distributed Systems, 99(PrePrints), 2011.

Digital Library

[21]

F. Verbeek and J. Schmaltz. On necessary and sufficient conditions for deadlock-free routing in wormhole networks. IEEE Transactions on Parallel and Distributed Systems, 99(PrePrints), 2011.

Digital Library

Cited By

Taylor LZhang Z(2022)Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_19(378-399)Online publication date: 14-Jan-2022
https://doi.org/10.1007/978-3-030-94583-1_19
Eltaras TFornaciari WZoni D(2019)Partial Packet Forwarding to Improve Performance in Fully Adaptive Routing for Cache-Coherent NoCs2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)10.1109/EMPDP.2019.8671582(33-40)Online publication date: Feb-2019
https://doi.org/10.1109/EMPDP.2019.8671582
Sheng Ma Zhiying Wang Enright Jerger NLi Shen Nong Xiao (2014)Novel Flow Control for Fully Adaptive Routing in Cache-Coherent NoCsIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2013.16625:9(2397-2407)Online publication date: Sep-2014
https://doi.org/10.1109/TPDS.2013.166
Show More Cited By

Index Terms

Automatic verification for deadlock in Networks-on-Chips with adaptive routing and wormhole switching
1. Networks
  1. Network protocols
    1. Network layer protocols
      1. Routing protocols

Recommendations

A Comparison of Router Architectures for Virtual Cut-Through and Wormhole Switching in a NOW Environment

Most multicomputer interconnection networks use wormhole switching, leading to fast and compact routers. Current routers incorporate virtual channels and even fully adaptive routing. Networks of workstations (NOWs) inherited multicomputer technology. ...
A Theory of Deadlock-Free Adaptive Multicast Routing in Wormhole Networks

A theory for the design of deadlock-free adaptive routing algorithms for wormhole networks was proposed in [12], [16]. This theory supplies the sufficient conditions for an adaptive routing algorithm to be deadlock-free, even when there are cyclic ...
An Efficient Adaptive Deadlock-Free Routing Algorithm for Torus Networks

A deadlock-free minimal routing algorithm called clue is first proposed for VCT (virtual cut-through)-switched tori. Only two virtual channels are required. One channel is applied in the deadlock-free routing algorithm for the mesh subnetwork based on a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

NOCS '11: Proceedings of the Fifth ACM/IEEE International Symposium on Networks-on-Chip

May 2011

282 pages

ISBN:9781450307208

DOI:10.1145/1999946

General Chairs:
Radu Marculescu
CMU
,
Mike Kishinevsky
Intel
,
Program Chairs:
Ran Ginosar
Technion, Israel
,
Karam S. Chatha
Arizona State University

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Nederlandse Organisatie voor Wetenschappelijk Onderzoek

Conference

NOCS'11

Sponsor:

NOCS'11: International Symposium on Networks-on-Chips

May 1 - 4, 2011

Pennsylvania, Pittsburgh

Acceptance Rates

Overall Acceptance Rate 14 of 44 submissions, 32%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
140
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Taylor LZhang Z(2022)Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_19(378-399)Online publication date: 14-Jan-2022
https://doi.org/10.1007/978-3-030-94583-1_19
Eltaras TFornaciari WZoni D(2019)Partial Packet Forwarding to Improve Performance in Fully Adaptive Routing for Cache-Coherent NoCs2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)10.1109/EMPDP.2019.8671582(33-40)Online publication date: Feb-2019
https://doi.org/10.1109/EMPDP.2019.8671582
Sheng Ma Zhiying Wang Enright Jerger NLi Shen Nong Xiao (2014)Novel Flow Control for Fully Adaptive Routing in Cache-Coherent NoCsIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2013.16625:9(2397-2407)Online publication date: Sep-2014
https://doi.org/10.1109/TPDS.2013.166
Verbeek FSchmaltz J(2014)A Decision Procedure for Deadlock-Free Routing in Wormhole NetworksIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2013.12125:8(1935-1944)Online publication date: Aug-2014
https://doi.org/10.1109/TPDS.2013.121
Alhussien ABagherzadeh NVerbeek Fvan Gastel BSchmaltz J(2012)A formally verified deadlock-free routing function in a fault-tolerant NoC architecture2012 25th Symposium on Integrated Circuits and Systems Design (SBCCI)10.1109/SBCCI.2012.6344433(1-6)Online publication date: Aug-2012
https://doi.org/10.1109/SBCCI.2012.6344433
Verbeek FSchmaltz J(2011)Formal verification of a deadlock detection algorithmElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.70.870(103-112)Online publication date: 20-Oct-2011
https://doi.org/10.4204/EPTCS.70.8

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents