A Correctness Proof of a Cache Coherence Protocol

SCI -- Scalable Coherent Interface -- is an IEEE standard for specifying communication between multiprocessors in a shared memory model. In this paper we model part of SCI by a program written in a UNITY-like programming language. 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 careful formulation of lemmata and the use of auxiliary predicates as an abstraction mechanism. 1 Introduction In this paper we formalize and verify part of the SCI (Scalable Coherent Interface) protocol [19]. 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 ..