Model Checking Data Consistency for Cache Coherence Protocols

A method for automatic verification of cache coherence protocols ispresented, in which cache coherence protocols are modeled asconcurrent value-passing processes, and control and data consistencyrequirement are described as formulas in first-order \mu-calculus.A model checker is employed to check if the protocol underinvestigation satisfies the required properties. Using this method adata consistency error has been revealed in a well-known cachecoherence protocol. The error has been corrected, and the revisedprotocol has been shown free from data consistency error for anydata domain size, by appealing to data independence technique.