|
|||||
|
|
| MOTEC: 一个存储一致性模型验证工具 | |
| 引用本文： | 吕正,陈昊,陈峰,吕毅. MOTEC: 一个存储一致性模型验证工具[J]. 计算机工程, 2012, 38(11): 242-246 |
| 作者姓名： | 吕正 陈昊 陈峰 吕毅 |
| 作者单位： | 1. 西北大学信息科学与技术学院,西安710069;中国科学院软件研究所,北京100190 2. 西北大学信息科学与技术学院,西安710069;中国劳动关系学院,北京100048 3. 西北大学信息科学与技术学院,西安,710069 4. 中国科学院软件研究所,北京,100190 |
| 基金项目： | 国家"863"计划基金资助项目 |
| 摘 要： | 由于缺乏可利用的额外观察条件，在芯片流片后阶段进行存储一致性模型验证较困难。为此，利用多核处理器系统中通用的性能计数器，通过定期扫描性能计数器以获得关键活动访存指令集合的信息，实现MOTEC工具。该工具由MOTEC随机指令发生模块、多核处理器性能计数器记录模块和MOTEC分析模块3个部分组成。对其核心算法的分析结果表明，MOTEC的时间复杂度仅为 ，在目前流片后阶段进行验证的工具中时间复杂度最低。 |
| 关 键 词： | 多核处理器 存储一致性模型 形式验证 动态验证 存储系统 验证工具 |
| 收稿时间： | 2011-11-03 |
MOTEC: A Validation Tool for Memory Consistency Model |
|
| LV Zheng , CHEN Hao , CHEN Feng , LV Yi. MOTEC: A Validation Tool for Memory Consistency Model[J]. Computer Engineering, 2012, 38(11): 242-246 | |
| Authors: | LV Zheng CHEN Hao CHEN Feng LV Yi |
| Affiliation: | 1.School of Information Science and Technology,Northwest University,Xi’an 710069,China;2.Institute of Software,Chinese Academy of Sciences,Beijing 100190,China;3.China Institute of Industrial Relations,Beijing 100048,China) |
| Abstract: | For the purpose of verification of the memory consistency model after tapeout stage,this paper proposes a low time complexity algorithm by exploring the key time order information which is implicitly derived based on the values of performance counters being scanned periodically.The MOTEC tool which implements this algorithm is general enough to support many multicore processor systems with trivial modifications.The complexity analysis shows that the time complexity of MOTEC is only,thus MOTEC can verify the multicore program of millions of lines. |
| Keywords: | multicore processor memory consistency model formal verification dynamic validation memory system validation tool |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机工程》浏览原始摘要信息 | |
| 点击此处可从《计算机工程》下载免费的PDF全文 | |