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