Modeling and verification of cache coherence protocols

Author

Ivanov, Lubomir ; Nunna, Ramakrishna

Author_Institution

Dept. of Comput. Sci., Iona Coll., New Rochelle, NY, USA

Volume

5

fYear

2001

fDate

2001

Firstpage

129

Abstract

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

Keywords

cache storage; formal verification; memory protocols; MESI protocol; cache coherence protocols; cache controllers; modeling methodology; series-parallel poset modeling/verification; verification methodology; Cache memory; Circuit faults; Coherence; Control systems; Formal verification; Hardware; Mathematical model; Polynomials; Power system modeling; Protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2001. ISCAS 2001. The 2001 IEEE International Symposium on

Conference_Location

Sydney, NSW

Print_ISBN

0-7803-6685-9

Type

conf

DOI

10.1109/ISCAS.2001.922002

Filename

922002