Cache Coherency in SCI: Specification and a Sketch of Correctness
Amy Felty, Frank Stomp · Formal Aspects of Computing · 1999
Abstract. 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 give a sketch of our proof that the program satisfies its specification. The proof has been carried out within LTL. It uses history variables. Structuring of the proof has been achieved by careful formulation of lemmata and the use of auxiliary predicates as an abstraction mechanism.