Design and verification of adaptive cache coherence protocols
Xiaowei Shen, Arvind Arvind · 2000
We propose to apply Term Rewriting Systems (TRSs) to modeling computer architectures and distributed protocols. TRSs offer a convenient way to precisely describe asynchronous systems and can be used to verify the correctness of an implementation with respect to a specification. This dissertation illustrates the use of TRSs by giving the operational semantics of a simple instruction set, and a processor that implements the same instruction set on a micro-architecture that allows register renaming and speculative execution. A mechanism-oriented memory model called Commit-Reconcile & Fences (CRF) is presented that allows scalable implementations of shared memory systems. The CRF model exposes a semantic notion of caches, referred to as saches, and decomposes memory access operations into simpler instructions. In CRF, a memory load operation becomes a Reconcile followed by a Loadl, and a memory store operation becomes a Storel followed by a Commit. The CRF model can serve as a stable interface between computer architects and compiler writers. We design a family of cache coherence protocols for distributed shared memory systems. Each protocol is optimized for some specific access patterns, and contains a set of voluntary rules to provide adaptivity that can be invoked whenever necessary. It is proved that each protocol is a correct implementation of CRF, and thus a correct implementation of any memory model whose programs can be translated into CRF programs. To simplify protocol design and verification, we employ a novel two-stage design methodology called Imperative-&-Directive that addresses the soundness and liveness concerns separately throughout protocol development. Furthermore, an adaptive cache coherence protocol called Cachet is developed that provides enormous adaptivity for programs with different access patterns. The Cachet protocol is a seamless integration of multiple micro-protocols, and embodies both intra-protocol and inter-protocol adaptivity that can be exploited via appropriate heuristic mechanisms to achieve optimal performance under changing program behaviors. The Cachet protocol allows store accesses to be performed without the exclusive ownership, which can notably reduce store latency and alleviate cache thrashing due to false sharing. (Copies available exclusively from MIT Libraries, Rm. 14-0551, Cambridge, MA 02139-4307. Ph. 617-253-5668; Fax 617-253-1690.)