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

摘要

RCC cache coherence protocol in Godson-T many-core processor is a characteristic parameterized concurrent system. It is a challenge to verify this protocol. Cubicle is a recently built parameterized model checking tool based on SMT solver. We used Cubicle to model and verify RCC protocol successfully. The experimental results show that RCC protocol satisfies all kinds of safety properties regardless of how many nodes it has.%Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统，对此协议的带参验证是一个很大的挑战。 Cubicle是最近出现的基于SMT求解器的带参模型检测工具。我们使用了Cubicle带参模型检测工具，成功对RCC协议进行了建模和验证。实验结果表明， RCC协议在结点个数为任意规模时均满足协议的各种安全性质。