一种ARM存储模型的快速检测方法  

A Novel Validation Method for ARM Memory Model

作　　者：吕正[1] 陈昊[2,1] 陈峰[1] 

机构地区：[1]西北大学信息科学与技术学院,西安710069 [2]中国劳动关系学院高职学院,北京100048

出　　处：《西安交通大学学报》2013年第6期68-72,共5页Journal of Xi'an Jiaotong University

基　　金：国家"863计划"资助项目(2007AA01Z147)

摘　　要：针对ARM多核处理器存储模型正确性的快速检测问题,提出了一种利用时间序和悬空窗口的有界特性的快速检测方法,并实现了检测工具。该方法给出了ARM存储模型基于barrier的弱一致性模型的公理语义,通过定期扫描处理器的性能计数器获得访存指令操作间的时间约束关系。检测工具由随机指令发生模块、多核处理器性能计数器记录模块和结果分析模块3部分组成,它的低算法时间复杂度特性使其能够有效处理上百万行ARM访存指令程序。检测工具使用C++语言实现,可以在运行时动态调整指令流的长度参数,具有很好的扩展性。利用支持ARMMPCore的模拟器进行了实验,并用手工的方法在指令流执行序列中注入了几个错误,以验证程序结果是否违反ARM存储模型。实验结果表明,检测工具能够正确发现上述注入错误,检测方法和检测工具可以有效检测ARM多核处理器存储模型的正确性。A low time complexity method for checking the correctness of ARM memory model is proposed by identifying the pending windows of microprocessor and introducing the restrictions of time order,and a validation tool is presented.The ARM memory model is explored and the formal definition of the model is given in the method.The time order constraints are obtained by scanning the performance counters of the ARM memory system periodically.The validation tool consists of three parts,namely,a random instruction generation module,a performance counter recording module and a results analysis module.The tool can effectively handle millions of lines of ARM multicore program because of the low time complexity of the algorithm.The validation tool is written in C＋＋,and the length of the access memory instructions can be adjusted dynamically in run-time,which supports high extendability.Experiments with several infected errors in an ARM MPCore simulator show that the validation tool can detect these errors correctly,and that the proposed validation method and tool can effectively verify the ARM memory model.

关 键 词：ARM处理器 存储模型 正确性检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]