The compositional approach to sequential consistency and lazy caching |
| |
Authors: | Wil Janssen Mannes Poel Job Zwiers |
| |
Affiliation: | (1) University of Twente, NL-7500 AE Enschede, The Netherlands , NL |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|