片上多核处理器存储一致性验证

作     者：王朋宇 陈云霁 沈海华 陈天石 张珩 WANG Peng-Yu;CHEN Yun-Ji;SHEN Hai-Hua;CHEN Tian-Shi;ZHANG Heng

作者机构：中国科学院计算技术研究所计算机系统结构重点实验室北京100190 中国科学院研究生院北京100049 中国科学技术大学计算机科学技术系安徽合肥230027 

基　　金：国家自然科学基金Nos.60603049 60673146 60736012 60721061 国家高技术研究发展计划(863)Nos.2007AA01Z112 2008AA110901 2007AA01Z114 国家重点基础研究发展计划(973)No.2005CB321600~~ 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2010年第21卷第4期

页      码：863-874页

摘      要：存储一致性验证是片上多核处理器功能验证的重要部分.由于验证并行程序的执行结果是否符合存储一致性模型理论上是NP难问题,现有的验证方法中只能采用一些时间复杂度大于O(n3)的不完全方法.发现在支持写原子性的多处理器系统中,两条执行时间不重叠的操作之间存在确定的时间序.通过引入时间序的概念,设计并实现了一种线性时间复杂度的存储一致性验证工具***利用时间序将验证局部化,使得在表示程序执行结果的有向图中,序关系边的推导和正确性检测都被限定在有限范围内.与现有其他方法相比,LCHECK时间复杂度低,对程序长度和访存地址数没有限制,因此验证效率更高.作为国产片上多核处理器龙芯3号的重要验证工具,LCHECK发现了一些存储系统的设计错误.

主 题 词：存储一致性模型 验证 时间序 片上多核处理器 缓存一致性 

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.3724/sp.j.1001.2010.03705

馆 藏 号：203864843...