| 一种ARM存储模型的快速检测方法 |
| |
| 引用本文： | 吕正,陈昊,陈峰. 一种ARM存储模型的快速检测方法[J]. 西安交通大学学报, 2013, 47(6) |
| |
| 作者姓名： | 吕正 陈昊 陈峰 |
| |
| 作者单位： | 1. 西北大学信息科学与技术学院,710069,西安
2. 中国劳动关系学院关系学院,100048,北京;西北大学信息科学与技术学院,710069,西安 |
| |
| 基金项目： | 国家"863计划"资助项目 |
| |
| 摘 要： | 针对ARM多核处理器存储模型正确性的快速检测问题,提出了一种利用时间序和悬空窗口的有界特性的快速检测方法,并实现了检测工具.该方法给出了ARM存储模型基于barrier的弱一致性模型的公理语义,通过定期扫描处理器的性能计数器获得访存指令操作间的时间约束关系.检测工具由随机指令发生模块、多核处理器性能计数器记录模块和结果分析模块3部分组成,它的低算法时间复杂度特性使其能够有效处理上百万行ARM访存指令程序.检测工具使用C++语言实现,可以在运行时动态调整指令流的长度参数,具有很好的扩展性.利用支持ARMMPCore的模拟器进行了实验,并用手工的方法在指令流执行序列中注入了几个错误,以验证程序结果是否违反ARM存储模型.实验结果表明,检测工具能够正确发现上述注入错误,检测方法和检测工具可以有效检测ARM多核处理器存储模型的正确性.
|
| 关 键 词： | ARM处理器 存储模型 正确性检测 |
A Novel Validation Method for ARM Memory Model |
| |
| L Zheng , CHEN Hao , CHEN Feng. A Novel Validation Method for ARM Memory Model[J]. Journal of Xi'an Jiaotong University, 2013, 47(6) |
| |
| Authors: | L Zheng CHEN Hao CHEN Feng |
| |
| Affiliation: | L(U) Zheng , CHEN Hao , CHEN Feng |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
