MOTEC: 一个存储一致性模型验证工具

doi:10.3969/j.issn.1000-3428.2012.11.074

计算机工程 ›› 2012, Vol. 38 ›› Issue (11): 242-246. doi: 10.3969/j.issn.1000-3428.2012.11.074

MOTEC: 一个存储一致性模型验证工具

吕正^1,2，陈昊^1,3，陈峰¹，吕毅²

(1. 西北大学信息科学与技术学院，西安 710069；2. 中国科学院软件研究所，北京 100190；3. 中国劳动关系学院，北京 100048)

收稿日期:2011-11-03 出版日期:2012-06-05 发布日期:2012-06-05
作者简介:吕正(1977－)，男，博士研究生，主研方向：计算机软件与理论；陈昊，讲师、博士研究生；陈峰，讲师、博士；吕毅，副研究员、博士
基金资助:
国家“863”计划基金资助项目(2007AA01Z147)

MOTEC: A Validation Tool for Memory Consistency Model

LV Zheng ^1,2, CHEN Hao ^1,3, CHEN Feng ¹, LV Yi ²

(1. School of Information Science and Technology, Northwest University, Xi’an 710069, China; 2. Institute of Software, Chinese Academy of Sciences, Beijing 100190, China; 3. China Institute of Industrial Relations, Beijing 100048, China)

Received:2011-11-03 Online:2012-06-05 Published:2012-06-05

摘要/Abstract

摘要： 由于缺乏可利用的额外观察条件，在芯片流片后阶段进行存储一致性模型验证较困难。为此，利用多核处理器系统中通用的性能计数器，通过定期扫描性能计数器以获得关键活动访存指令集合的信息，实现MOTEC工具。该工具由MOTEC随机指令发生模块、多核处理器性能计数器记录模块和MOTEC分析模块3个部分组成。对其核心算法的分析结果表明，MOTEC的时间复杂度仅为，在目前流片后阶段进行验证的工具中时间复杂度最低。

关键词: 多核处理器, 存储一致性模型, 形式验证, 动态验证, 存储系统, 验证工具

Abstract: For the purpose of verification of the memory consistency model after tapeout stage, this paper proposes a low time complexity algorithm by exploring the key time order information which is implicitly derived based on the values of performance counters being scanned periodically. The MOTEC tool which implements this algorithm is general enough to support many multicore processor systems with trivial modifications. The complexity analysis shows that the time complexity of MOTEC is only , thus MOTEC can verify the multicore program of millions of lines.

Key words: multicore processor, memory consistency model, formal verification, dynamic validation, memory system, validation tool

中图分类号:

TP311.5

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

LV Zheng, CHEN Hao, CHEN Feng, LV Yi. MOTEC: A Validation Tool for Memory Consistency Model[J]. Computer Engineering, 2012, 38(11): 242-246.

http://www.ecice06.com/CN/Y2012/V38/I11/242

参考文献

[1] Leverich J, Arakida H, Solomatnikov A, et al. Comparing Memory Systems for Chip Multiprocessors[C]//Proc. of the 34th Annual International Symposium on Computer Architecture.

