Rapid parameterized model checking of snoopy cache coherence protocols

20Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

A new method is proposed for parameterized reasoning about snoopy cache coherence protocols. The method is distinctive for being exact (sound and complete), fully automatic (algorithmic), and tractably efficient. The states of most cache coherence protocols can be organized into a hierarchy reflecting how tightly a memory block in a given cache state is bound to the processor. A broad framework encompassing snoopy cache coherence protocols is proposed where the hierarchy implicit in the design of protocols is captured as a pre-order. This yields a new solution technique that hinges on the construction of an abstract history graph where a global concrete state is represented by an abstract state reflecting the occupied local states. The abstract graph also takes into account the history of local transitions of the protocol that were fired along the computation to get to the global state. This permits the abstract history graph to exactly capture the behaviour of systems with an arbitrary number of homogeneous processes. Although the worst case size of the abstract history graph can be exponential in the size of the transition diagram describing the protocol, the actual size of the abstract history graph is small for standard cache protocols. The method is applicable to all 8 of the most common snoopy cache protocols described in Handy's book [19] from Illinois-MESI to Dragon. The experimental results for parameterized verification of each of those 8 protocols document the efficiency of this new method in practice, with each protocol being verified in just a fraction of a second. It is emphasized that this is parameterized verification. © Springer-Verlag Berlin Heidelberg 2003.

Cite

CITATION STYLE

APA

Emerson, E. A., & Kahlon, V. (2003). Rapid parameterized model checking of snoopy cache coherence protocols. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2619, 144–159. https://doi.org/10.1007/3-540-36577-x_11

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free