Compositional Approach to Sequential Consistency and Lazy Caching

摘要

The lazy caching algorithm is explained and formally proven correct by means ofcompositional methods. The algorithm is decomposed into four simple protocols, that 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. Detailed proofs are given within a partial order variation of the quiescent trace model.