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 languageEnglish
Pages (from-to)61–74
Number of pages14
JournalDistributed computing
Volume12
Issue number2-3
DOIs
Publication statusPublished - Jun 1999

Fingerprint

Cache
Caching
Data storage equipment
Correctness
Specifications
Memory architecture
Specification
Factorization
Distributed Memory
Transducers
Fairness
Transducer
Semantics
Design
Refinement
Network protocols
Strictly
Higher Order

Keywords

  • FMT-PA: PROCESS ALGEBRAS
  • Formal design
  • Caching protocols
  • Reactive systems
  • Process algebra
  • Correctness preserving
  • Transformations

Cite this

Brinksma, Ed. / Cache consistency by design. In: Distributed computing. 1999 ; Vol. 12, No. 2-3. pp. 61–74.
@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 = "FMT-PA: PROCESS ALGEBRAS, Formal design, Caching protocols, Reactive systems, Process algebra, Correctness preserving, Transformations",
author = "Ed Brinksma",
year = "1999",
month = "6",
doi = "10.1007/s004460050058",
language = "English",
volume = "12",
pages = "61–74",
journal = "Distributed computing",
issn = "0178-2770",
publisher = "Springer",
number = "2-3",

}

Cache consistency by design. / Brinksma, Ed.

In: Distributed computing, Vol. 12, No. 2-3, 06.1999, p. 61–74.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Cache consistency by design

AU - Brinksma, Ed

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 - FMT-PA: PROCESS ALGEBRAS

KW - Formal design

KW - Caching protocols

KW - Reactive systems

KW - Process algebra

KW - Correctness preserving

KW - Transformations

U2 - 10.1007/s004460050058

DO - 10.1007/s004460050058

M3 - Article

VL - 12

SP - 61

EP - 74

JO - Distributed computing

JF - Distributed computing

SN - 0178-2770

IS - 2-3

ER -