Automatic generation of verifiable cache coherence simulation models from high-level specifications

Performance modelling and verification are vital steps in the development cycle of any cache coherency protocol. Two separate models are usually required to perform each analysis step and as protocols become increasingly complex each can become correspondingly unwieldy. We examine how stochastic process algebra can be used to describe cache coherency protocols in such a way as to allow both the correctness and performance of the protocol to be investigated together. We reintroduce a formalism called "Spade" and show how a simulation model can be generated from a Spade description of a memory system. We also show how the coherency protocol underlying the memory system can be verified as correct by showing observational equivalence between the system and a specification for the memory system based on a memory consistency model. We demonstrate the approach by applying it to a model of the write-through coherency protocol for bus-based shared-memory multiprocessors. We validate simulation results from the model by comparing against a hand coded simulation.