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

摘要：

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

关键词：众核处理器、缓存一致性协议、带参模型检测、RCC、Godson-T

分类号：TP3;TN9

在线出版日期：2014-12-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：10-15