A top down approach to the formal specification of SCI cache coherence

Abstract

The paper gives an introduction to an ongoing effort of formally specifying and verifying the cache coherence protocol of the new IEEE interconnect standard called the Scalable Coherent Interface. We first give the the most abstract (top level) specification of a memory system. We then introduce a private cache for each processor, and specify the notion of cache coherence. We refine the specifications of the memory operations for use with caches, and finally outline the more complex bottom layers where directory structures and concurrency are introduced.