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

    Keywords

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

    Fingerprint Dive into the research topics of 'Cache consistency by design'. Together they form a unique fingerprint.

  • Cite this