MOTEC:一个存储一致性模型验证工具

• 作者: 吕正 吕毅 陈峰 陈昊
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 多核处理器 存储一致性模型 形式验证 动态验证 存储系统 验证工具
• 年，卷（期）: 2012,（11）
• 所属期刊栏目: 开发研究与设计技术
• 页码范围: 242-246
• 分类号: TP311.5
• 字数: 6288字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2012.11.074

摘要

由于缺乏可利用的额外观察条件,在芯片流片后阶段进行存储一致性模型验证较困难.为此,利用多核处理器系统中通用的性能计数器,通过定期扫描性能计数器以获得关键活动访存指令集合的信息,实现MOTEC工具.该工具由MOTEC随机指令发生模块、多核处理器性能计数器记录模块和MOTEC分析模块3个部分组成.对其核心算法的分析结果表明,MOTEC的时间复杂度仅为O(p3n),在目前流片后阶段进行验证的工具中时间复杂度最低.

作者信息

序号	姓名	单位	发文数	被引次数	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