The compositional approach to sequential consistency and lazy caching

The lazy caching protocol proposed by Afek, Brown and Merritt [ABM93], is e xplained and formally proven correct by means of compositional methods. The protocol is decomposed into four simple protocols, which are of interest o n their own. A top level proof is given that is to a large extent independe nt of the particular model used for the more detailed proofs and allows for a number of generalizations of the original lazy caching protocol. Detaile d proofs of safety and liveness properties are given using CSP and trace lo gic.