In a cache-coherent shared-memory multiprocessor system, data consistency among cached copies can be delayed until synchronization points under relaxed memory consistency models. Some protocols, called 'delayed consistency protocols', take advantage of this flexibility to reduce cache miss rates and memory traffic. However, they are very complex, and validating their correctness, even at the behavioral level, is a challenge. We have successfully applied a new verification tool to verify the delayed consistency protocol at the behavioral level. The method is called SSM (Symbolic State Model). The contribution of this paper, besides verifying the protocol, is to demonstrate how to deal with relaxed memory models and latency tolerance hardware in the context of SSM.
展开▼
