| 引用本文: | 屈婉霞,郭阳,庞征斌,等.基于伪临界值的Cache一致性协议验证方法.[J].国防科技大学学报,2008,30(6):47-52.[点击复制] |
| QU Wanxia,GUO Yang,PANG Zhengbin,et al.An Efficient Verification Method of Cache Coherence Protocol Based on Pseudo-cutoff[J].Journal of National University of Defense Technology,2008,30(6):47-52[点击复制] |
|
| |
|
|
| 本文已被：浏览 7560次 下载 6182次 |
| 基于伪临界值的Cache一致性协议验证方法 |
| 屈婉霞, 郭阳, 庞征斌, 杨晓东 |
|
(国防科技大学 计算机学院，湖南 长沙 410073)
|
| 摘要: |
| 针对Cache一致性协议状态空间爆炸问题，提出共享集合伪临界值(Pseudo-cutoff)的概念，并以采用释放一致性模型的CC-NUMA系统为例，分析了共享数据的分布情况，推导出在一定条件下共享集合伪临界值为4的结论，有效优化了目录Cache协议状态空间，并提出了解决小概率的宽共享事件的方法。实验数据表明，基于伪临界值的协议模型优化，能够有效缩小Cache协议状态空间，加快验证速度，扩大验证规模。 |
| 关键词: 形式化验证 模型检验 多处理机系统 Cache一致性协议 |
| DOI： |
| 投稿日期：2008-08-26 |
| 基金项目:国家自然科学基金资助项目(60573173，60773025)；新世纪优秀人才支持计划资助项目 |
|
| An Efficient Verification Method of Cache Coherence Protocol Based on Pseudo-cutoff |
| QU Wanxia, GUO Yang, PANG Zhengbin, YANG Xiaodong |
|
(College of Computer, National Univ. of Defense Technology, Changsha 410073, China)
|
| 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. |
| Keywords: formal verification model checking multiprocessor Cache coherence protocol |
|
|
|
|
|
