Design and Verification of Adaptive Cache Coherence Protocols

        Arvind (MIT) and Xiaowei Shen (IBM T.J. Watson)

This talk discusses three issues regarding cache coherence protocols: What
memory model should be supported?  What adaptivity can be provided to deal
with changing memory-access patterns or resources?  And how adaptive
protocols should be designed and verified?

We present a novel mechanism-oriented memory model called Commit-Reconcile &
Fences (CRF). CRF exposes a semantic notion of caches, and decomposes
conventional load and store instructions into finer-grain operations.  In
CRF, a memory load operation becomes a Reconcile followed by a Load-local,
and a memory store operation becomes a Store-local followed by a Commit.
The CRF model can serve as a stable interface between computer architects
and compiler writers.

We then present a family of cache coherence protocols that implement the CRF
model for DSM 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.  Furthermore, we develop a protocol
called CACHET that seamlessly integrates multiple protocols to provide both
intra- and inter-protocol adaptivity.

We employ a novel Imperative-&-Directive design methodology that addresses
the soundness and liveness concerns separately throughout protocol
development. The use of this methodology dramatically facilitates protocol
design and verification. It has been shown 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. Time permitting,
we will give an anecdotal account of the issues in manual and semiautomatic
proofs (using TLA's and PVS) of CACHET.

References:

[1]  "Commit-Reconcile & Fences: A New Memory Model for Architects and Compiler Writers",
Xiaowei Shen, Arvind and Larry Rudolph. In Proceedings of the 26th International Symposium on
Computer Architectures, Atlanta, Georgia, May 1999.

[2]  "CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems",
Xiaowei Shen, Arvind and Larry Rudolph. In Proceedings of the 13th ACM-SIGARCH International
Conference on Supercomputing, Rhodes, Greece, June 1999.

[3]  "Design and Verification of Adaptive Cache Coherence Protocols", PhD Thesis, Department of
Electrical Engineering and Computer Science, Massachusetts Institute of Technology, January 2000.
        http://www.csg.lcs.mit.edu/Users/xwshen/publications.html
                (The thesis subsumes references [1] and [2])

[4]  "Specification of Memory Models and Design of Provably Correct Cache Coherence Protocols",
Xiaowei Shen and Arvind, MIT CSG Memo 398, June 1997.
        http://www.csg.lcs.mit.edu/pubs/csgmemo.html