模型检测MESIF Cache一致性协议

• 作者: 吕正 吕毅 陈峰 陈昊
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 模型检测 Cache 一致性协议 形式验证
• 年，卷（期）: 2010,（17）
• 所属期刊栏目: 研发、设计、测试
• 页码范围: 66-68,152
• 分类号: TP311
• 字数: 5405字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2010.17.019

摘要

在处理器从单核向多核演进的过程中,为了获得更好的性能和可扩展性,适用于多核处理器系统的Cache一致性协议变得越来越复杂.Cache一致性协议的验证一直是模型检测在工业界主要应用之一,被工业界和学术界关注.相对传统方法而言,微结构级的模型检测能够描述和验证更多的协议细节.利用NuSMV工具对Intel公司的MESIF Cache一致性协议进行模型检测在微结构层次上进行了建模,并对该协议进行模型检测,试验结果证明了此方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈峰	西北大学信息科学与技术学院	83	358	12.0	16.0
2	陈昊	西北大学信息科学与技术学院	9	29	3.0	4.0
4	吕毅	中国科学院软件研究所	11	158	4.0	11.0
7	吕正	西北大学信息科学与技术学院	6	19	3.0	4.0