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 -