A Novel Validation Method for ARM Memory Model

doi:10.7652/xjtuxb201306012

您当前的位置：

首页 >

文章列表页 >

A Novel Validation Method for ARM Memory Model

更新时间：2025-05-01

- A Novel Validation Method for ARM Memory Model
- Vol. 47, Issue 6, Pages: 68-72(2013)
- 作者机构：
  
  西北大学信息科学与技术学院,西安,710069
- 作者简介：
- 基金信息：
- DOI：10.7652/xjtuxb201306012
  CLC： TP311
- Online First：10 June 2013，
  
  Published：2013
- 稿件说明：
移动端阅览
A Novel Validation Method for ARM Memory Model[J]. 2013, 47(6): 68-72.
DOI：

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.

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Evaluation of Branch Prediction Vulnerability and New Vulnerability Discovery on ARM Processors

Sensitivity Analysis of Foil Geometrical Parameters for the Third-Generation CO2 Gas Foil Bearings Based on Design of Experiments Method

Integrated and Joint Design Optimization of Centrifugal Compressor Impeller and Casing Treatment at Multiple Working Points

Review of the Application of EBSILON Software in Combined Heat and Power System Optimization

Study on the Thermodynamic Properties in the Anomalous Region of Supercritical Water

Related Author

王春露

田瑞冬

赵旭

吕勇强

汪东升

Related Institution

Ministry of Education Key Laboratory of Trustworthy Distributed Computing and Service, Beijing University of Posts and Telecommunications

⁰