| RCC高速缓存一致性协议的带参验证 |
| |
| 引用本文： | 孙鲁明,周琰.RCC高速缓存一致性协议的带参验证[J].计算机系统应用,2014,23(11):10-15. |
| |
| 作者姓名： | 孙鲁明 周琰 |
| |
| 作者单位： | 1. 中国科学院 软件研究所，北京 100190; 中国科学院大学，北京 100490
2. 微软中国有限公司,苏州,215000 |
| |
| 摘 要： | Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统，对此协议的带参验证是一个很大的挑战。 Cubicle是最近出现的基于SMT求解器的带参模型检测工具。我们使用了Cubicle带参模型检测工具，成功对RCC协议进行了建模和验证。实验结果表明， RCC协议在结点个数为任意规模时均满足协议的各种安全性质。
|
| 关 键 词： | 众核处理器 缓存一致性协议 带参模型检测 RCC Godson-T |
| 收稿时间： | 2014/3/11 0:00:00 |
| 修稿时间： | 2014/4/14 0:00:00 |
Parameterized Verifation of RCC Cache Coherence Protocol |
| |
| SUN Lu-Ming and ZHOU Yan.Parameterized Verifation of RCC Cache Coherence Protocol[J].Computer Systems& Applications,2014,23(11):10-15. |
| |
| Authors: | SUN Lu-Ming and ZHOU Yan |
| |
| Affiliation: | Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;University of Chinese Academy of Sciences, Beijing 100190, China;MicrosoftChina Corporation, Ltd., Suzhou 215000, China |
| |
| Abstract: | 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. |
| |
| Keywords: | many-core processor cache coherence protocol parameterized model checking RCC Godson-T |
|
| 点击此处可从《计算机系统应用》浏览原始摘要信息 |
|
点击此处可从《计算机系统应用》下载全文 |
