基于伪临界值的Cache一致性协议验证方法

An Efficient Verification Method of Cache Coherence Protocol Based on Pseudo-cutoff

针对Cache一致性协议状态空间爆炸问题,提出共享集合伪临界值(Pseudo-cutoff)的概念,并以采用释放一致性模型的CC-NUMA系统为例,分析了共享数据的分布情况,推导出在一定条件下共享集合伪临界值为4的结论,有效优化了目录Cache协议状态空间,并提出了解决小概率的宽共享事件的方法。实验数据表明,基于伪临界值的协议模型优化,能够有效缩小Cache协议状态空间,加快验证速度,扩大验证规模。

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-cuteff 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-cuteff can effectively reduce the state space of Cache protocol, accelerate verification speed and improve the capability of verifying large scale Cache protocol.