Godson-T缓存一致性协议的Murphi建模和验证
文献类型：期刊论文
| 作者 | 周琰 |
| 刊名 | 计算机系统应用
 |
| 出版日期 | 2013 |
| 期号 | 10页码:124-128 |
| 关键词 | 众核处理器 内存一致性模型 缓存一致性协议 模型检测 many-core processer memory consistency model cache coherence protocol model checking |
| ISSN号 | 1003-3254 |
| 其他题名 | Modeling and Verification of Godson-T Cache Coherence Protocol with Murphi Tool |
| 中文摘要 | Godson-T 缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议。在Godson-T协议中，缓存一致性协议和存储一致性模型存在紧密的紧耦合关系，分析协议的一致性时发现该协议满足的缓存一致性不是强一致性，不满足传统意义上缓存透明的一致性要求。我们选取了 Murphi 模型检测工具作为我们建模的语言和验证工具。在对Godson-T缓存一致性协议建模的时候，由于协议的上述特点，我们需要对处理器核结点，高速缓存和内存作为一个整体建模，并成功地验证了协议的相关性质。 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. |
| 语种 | 中文 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/17004]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | 周琰. Godson-T缓存一致性协议的Murphi建模和验证[J]. 计算机系统应用,2013(10):124-128. |
| APA | 周琰.(2013).Godson-T缓存一致性协议的Murphi建模和验证.计算机系统应用(10),124-128. |
| MLA | 周琰."Godson-T缓存一致性协议的Murphi建模和验证".计算机系统应用 .10(2013):124-128. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。