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

• 作者: 屈婉霞 庞征斌 杨晓东 郭阳
• 来源期刊: 国防科技大学学报
• 学科: 工学
• 关键词: 形式化验证 模型检验 多处理机系统 Cache一致性协议
• 年，卷（期）: 2008,（6）
• 所属期刊栏目: 计算机工程·信息工程·应用物理
• 页码范围: 47-52
• 页数: 6页
• 分类号: TP302.1
• 字数: 4707字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2486.2008.06.011

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭阳	国防科技大学计算机学院	50	449	9.0	20.0
2	庞征斌	国防科技大学计算机学院	19	107	5.0	10.0
3	杨晓东	国防科技大学计算机学院	23	82	5.0	8.0
4	屈婉霞	国防科技大学计算机学院	11	25	3.0	4.0