|
|||||
|
|
| Godson-T缓存一致性协议的Murphi建模和验证 | |
| 作者姓名： | 周琰 |
| 作者单位： | 中国科学院软件研究所,北京 100190; 中国科学院大学,北京 100190 |
| 基金项目： | 国家自然科学基金(61272135) |
| 摘 要： | Godson-T缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议．在Godson-T协议中,缓存一致性协议和存储一致性模型存在紧密的紧耦合关系,分析协议的一致性时发现该协议满足的缓存一致性不是强一致性,不满足传统意义上缓存透明的一致性要求．我们选取了Murphi模型检测工具作为我们建模的语言和验证工具．在对Godson-T缓存一致性协议建模的时候,由于协议的上述特点,我们需要对处理器核结点,高速缓存和内存作为一个整体建模,并成功地验证了协议的相关性质． |
| 关 键 词： | 众核处理器 内存一致性模型 缓存一致性协议 模型检测 |
| 收稿时间： | 2013-03-22 |
| 修稿时间： | 2013-04-18 |
| 本文献已被 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机系统应用》浏览原始摘要信息 | |
| 点击此处可从《计算机系统应用》下载免费的PDF全文 | |