Sciweavers

55
Voted
CHARME
2003
Springer

Exact and Efficient Verification of Parameterized Cache Coherence Protocols

14 years 3 months ago
Exact and Efficient Verification of Parameterized Cache Coherence Protocols
Abstract. We propose new, tractably (in some cases provably) efficient algorithmic methods for exact (sound and complete) parameterized reasoning about cache coherence protocols. For reasoning about general snoopy cache protocols, duce the guarded broadcast protocols model and show how an abstract history graph construction can be used to reason about safety properties for this framework. Although the worst case size of the abstract history graph can be exponential in the size of the transition diagram of the given protocol, the actual size is small for standard cache protocols as is evidenced by our experimental results. The framework can handle all 8 of the cache protocols in [19] as well as their split-transaction versions. We next identify a framework called initialized broadcast protocols suitable for reasoning about invalidation-based snoopy cache protocols and show how to reduce reasoning about such systems with an arbitrary number of caches to a system with at most 7 caches. Th...
E. Allen Emerson, Vineet Kahlon
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Where CHARME
Authors E. Allen Emerson, Vineet Kahlon
Comments (0)