Implementing Coherent Memory

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.