San Diego, USA: ACM Press, 2007: 358-368.
[2] Alur R, McMillan K, Peled D. Model-checking of Correctness Conditions for Concurrent Objects[C]//Proc. of the 11th Annual IEEE Symposium on Logic in Computer Science. [S. l.]: IEEE Computer Society, 1996: 219-228.
[3] Ludden J M, Roesner W, Heiling G M, et al. Functional Veri?cation of the POWER4 Microprocessor and POWER4 Multiprocessor Systems[J]. IBM Journal of Research and Development, 2002, 46(1): 53-76.
[4] Hangal S, Vahia D, Manovit C, et al. TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model[C]//Proc. of the 31st Annual International Symposium on Computer Architecture. Los Alamitos, USA: IEEE Computer Society, 2004: 114-123.
[5] Manovit C, Hangal S. Efficient Algorithms for Verifying Memory Consistency[C]//Proc. of the 17th Annual ACM Symposium on Parallelism in Algorithms and Architectures. Las Vegas, USA: ACM Press, 2005: 245-252.
[6] Manovit C, Hangal S. Completely Verifying Memory Consistency of Test Program Executions[C]//Proc. of the 12th International Symposium on High Performance Computer Architecture. [S. l.]: IEEE Computer Society, 2006: 166-175.
[7] Roy A, Zeisset S, Fleckenstein C, et al. Fast and Generalized Polynomial Time Memory Consistency Veri?cation[C]//Proc. of the 18th International Conference on Computer Aided Verification. Berlin, Germany: Springer-Verlag, 2006: 503-516.
[8] Chen Yunji, Lv Yi, Hu Weiwu, et al. Fast Complete Memory Consistency Veri?cation[C]//Proc. of the 15th International Symposium on High Performance Computer Architecture. [S. l.]: IEEE Computer Society, 2009: 381-392.
[9] 王朋宇, 陈云霁, 沈海华, 等. 片上多核处理器存储一致性验证[J]. 软件学报, 2010, 21(4): 863-874.
[10] Lv Zheng, Chen Hao, Chen Feng, et al. Fast Verification of Memory Consistency for Chip Multi-processor[C]//Proc. of the 7th International Conference on Computational Intelligence and Security. [S. l.]: IEEE Computer Society, 2011: 1497-1502.

[1]	高秀武, 姜军, 白书敬, 黄亮明. 一种加速访存地址计算的编译优化[J]. 计算机工程, 2023, 49(1): 173-180.
[2]	周雍浩, 徐金龙, 李斌, 钱宏, 聂凯. 面向神威高性能多核处理器的并行编译优化方法[J]. 计算机工程, 2022, 48(9): 130-138.
[3]	焦童, 陈玲玲, 安鑫, 李建华. 基于重用信息的非易失性缓存动态旁路策略[J]. 计算机工程, 2021, 47(4): 158-165.
[4]	郭威, 谢光伟, 张帆, 李敏. 一种分布式存储系统拟态化架构设计与实现[J]. 计算机工程, 2020, 46(6): 12-19.
[5]	毛向杰, 张品. 云平台数据完整性混合验证方案[J]. 计算机工程, 2020, 46(10): 46-51.
[6]	冯国富, 舒玉娟, 陈明, 董立夫. 基于big.LITTLE架构的多目标功耗自适应控制方法[J]. 计算机工程, 2019, 45(7): 60-65.
[7]	吴颖豪,凌捷. 一种改进的云存储数据完整性验证方法[J]. 计算机工程, 2019, 45(3): 36-40.
[8]	孙黎, 苏宇, 张弛, 张涛. 分布式存储系统中的纠删码容错方法研究[J]. 计算机工程, 2019, 45(11): 74-80.
[9]	赵瑞姣,朱怡安,李联. 基于异构多核系统的混合关键任务调度算法[J]. 计算机工程, 2018, 44(2): 51-55.
[10]	吴修国. 云存储系统中基于动态规划的最小开销数据副本布局研究[J]. 计算机工程, 2017, 43(7): 29-37.
[11]	陆思羽,王宏伟,张悠慧,杨广文,郑纬民. 面向MPI集合操作的定制化片上网络[J]. 计算机工程, 2017, 43(6): 1-10,18.
[12]	张晶,孙少杰,范洪博,付鑫,张果. 高实时性异构多核处理器任务调度算法[J]. 计算机工程, 2017, 43(5): 55-59.
[13]	朱怡安,黄林林,李联,罗殊彦. 多核平台下分区操作系统的安全关键任务调度方法[J]. 计算机工程, 2017, 43(12): 38-44.
[14]	金星,荆明娥,曾晓洋. 基于异构通信机制的任务映射算法[J]. 计算机工程, 2017, 43(12): 51-54,59.
[15]	杜然,黄秋兰,阚文枭,王聪,徐琪,陈刚. 基于Chord算法的可扩展高性能元数据存储环设计[J]. 计算机工程, 2016, 42(8): 1-8.

选择文件类型/文献管理软件名称

选择包含的内容

MOTEC: 一个存储一致性模型验证工具

MOTEC: A Validation Tool for Memory Consistency Model

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

MOTEC: 一个存储一致性模型验证工具

MOTEC: A Validation Tool for Memory Consistency Model

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价