Abstract
In this paper we present a proof outline of the sequential consistency the lazy caching protocol of Afek, Brown, and Merritt. We 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. What we present, in fact, is a rationalized design of the distributed caching memory. We will use 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 follow 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.
Original language | English |
---|---|
Title of host publication | Protocol Specification, Testing and Verification XIV |
Editors | Son T. Vuong, Samuel T. Chanson |
Place of Publication | London, UK |
Publisher | Chapman & Hall |
Pages | 53-67 |
ISBN (Electronic) | 978-0-387-34867-4 |
ISBN (Print) | 978-1-4757-6308-9 |
DOIs | |
Publication status | Published - 1994 |
Event | 14th International IFIP W.G. 6.1 Symposium on Protocol Specification, Testing and Verification, PSTV 1994 - Vancouver, Canada Duration: 7 Jun 1994 → 10 Jun 1994 Conference number: 14 |
Publication series
Name | IFIP Advances in Information and Communication Technology |
---|---|
Publisher | Springer |
ISSN (Print) | 1868-4238 |
ISSN (Electronic) | 1868-422X |
Conference
Conference | 14th International IFIP W.G. 6.1 Symposium on Protocol Specification, Testing and Verification, PSTV 1994 |
---|---|
Abbreviated title | PSTV XIV |
Country | Canada |
City | Vancouver |
Period | 7/06/94 → 10/06/94 |
Keywords
- Behaviour expression
- Label transition system
- Local cache
- Process definition
- Sequential consistency