RCC高速缓存一致性协议的带参验证

• 作者: 周琰 孙鲁明
• 来源期刊: 计算机系统应用
• 关键词: 众核处理器 缓存一致性协议 带参模型检测 RCC Godson-T
• 年，卷（期）: 2014,（11）
• 所属期刊栏目: 专论?综述
• 页码范围: 10-15
• 页数: 6页
• 字数: 5761字
• 语种: 中文

摘要

Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统，对此协议的带参验证是一个很大的挑战。 Cubicle是最近出现的基于SMT求解器的带参模型检测工具。我们使用了Cubicle带参模型检测工具，成功对RCC协议进行了建模和验证。实验结果表明， RCC协议在结点个数为任意规模时均满足协议的各种安全性质。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙鲁明	中国科学院软件研究所	2	3	1.0	1.0
5	周琰		1	3	1.0	1.0