Cache Consistency by Design

Research output: Contribution to journalArticleAcademicpeer-review

6 Citations (Scopus)

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.
Original languageUndefined
Article number10.1007/s004460050058
Pages (from-to)552-565
Number of pages14
JournalDistributed computing
Volume12
Issue number2/3
DOIs
Publication statusPublished - Jun 1999

Keywords

  • IR-63266
  • FMT-PA: PROCESS ALGEBRAS
  • EWI-6397

Cite this

Brinksma, Hendrik. / Cache Consistency by Design. In: Distributed computing. 1999 ; Vol. 12, No. 2/3. pp. 552-565.
@article{88da85d5ed46424982311c47a89b4603,
title = "Cache Consistency by Design",
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.",
keywords = "IR-63266, FMT-PA: PROCESS ALGEBRAS, EWI-6397",
author = "Hendrik Brinksma",
year = "1999",
month = "6",
doi = "10.1007/s004460050058",
language = "Undefined",
volume = "12",
pages = "552--565",
journal = "Distributed computing",
issn = "0178-2770",
publisher = "Springer",
number = "2/3",

}

Brinksma, H 1999, 'Cache Consistency by Design' Distributed computing, vol. 12, no. 2/3, 10.1007/s004460050058, pp. 552-565. https://doi.org/10.1007/s004460050058

Cache Consistency by Design. / Brinksma, Hendrik.

In: Distributed computing, Vol. 12, No. 2/3, 10.1007/s004460050058, 06.1999, p. 552-565.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Cache Consistency by Design

AU - Brinksma, Hendrik

PY - 1999/6

Y1 - 1999/6

N2 - 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.

AB - 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.

KW - IR-63266

KW - FMT-PA: PROCESS ALGEBRAS

KW - EWI-6397

U2 - 10.1007/s004460050058

DO - 10.1007/s004460050058

M3 - Article

VL - 12

SP - 552

EP - 565

JO - Distributed computing

JF - Distributed computing

SN - 0178-2770

IS - 2/3

M1 - 10.1007/s004460050058

ER -