Case study

For the case study we have tried to verify parameterized versions of cache coherence protocols.

Cache coherence protocols.Local cache techniques are important in shared-memory multiprocessor systems because they allow the reduction of both memory access latency and network traffic. Using such techniques, each processor has its own fast memory cache, holding local copies of main memory blocks. Although reducing the access time, this approach poses the problem of cache consistency, whereby one has to ensure that copies of the same memory block residing in the caches of different processors are consistent. Such data consistency can be provided by cache coherence protocols, which typically operate as follows: every processor is equipped with a finite state control process, which reacts to read and write requests. This control process ensures that consistency of each cache is retained with respect to the other caches in the system. Abstracting from the low-level implementation details of the I/O and synchronization primitives, one may consider cache coherence protocols as families of identical finite state machines together with a primitive form of communication. Correctness at such a level of abstraction can be expressed in terms of co-occurrences of some states in which, for example, the processors are allowed to change the content of their cache copies.

Verification of parametrized cache coherence protocols (for all possible numbers of processors) is a non-trivial, but still in some cases feasible problem to tackle. One particular successful approach is presented in [5]. More references will follow soon.