Abstract :
Synchronous languages have been widely used for the reliable design of reactive systems and synchronous circuits as it has become possible to move from the realm of simulations to that of proofs. While ESTEREL has been used for the modelling and verification of reactive systems, it has not been used that widely for the modelling and verification of cache coherency protocols. In this paper, we discuss the use of ESTEREL for the modelling and verification of cache coherence protocols, in particular on the adaptive cache coherence protocols called CACHET built on the Commit-Reconcile and Fences (CRF) distributed shared memory model. In the paper, we (i) first, model the CRF memory model along with the various CACHET micro-protocols in ESTEREL, (ii) verify properties of the CACHET micro-protocols in a graded manner reflecting the protocol design using the synchronous observer method, and (iii) highlight the experiences in overcoming limitations including state-explosion
Keywords :
cache storage; distributed shared memory systems; formal verification; observers; protocols; reachability analysis; CACHET; CRF memory model; Cachet protocol; Commit-Reconcile and Fences; Esterel; micro-protocols; protocol design; state-explosion; synchronous languages; synchronous observer method; Access protocols; Application software; Cache memory; Coherence; Computational modeling; Computer science; Computer simulation; Delay; Read-write memory; Writing;
