Model Checking for Commutative Cache Coherence System

Traditional cache coherence protocols can limit processor performance due to bus contention in multi-core systems. As a result, numerous extended protocols have been developed to reduce unnecessary memory accesses. However, ensuring the correctness of these protocols in various concurrency scenarios poses a significant challenge. This paper focuses on the MUSI (Modified Update-only Shared Invalid) protocol and addresses this challenge by formalizing and analyzing it using the Maude formal specification and verification language. By leveraging the expressive power of Maude, we capture the intricate state transitions and behaviors of the MUSI protocol, enabling comprehensive verification of its safety and liveness properties. Additionally, we evaluate the scalability and robustness of our formalization through a series of experiments, comparing it against existing techniques.