| 基于伪临界值的Cache一致性协议验证方法 |
| |
| 作者姓名： | 屈婉霞 郭阳 庞征斌 杨晓东 |
| |
| 作者单位： | 国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金资助项目
,
新世纪优秀人才支持计划资助项目
|
| |
| 摘 要： | 针对Cache一致性协议状态空间爆炸问题,提出共享集合伪临界值(Pseudo-cutoff)的概念,并以采用释放一致性模型的CC-NUMA系统为例,分析了共享数据的分布情况,推导出在一定条件下共享集合伪临界值为4的结论,有效优化了目录Cache协议状态空间,并提出了解决小概率的宽共享事件的方法.实验数据表明,基于伪临界值的协议模型优化,能够有效缩小Cache协议状态空间,加快验证速度,扩大验证规模.
|
| 关 键 词： | 形式化验证 模型检验 多处理机系统 Cache一致性协议 |
| 收稿时间： | 2008-08-26 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载全文 |
|
