Efficient Verification of Parameterized Cache Coherence Protocols

To address the state explosion problem of parameterized directory based cache protocol in model checking, we put forward the concept of pseudo-cutoff, a bound of the number of nodes which share the same memory block in this paper. Based on the analysis on inherent characteristics of parallel programs, we deduce the pseudo-cutoff value in relaxed consistency Cache-coherent non-uniform memory architecture (CC-NUMA) system under certain conditions. We optimize the state space of parameterized directory-based cache protocol effectively using pseudo-cutoff, and present a new scheme to small probability matter of wide sharing. Experiment results including different system scales show that, the method of protocol model optimization based on pseudo-cutoff could effectively reduce the state space of parameterized cache protocol, accelerates verification speed and improves the capability of verifying large scale Cache protocol.