Modeling a Cache Coherence Protocol with the Guarded Action Language

Quentin L. Meunier
(Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6)
Yann Thierry-Mieg
(Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6)
Emmanuelle Encrenaz
(Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6)

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.

In John P. Gallagher, Rob van Glabbeek and Wendelin Serwe: Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece, 20th April 2018, Electronic Proceedings in Theoretical Computer Science 268, pp. 88–103.
Published: 23rd March 2018.

ArXived at: https://dx.doi.org/10.4204/EPTCS.268.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org