Cache consistency by design (Invited Address I)

In this paper we present a proof outline of the sequential consistency the lazy caching protocol of Afek, Brown, and Merritt. We will follow a strategy of stepwise refinement, developing the distributed caching memory in five transformation steps from a specification of the serial memory, whilst preserving the sequential consistency in each step. What we present, in fact, is a rationalized design of the distributed caching memory. We will use a simple process-algebraic formalism for the specification of the various design stages. We will not follow a strictly algebraic exposition, however. At some points the correctness will follow using direct semantic arguments, and we will also employ higher-order constructs like action transducers to relate behaviours. The distribution of the design/proof over five transformation steps provides a good insight into the variations that could have been allowed at each point of the design while still maintaining sequential consistency. The design/proof in fact establishes the correctness of a whole family of related memory architectures. The factorization in smaller steps also allows for a closer analysis of the fairness assumptions about the distributed memory.