Verification of hierarchical cache coherence protocols for futuristic processors
Xiaofang Chen · 2008
Multicore architectures are considered inevitable, given that sequential processing hardware has hit various limits. Unfortunately, the memory system of multicore processors is a huge bottleneck, as distant memory accesses cost thousands of cycles. To combat this problem, one must design aggressively optimized cache coherence protocols. This introduces two problems for futuristic cache coherence protocols which will be hierarchically organized for scalable designs: design correctness and hardware implementation correctness. Experiences show that monolithic verification will not scale to hierarchical designs and implementations. Hence there exist two unsolved problems for futuristic cache coherence protocols: (i) handle the complexity of several coherence protocols running concurrently, i.e., hierarchical protocols, and (ii) verify that the RTL implementations correctly implement the specifications. Our thesis is that formal methods based on model checking and assume guarantee verification methods can be developed to substantially ameliorate these problems faced by designers. More specifically, to solve the first problem, we develop assume guarantee reasoning to decompose a hierarchical coherence protocol into a set of abstract protocols. The approach is conservative, in the sense that by verifying these abstract protocols, the original hierarchical protocol is guaranteed to be correct with respect to its properties. For the second problem, we develop a formal theory to check the refinement relationship, i.e., under which conditions can we claim that an RTL implementation correctly implements a high level specification. We also develop a compositional approach using abstraction and assume guarantee reasoning to reduce the verification complexity of refinement check. Finally, we evaluate the solutions in collaboration with industry and partly mechanize the refinement check. We propose research that will lead to a characterization of the proposed mechanisms through several verification tools and protocol benchmarks. For high level modeling and verification, we show that for three hierarchical protocols with different features which we developed for multiple chip-multiprocessors, more than a 20-fold improvement in terms of the number of states visited can be achieved. For refinement check, we show that for a driving coherence protocol example with realistic hardware features, refinement check can find subtle bugs which are easy to miss by checking coherence properties alone. Furthermore, we show that for the protocol example, our compositional approach can finish the refinement check within 30 minutes while a state-of-art verification tool in industry cannot finish in over a day. Finally, we extend a hardware language and a tool, to mechanize the refinement check process. In summary the research accomplished in this work substantiates our thesis statement with a body of results generated using tools that were constructed during this research.