Modeling and verification of cache coherence protocols

A cache coherence protocol is a set of rules, which cache controllers in a system with multiple cache memories must follow to maintain the consistency of data stored in the local cache memories as well as in main memory. MESI is a popular cache coherence protocol used to synchronize the operation of cache controllers in many Shared Memory MIMD systems. MESI is also used to maintain the consistency between the level-1 and level-2 caches of the Intel Pentium(R) microprocessor. In this paper we present a model of the MESI protocol based on the recently introduced series-parallel poset modeling and verification methodology. We illustrate the use of the new methodology by verifying a few properties of the MESI protocol