Modeling a Cache Coherence Protocol with the Guarded Action Language
Quentin L. Meunier (Sorbonne Universit\'e, CNRS, Laboratoire, d'Informatique de Paris 6), Yann Thierry-Mieg (Sorbonne Universit\'e, CNRS,, Laboratoire d'Informatique de Paris 6), Emmanuelle Encrenaz (Sorbonne, Universit\'e, CNRS, Laboratoire d'Informatique de Paris 6)
TL;DR
This paper develops a formal model of the TSAR's Distributed Hybrid Cache Coherence Protocol using the Guarded Action Language to verify properties like deadlock freedom and fairness in a complex asynchronous distributed system.
Contribution
It introduces a formal verification approach for a complex cache coherence protocol using the Guarded Action Language, addressing challenges in asynchronous distributed hardware validation.
Findings
Proved absence of deadlocks in the protocol
Established eventual consensus and fairness properties
Demonstrated effectiveness of formal methods for hardware protocol verification
Abstract
We present a formal model built for verification of the hardware Tera-Scale ARchitecture (TSAR), focusing on its Distributed Hybrid Cache Coherence Protocol (DHCCP). This protocol is by nature asynchronous, concurrent and distributed, which makes classical validation of the design (e.g. through testing) difficult. We therefore applied formal methods to prove essential properties of the protocol, such as absence of deadlocks, eventual consensus, and fairness.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.