A Correctness Proof of a Cache Coherence Protocol

SCI -- Scalable Coherent Interface -- is a new IEEE standard for specifying communicationbetween multiprocessors in a shared memory model. In this paper we model part of SCI by a program written in a UNITY-like programminglanguage. This part of SCI is formally specified in Manna and Pnueli's Linear Time Temporal Logic (LTL). We prove that the program satisfies its specification. The proof is carried out within LTL and uses history variables. Structuring of the proof is achieved by means of auxiliary predicates. 1. Introduction In this paper we formalize and verify part of the SCI (Scalable Coherent Interface) protocol [17]. This protocol is an IEEE standard for specifying communication between shared memory multiprocessors. It is called scalable because the protocol is intended to be performed in a system which may consist of up to 64,000 processors. The correctness proof we present in the current paper is carried out for an arbitrary, finite number of processors (and not for some max..