Application of Esterel for modelling and verification of Cachet protocol on CRF memory model

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