本文已被：浏览 1514次 下载 3335次
Received:March 22, 2013 Revised:April 18, 2013
Received:March 22, 2013 Revised:April 18, 2013
中文摘要: Godson-T 缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议. 在Godson-T协议中, 缓存一致性协议和存储一致性模型存在紧密的紧耦合关系, 分析协议的一致性时发现该协议满足的缓存一致性不是强一致性, 不满足传统意义上缓存透明的一致性要求. 我们选取了Murphi模型检测工具作为我们建模的语言和验证工具. 在对Godson-T缓存一致性协议建模的时候, 由于协议的上述特点, 我们需要对处理器核结点, 高速缓存和内存作为一个整体建模, 并成功地验证了协议的相关性质.
Abstract:Godson-T cache coherence protocol is used in Godson-T many-core architecture. In Godson-T, there is a close tight coupling relationship between cache coherence protocol and memory consistency model. In our research of Godson-T, we found that its cache coherence is relaxed unlike other cache coherence protocols. We choose Murphi as modeling language and verification tool. Thus, when we modeling Godson-T, core, cache and memory must be take into account as a whole. Some invariants and properties has been verified with Murphi.
文章编号： 中图分类号： 文献标志码：
基金项目:国家自然科学基金(61272135)
| Author Name | Affiliation |
| ZHOU Yan | Institute of Software, Chinese Academy of Sciences, Beijing 100190, China University of Chinese Academy of Sciences, Beijing 100190, China |
| Author Name | Affiliation |
| ZHOU Yan | Institute of Software, Chinese Academy of Sciences, Beijing 100190, China University of Chinese Academy of Sciences, Beijing 100190, China |
引用文本：
周琰.Godson-T缓存一致性协议的Murphi建模和验证.计算机系统应用,2013,22(10):124-128
ZHOU Yan.Modeling and Verification of Godson-T Cache Coherence Protocol with Murphi Tool.COMPUTER SYSTEMS APPLICATIONS,2013,22(10):124-128
周琰.Godson-T缓存一致性协议的Murphi建模和验证.计算机系统应用,2013,22(10):124-128
ZHOU Yan.Modeling and Verification of Godson-T Cache Coherence Protocol with Murphi Tool.COMPUTER SYSTEMS APPLICATIONS,2013,22(10):124-128
