A Language-Theoretic Approach to Specifying and Verifying Multiprocessor Cache Coherence Protocols

Computer architects have often used trace-driven simulations to evaluate the performance of new architectural features. However, the verification of these features often proves to be more difficult than their specification and implementation. This paper proposes a novel approach for extending the basic idea of trace-driven simulation to automatically verify a complex cache coherence protocol for large-scale multiprocessor systems. A formal model of the coherence protocol is specified as several human-readable text files which are automatically verified using the Mur' formal verfication tool. A formal execution trace is extracted during the verification process and re-encoded to provide the input stimulus for a simulation of the actual implementation model, which is typically specified in a standard hardware description language. This approach provides a rigorous connection between the architectural specification and the verification of the low-level implementation. The feasibility of this approach is demonstrated by using it to verify the coherence protocol of the Cray SV2