The compositional approach to sequential consistency and lazy caching

摘要

The lazy caching protocol propose by Afek, Brown and Merritt [ABM93], is explained and formally Proven correct by means of compositional methods. The pro- Tocol is decomposed into four simple protocols, which are Of interest on their own. A top level proof is given tat is to A large extent independent of the particular model used for The more detailed proofs and allows for a mumber of gen- Eralizations of the original lazy caching protocol.