Back to University of Twente portal
Cache Consistency by Design
Brinksma, H. (1999) Cache Consistency by Design. Distributed Computing, 12 (2/3). pp. 552-565. ISSN 0178-2770
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png) | PDF Restricted to UT campus only: Request a copy 375Kb |
| Abstract: | In this paper we present a proof of the sequential consistency of the lazy caching protocol of Afek, Brown, and Merritt. The proof will follow a strategy of stepwise refinement, developing the distributed caching memory in five transformation steps from a specification of the serial memory, whilst preserving the sequential consistency in each step. The proof, in fact, presents a rationalized design of the distributed caching memory. We will carry out our proof using a simple process-algebraic formalism for the specification of the various design stages. We will not follow a strictly algebraic exposition, however. At some points the correctness will be shown using direct semantic arguments, and we will also employ higher-order constructs like action transducers to relate behaviours. The distribution of the design/proof over five transformation steps provides a good insight into the variations that could have been allowed at each point of the design while still maintaining sequential consistency. The design/proof in fact establishes the correctness of a whole family of related memory architectures. The factorization in smaller steps also allows for a closer analysis of the fairness assumptions about the distributed memory. |
| Item Type: | Article |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Link to this item: | http://purl.utwente.nl/publications/63266 |
| Official URL: | http://dx.doi.org/10.1007/s004460050058 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page