Symbolic state model: A new approach for the verification of cache coherence protocols
Pong, Fong · University of Southern California Digital Library · 2017
Cache coherence protocols are important to the correct and efficient operation of a shared-memory multiprocessor system. The complexity of cache coherence protocols is increasing due to difficulty of providing the programmer with a logical view of shared-memory while distributing the physical memory so that most accesses are local. This is particularly true for large-scale, scalable multiprocessors, where cache coherence protocols cooperating with latency tolerance techniques and relaxed memory models are used to overcome the problems of long latency and large bandwidth for remote memory accesses. Since random testing and trace-driven simulations are not sufficient to validate their correctness, it is necessary to develop efficient and reliable verification methods. Most verification methods now use finite state machines to model cache protocols and check the correctness of cache protocols by exploring the state spaces. These methods are plagued by the state space explosion problem in that the state space increases exponentially as the number and the complexity of components of the system increase. Applications are therefore limited to small and simplified protocol models. We have developed a new method based on a symbolic state model (SSM). The method exploits the symmetry of cache-based systems and a unique feature of coherence protocols, which makes it only necessary to keep track of whether there are 0,1, or several copies in a particular cache state in order to verify a protocol. This symbolic state representation leads to a drastic reduction of the state space, which makes the verification time shorter, and uses less memory to store states. Importantly, the protocols are verified for any system size without the state space explosion problem. A fully automated verification system has been implemented, which includes a high-level description language and a mechanical verifier. The tool has been successfully applied to a wide range of cache protocols, including simple snooping protocols, central directory-based protocols, S3.mp (Sun's Scalable Shared-memory MultiProcessor) distributed directory-based protocol, and delayed consistency protocols developed for systems with relaxed memory models.