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...

• Type: Conference
• Year: 2003
• Where: CHARME
• Authors: E. Allen Emerson, Vineet Kahlon
• Keywords: Cache Protocols, CHARME 2003, Hardware, Snoopy Cache Protocols, Snoopy Protocol