Verification of the Futurebus+ Cache Coherence protocol: A case study in model checking

This paper presents a case study for automatic verification using the Communicating Sequential Processes formalism. The case study concerns the Futurebus+ cache coherency standard; we develop a formal model of the protocol and perform some verification tasks upon it. In the process of doing so, we extend the previous solution by developing a formal specification of cache coherence that is suitable for the verification of both directory and snooping based cache coherence protocols.

• Type: Conference
• Year: 2004
• Where: ACSC
• Authors: Kylie Williams, Robert Esser
• Keywords: ACSC 2004, Cache Coherence, Cache Coherency Standard, Case Study, Theoretical Computer Science