Summary.
The lazy caching protocol proposed by Afek, Brown and Merritt [ABM93], is explained and formally proven correct by means of compositional methods. The protocol is decomposed into four simple protocols, which are of interest on their own. A top level proof is given that is to a large extent independent of the particular model used for the more detailed proofs and allows for a number of generalizations of the original lazy caching protocol. Detailed proofs of safety and liveness properties are given using CSP and trace logic.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Janssen, W., Poel, M. & Zwiers, J. The compositional approach to sequential consistency and lazy caching. Distrib Comput 12, 105–127 (1999). https://doi.org/10.1007/s004460050061
Issue Date:
DOI: https://doi.org/10.1007/s004460050061