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

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

作　　者：屈婉霞[1] 郭阳[1] 庞征斌[1] 杨晓东[1] 

机构地区：[1]国防科技大学计算机学院,湖南长沙410073

出　　处：《国防科技大学学报》2008年第6期47-52,共6页Journal of National University of Defense Technology

基　　金：国家自然科学基金资助项目(60573173;60773025);新世纪优秀人才支持计划资助项目

摘　　要：针对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.

关 键 词：形式化验证 模型检验 多处理机系统 CACHE一致性协议 

分 类 号：TP302.1[自动化与计算机技术—计算机系统结构]