VERIFICATION TECHNIQUES FOR CACHE COHERENCE PROTOCOLS

In this article we present a comprehensive survey of various approache s for the verification of cache coherence protocols based on state enu meration, (symbolic) model checking, and symbolic state models. Since these techniques search the state space of the protocol exhaustively, the amount of memory required to manipulate the state information and the verification time grow very fast with the number of processors and the complexity of the protocol mechanisms. To be successful for syste ms of arbitrary complexity, a verification technique must solve this s o-called state space explosion problem. The emphasis of our discussion is on the underlying theory in each method of handling the state spac e explosion problem, and formulating and checking the safety propertie s (e.g., data consistency) and the liveness properties (absence of dea dlock and livelock). We compare the efficiency and discuss the limitat ions of each technique in terms of memory and computation time. Also, we discuss issues of generality, applicability, automaticity, and amen ity for existing tools in each class of methods. No method is truly su perior because each method has its own strengths and weaknesses. Final ly, refinements that can further reduce the verification time and/or t he memory requirement are also discussed.