Abstract:Regarding the state space explosion problem in model checking Cache coherence protocol, the concept of pseudo-cutoff, a limit of the nodes which share the same memory block, is put forward in this paper. Based on the analysis of the inherent characteristics of parallel programs, the pseudo-cutoff value in relaxed consistency Cache coherent non-uniform memory access system under certain conditions is deduced. The state space of the directory-based Cache protocol is optimized effectively using pseudo-cutoff, and a new scheme to small probability matter of wide sharing is presented. Experimental results show that, the method of protocol model optimization based on pseudo-cutoff can effectively reduce the state space of Cache protocol, accelerate verification speed and improve the capability of verifying large scale Cache protocol.