Tera-Scale ARchitecture (TSAR)
| Description: | Model of the hardware Tera-Scale ARchitecture (TSAR), focusing on its Distributed Hybrid Cache Coherence Protocol (DHCCP) |
| Author(s): | Quentin L. Meunier, Yann Thierry-Mieg, Emmanuelle Encrenaz |
| Event(s): | MARS'18 |
| Paper(s): |
A Modeling a Cache Coherence Protocol with the Guarded Action Language |
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.
Model(s)
-
- Download Model
- Browse Model
- tool(s): Promela (Spin)
-
- Download Model
- Browse Model
- tool(s): ITS-tools
This work is licensed under a Creative Commons
Attribution-NonCommercial-ShareAlike 4.0 International License.