A Top Down Approach to the Formal Specification of SCI Cache Coherence

Scalable Coherent Interface (SCI) is a bus defined by an IEEE working group. The purpose of SCI is to be the interconnect in future shared memory multiprocessors. The SCI definition, as proposed by the working group, specifies a cache coherence protocol. This specification is given in the C programming language. This report describes a layered approach to the specification of this cache coherence protocol. The top layer defines our most abstract view of the memory system, that is a store without cache. Caches are introduced at the second level. The SCI coherence protocol is directory based, the directory being implemented as a doubly linked list between all caches that contain the same memory entity. In our layered approach to this structure we first implement the set of caches that share the same memory entity, as a sequence of caches. At the bottom level specified in this report the data structure is a set of caches structured in a doubly linked list. Our specifications are fully app..