Cache Coherency in SCI: Specication and a Sketch of Correctness

Abstract. SCI { Scalable Coherent Interface { is an IEEE standard for specify-ing communication between multiprocessors in a shared memory model. In this paper we model part of SCI by a program written in a UNITY-like program-ming language. This part of SCI is formally specied in Manna and Pnueli's Linear Time Temporal Logic (LTL). We give a sketch of our proof that the pro-gram satises its specication. The proof has carried out within LTL. It uses history variables. Structuring of the proof hass achieved by careful formulation of lemmata and the use of auxiliary predicates as an abstraction mechanism. 1