| 基于伪临界值的Cache一致性协议验证方法 |
| |
| 引用本文： | 屈婉霞,郭阳,庞征斌,杨晓东. 基于伪临界值的Cache一致性协议验证方法[J]. 国防科技大学学报, 2008, 30(6): 47-52 |
| |
| 作者姓名： | 屈婉霞 郭阳 庞征斌 杨晓东 |
| |
| 作者单位： | 国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金资助项目 ， 新世纪优秀人才支持计划资助项目 |
| |
| 摘 要： | 针对Cache一致性协议状态空间爆炸问题,提出共享集合伪临界值(Pseudo-cutoff)的概念,并以采用释放一致性模型的CC-NUMA系统为例,分析了共享数据的分布情况,推导出在一定条件下共享集合伪临界值为4的结论,有效优化了目录Cache协议状态空间,并提出了解决小概率的宽共享事件的方法.实验数据表明,基于伪临界值的协议模型优化,能够有效缩小Cache协议状态空间,加快验证速度,扩大验证规模.
|
| 关 键 词： | 形式化验证 模型检验 多处理机系统 Cache一致性协议 |
| 收稿时间： | 2008-08-26 |
An Efficient Verification Method of Cache Coherence Protocol Based on Pseudo-cutoff |
| |
| QU Wanxi,GUO Yang,PANG Zhengbin and YANG Xiaodong. 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 |
| |
| Authors: | QU Wanxi GUO Yang PANG Zhengbin YANG Xiaodong |
| |
| Affiliation: | QU Wan-xia,GUO Yang,PANG Zheng-bin,YANG Xiao-dong(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 n... |
| |
| Keywords: | formal verification model checking multiprocessor Cache coherence protocol |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|
