【摘要】针对ARM多核处理器存储模型正确性的快速检测问题,提出了一种利用时间序和悬空窗口的有界特性的快速检测方法,并实现了检测工具。该方法给出了ARM存储模型基于barrier的弱一致性模型的公理语义,通过定期扫描处理器的性能计数器获得访存指令操作间的时间约束关系。检测工具由随机指令发生模块、多核处理器性能计数器记录模块和结果分析模块3部分组成,它的低算法时间复杂度特性使其能够有效处理上百万行ARM访存指令程序。检测工具使用C＋＋语言实现,可以在运行时动态调整指令流的长度参数,具有很好的扩展性。利用支持ARMMPCore的模拟器进行了实验,并用手工的方法在指令流执行序列中注入了几个错误,以验证程序结果是否违反ARM存储模型。实验结果表明,检测工具能够正确发现上述注入错误,检测方法和检测工具可以有效检测ARM多核处理器存储模型的正确性。