论文部分内容阅读
Godson-T缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议．在Godson-T协议中，缓存一致性协议和存储一致性模型存在紧密的紧耦合关系，分析协议的一致性时发现该协议满足的缓存一致性不是强一致性，不满足传统意义上缓存透明的一致性要求．我们选取了Murphi模型检测工具作为我们建模的语言和验证工具．在对Godson-T缓存一致性协议建模的时候，由于协议的上述特点，我们需要对处理器核结点，高速缓存和内存作为一个整体建模，并成功地验证了协议的相关性质．