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

吕正 1; 陈昊 2; 1; 陈峰 1

doi:10.7652/xjtuxb201306012

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-05-01

- 一种ARM存储模型的快速检测方法
- A Novel Validation Method for ARM Memory Model
- 西安交通大学学报 2013年47卷第6期页码：68-72
- 作者机构：
  
  西北大学信息科学与技术学院,西安,710069
- 作者简介：
- 基金信息：
  
  : 2012-12-02。作者简介: 吕正(1977—),男,博士生。基金项目: 国家“863计划”资助项目(2007AA01Z147)
- DOI：10.7652/xjtuxb201306012
  中图分类号： TP311
- 网络首发：2013-06-10，
  
  纸质出版：2013
- 稿件说明：
移动端阅览
吕正 1, 陈昊 2, 1, 等. 一种ARM存储模型的快速检测方法[J]. 西安交通大学学报, 2013,47(6):68-72.

A Novel Validation Method for ARM Memory Model[J]. 2013, 47(6): 68-72.
吕正 1, 陈昊 2, 1, 等. 一种ARM存储模型的快速检测方法[J]. 西安交通大学学报, 2013,47(6):68-72. DOI： 10.7652/xjtuxb201306012.

A Novel Validation Method for ARM Memory Model[J]. 2013, 47(6): 68-72. DOI： 10.7652/xjtuxb201306012.

摘要

针对ARM多核处理器存储模型正确性的快速检测问题

提出了一种利用时间序和悬空窗口的有界特性的快速检测方法

并实现了检测工具。该方法给出了ARM存储模型基于barrier的弱一致性模型的公理语义

通过定期扫描处理器的性能计数器获得访存指令操作间的时间约束关系。检测工具由随机指令发生模块、多核处理器性能计数器记录模块和结果分析模块3部分组成

它的低算法时间复杂度特性使其能够有效处理上百万行ARM访存指令程序。检测工具使用C++语言实现

可以在运行时动态调整指令流的长度参数

具有很好的扩展性。利用支持ARM MPCore的模拟器进行了实验

并用手工的方法在指令流执行序列中注入了几个错误

以验证程序结果是否违反ARM存储模型。实验结果表明

检测工具能够正确发现上述注入错误

检测方法和检测工具可以有效检测ARM多核处理器存储模型的正确性。

Abstract

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.

关键词

Keywords

references

ARM. ARM architectural reference manual [M]. Cambridge, UK: ARM, 2008.

COLLIER W W. Reasoning about parallel architectures [M]. Upper Saddle River, NJ, USA: Prentice-Hall, 1992.

Compaq Computer Corp. Alpha architecture handbook [M/OL].(1998-10-04)[2012-04-01]. http:∥www.cs.cmu.edu/afs/cs/academic/class/15347-s98/public/doc/alpha-ref.pdf.

Intel Corporation. Intel 64 architecture memory ordering white paper [R]. San Francisco, CA, USA: Intel Corporation, 2007.

HANGAL S, VAHIA D, MANOVIT C, et al. TSOtool: a program for verifying memory systems using the memory consistency model [J]. SIGARCH Computer Architecture News, 2004, 32(2): 114-123.

MANOVIT C, HANGAL S. Efficient algorithms for verifying memory consistency [C]∥Proceedings of the 17th Annual ACM Symposium on Parallelism in Algorithms and Architectures. New York, USA: ACM Press, 2005: 245-252.

ROY A, ZEISSET S, FLECKENSTEIN C, et al. Fast and generalized polynomial time memory consistency verification [C]∥Proceedings of the International Conference on Computer Aided Verification. Berlin, Germany: Springer, 2006: 503-516.

MANOVIT C, HANGAL S. Completely verifying memory consistency of test program executions [C]∥Proceedings of the 12th International Symposium on High-Performance Computer Architecture. Washington DC, USA: IEEE Computer Society Press, 2006: 166-175.

CHEN Yunji, LV Yi, HU Weiwu, et al. Fast complete memory consistency verification [C]∥Proceedings of the 15th International Symposium on High-Performance Computer Architecture. Washington DC, USA: IEEE Computer Society Press, 2009: 381-392.

王朋宇, 陈云霁, 沈海华, 等. 片上多核处理器存储一致性验证 [J]. 软件学报, 2010, 21(4): 863-874.

WANG Pengyu, CHEN Yunji, SHEN Haihua, et al. Memory consistency verification of chip multi-processor [J]. Journal of Software, 2010, 21(4): 863-874.

LV Zheng, CHEN Hao, CHEN Feng, et al. Fast verification of memory consistency for chip multi-processor [C]∥Proceedings of the Seventh International Conference on Computational Intelligence and Security. Washington DC, USA: IEEE Computer Society, 2011: 1497-1502.

吕正, 陈昊, 陈峰, 等. MOTEC: 一个存储一致性模型验证工具 [J]. 计算机工程, 2012, 38(11): 242-246.

LV Zheng, CHEN Hao, CHEN Feng, et al. MOTEC: a tool for quick verification of memory consistency model [J]. Computer Engineering, 2012, 38(11): 242-246.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

ARM处理器分支预测漏洞分析测评及新漏洞发现

EBSILON软件在热电联产系统优化中的应用综述

融合物理信息与深度算子网络的变压器绕组热-流场快速计算方法

采用试验设计方法的第三代CO2气体箔轴承箔片几何参数敏感性分析

混合电解槽阵列协同的风光耦合制氢系统双层多目标优化