Implementing Coherent Memory

Butler W. Lampson

Citation: Implementing coherent memory. In A Classical Mind: Essays in Honour of C.A.R. Hoare, ed. A. Roscoe, Prentice-Hall, 1994, pp 259-274.

Links: Abstract, Postscript, Acrobat. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.

Email: blampson@microsoft.com. This paper is at http://research.microsoft.com.

Abstract:

In this paper we show how to write precise specifications for coherent and incoherent memory, and how to implement coherent memory in several ways, one of which is on top of incoherent memory. Our technique for showing the correctness of the implementations is the abstraction function introduced by Hoare to handle abstract data types. A decade later, Lamport and Lynch extended Hoare's methods to concurrent systems like the ones we treat.