Revisiting the Complexity of Hardware Cache Coherence and Some Implications
Revisiting the Complexity of Hardware Cache Coherence and Some Implications
复制标题
重新审视硬件缓存一致性的复杂性和一些含义
DOI：
10.1145/2663345
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Ching
中科院分区：
文献类型：
--
作者：
Rakesh Komuravelli;S. Adve;Ching
Cache Coolerence是共享内存系统的组成部分，但也被认为是此类系统中最复杂的部分之一多核时代随着核心的数量越来越多，关于硬件连贯性的复杂性是否已被驯服或是否应该放弃软件连贯性通过使用MURφ模型检查工具验证广泛使用的MESI协议的公开可用的最新实现，重新审视硬件缓存相干性的复杂性。我们很难分析，并花了几天的时间来比较复杂性，我们还验证了最近提出的Denovo协议，该协议利用了纪律处分的软件编程。在修复这些错误后，易于修复错误，我们的验证实验表明，与Denovo相比，MESI的到达状态更高，导致验证时间增加了20倍（模型检查）。验证协议，需要做几个简化的假设（例如，两个地址）的工具。一致性协议仍然是复杂的； ;（4）他们表明，基于硬件软件共同设计的系统可以为缓存连贯性提供更简单的方法，从而减少整体验证工作并允许验证更详细的模型和协议否则将通过计算资源限制的扩展。
Cache coherence is an integral part of shared-memory systems but is also widely considered to be one of the most complex parts of such systems. Much prior work has addressed this complexity and the verification techniques to prove the correctness of hardware coherence. Given the new multicore era with increasing number of cores, there is a renewed debate about whether the complexity of hardware coherence has been tamed or whether it should be abandoned in favor of software coherence. This article revisits the complexity of hardware cache coherence by verifying a publicly available, state-of-the-art implementation of the widely used MESI protocol, using the Murφ model checking tool. To our surprise, we found six bugs in this protocol, most of which were hard to analyze and took several days to fix. To compare the complexity, we also verified the recently proposed DeNovo protocol, which exploits disciplined software programming models. We found three relatively easy to fix bugs in this less mature protocol. After fixing these bugs, our verification experiments showed that, compared to DeNovo, MESI had 15X more reachable states leading to a 20X increase in verification (model checking) time. Although we were eventually successful in verifying the protocols, the tool required making several simplifying assumptions (e.g., two cores, one address). Our results have several implications: (1) they indicate that hardware coherence protocols remain complex; (2) they reinforce the need for protocol designers to embrace formal verification tools to demonstrate correctness of new protocols and extensions; (3) they reinforce the need for formal verification tools that are both scalable and usable by non-expert; and (4) they show that a system based on hardware-software co-design can offer a simpler approach for cache coherence, thus reducing the overall verification effort and allowing verification of more detailed models and protocol extensions that are otherwise limited by computing resources.