Deadlock Verification of Cache Coherence Protocols and Communication Fabrics
| Autor: | Freek Verbeek, Pooria M. Yaghini, Ashkan Eghbal, Nader Bagherzadeh |
|---|---|
| Přispěvatelé: | RS-Research Line Resilience (part of LIRS program), Department Computer Science |
| Rok vydání: | 2017 |
| Předmět: |
Computer science
Distributed computing 0211 other engineering and technologies 02 engineering and technology Network topology Synchronization Theoretical Computer Science deadlock freedom Synchronization (computer science) 0202 electrical engineering electronic engineering information engineering communication networks Cache coherence formal verification Formal verification 021106 design practice & management business.industry Network packet Deadlock Formal methods 020202 computer hardware & architecture Computational Theory and Mathematics Hardware and Architecture Scalability Digital Security business Software Computer network |
| Zdroj: | Verbeek, F, Yaghini, P M, Eghbal, A & Bagherzadeh, N 2017, ' Deadlock Verification of Cache Coherence Protocols and Communication Fabrics ', Ieee Transactions on Computers, vol. 66, no. 2, pp. 272-284 . https://doi.org/10.1109/TC.2016.2584060 IEEE Transactions on Computers, 66, 2, pp. 272-284 IEEE Transactions on Computers, 66, 272-284 Ieee Transactions on Computers, 66(2), 272-284. IEEE COMPUTER SOC |
| ISSN: | 0018-9340 |
| DOI: | 10.1109/TC.2016.2584060 |
| Popis: | Cache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emerging property. Formal methods often decouple verification of the protocol from verification of the communication interconnect. Modern communication fabrics, however, become more advanced and include a network topology, routing, arbitration, synchronization, and more. In this paper, an integrated approach is proposed that allows cross-layer verification of both the cache coherence protocol and the communication fabric all at once. An automated methodology for deriving cross-layer invariants is proposed. These invariants relate the state of the application-layer protocols to en route packets in the communication fabric. Using the invariants, we derive formal proofs of deadlock-freedom for two case studies: a directory-based MI protocol in a 2D mesh, and a ring-based snoopy protocol in a 2D torus. Additionally, we show that our methodology can be used to derive the smallest possible queue sizes that ensure absence of deadlocks. Our methodology is generally applicable and shows promising scalability. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|