10.3969/j.issn.1003-3254.2013.10.024
Godson-T缓存一致性协议的Murphi建模和验证
Godson-T 缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议。在Godson-T协议中,缓存一致性协议和存储一致性模型存在紧密的紧耦合关系,分析协议的一致性时发现该协议满足的缓存一致性不是强一致性,不满足传统意义上缓存透明的一致性要求。我们选取了 Murphi 模型检测工具作为我们建模的语言和验证工具。在对Godson-T缓存一致性协议建模的时候,由于协议的上述特点,我们需要对处理器核结点,高速缓存和内存作为一个整体建模,并成功地验证了协议的相关性质。
众核处理器、内存一致性模型、缓存一致性协议、模型检测
TP3;TP1
国家自然科学基金61272135
2013-10-30(万方平台首次上网日期,不代表论文的发表时间)
共5页
124-128