MOTEC:一个存储一致性模型验证工具
MOTEC:A Validation Tool for Memory Consistency Model作者机构:西北大学信息科学与技术学院西安710069 中国科学院软件研究所北京100190 中国劳动关系学院北京100048
出 版 物:《计算机工程》 (Computer Engineering)
年 卷 期:2012年第38卷第11期
页 面:242-246页
核心收录:
学科分类:08[工学] 0812[工学-计算机科学与技术(可授工学、理学学位)] 081202[工学-计算机软件与理论]
基 金:国家"863"计划基金资助项目(2007AA01Z147)
主 题:多核处理器 存储一致性模型 形式验证 动态验证 存储系统 验证工具
摘 要:由于缺乏可利用的额外观察条件,在芯片流片后阶段进行存储一致性模型验证较困难。为此,利用多核处理器系统中通用的性能计数器,通过定期扫描性能计数器以获得关键活动访存指令集合的信息,实现MOTEC工具。该工具由MOTEC随机指令发生模块、多核处理器性能计数器记录模块和MOTEC分析模块3个部分组成。对其核心算法的分析结果表明,MOTEC的时间复杂度仅为O(p 3n),在目前流片后阶段进行验证的工具中时间复杂度最低。