Formal verification of safety properties for a cache coherence protocol

This paper presents a case study on the formal specification of a cache coherence protocol and the verification of some of its safety properties. Cache coherence refers to the consistency between the contents of a memory resource shared by many processes, that can have read and write access, and each local copy of the memory contents. The protocol presented in this paper is based on the ESI standard in which a central controller can grant exclusive and shared access to the memory, and also invalidate access to the memory. The formal specification of the protocol is presented as a rewriting logic theory and it is fully executable in the Maude system. The safety properties presented in this paper are linear temporal logic (LTL) formulas expressing invariants about mutual exclusion among the processes accessing the shared memory resource. By using Maude´s search functionality and LTL model checker, some of these invariants can be proved automatically for a finite number of processes. This paper also presents an initial exploration on the mechanical verification of an invariant for any number of processes by means of deductive techniques based on inductive reasoning.