Specication of Memory Models and Design of Provably Correct Cache Coherence Protocols

We propose a twophase ImperativeDirective design methodology for designing cache coherence protocols and use it to develop a family of protocols to implement Sequential Consistency in a distributed system with hierarchical caches In the Impera tive design phase actions or state transitions are dened to ensure that the system only exhibits behaviors that are consistent with the memory model In the Directive design phase one ensures liveness ie the system eventually takes the desired action In each design phase the protocol can be rened incrementally to accommodate implementa tion constraints The separation of correctness and liveness concerns and successive renement greatly simplies protocol design and verication The methodology is especially suitable for designing adaptive protocols which essentially allow imperative actions to be invoked adaptively according to program access patterns The design of cache coherence protocols plays an important role in building parallel or distributed systems that support shared memory Protocols can be implemented completel