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

• 作者: 张珩 沈海华 王朋宇 陈云霁 陈天石
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 存储一致性模型 验证 时间序 片上多核处理器 缓存一致性
• 年，卷（期）: 2010,（4）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 863-874
• 页数: 12页
• 分类号: TP316
• 字数: 10425字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2010.03705

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈云霁		1	24	1.0	1.0
2	沈海华		1	24	1.0	1.0
3	陈天石	中国科学技术大学计算机科学技术系	6	65	4.0	6.0
4	张珩		1	24	1.0	1.0