Deriving Efficient Cache Coherence Protocols through Refinement

Abstract. We address the problem of developing efficient cache coherence protocols implementing distributed shared memory (DSM) using message passing. A serious drawback of traditional approaches to this problem is that designers are required to state the desired coherence protocol at the level of asynchronous message interactions. We propose a method in which designers express the desired protocol at a high-level using rendezvous communication. These descriptions are much easier to understand and computationally more efficient to verify than asynchronousprotocols due to their small state spaces. The rendezvous protocol can also be synthesized into efficient asynchronous protocols. We present our protocol refinement procedure, prove its soundness, and provide examples of its efficiency.

• Type: Conference
• Year: 1998
• Where: IPPS
• Authors: Ratan Nalumasu, Ganesh Gopalakrishnan
• Keywords: Coherence Protocol, Distributed And Parallel Computing, Efficient Asynchronous Protocols, Efficient Cache Coherence, IPPS 1998