Cache consistency by design (Invited Address I)

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    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 languageEnglish
    Title of host publicationProtocol Specification, Testing and Verification XIV
    EditorsSon T. Vuong, Samuel T. Chanson
    Place of PublicationLondon, UK
    PublisherChapman & Hall
    Pages53-67
    ISBN (Electronic)978-0-387-34867-4
    ISBN (Print)978-1-4757-6308-9
    DOIs
    Publication statusPublished - 1994
    Event14th International IFIP W.G. 6.1 Symposium on Protocol Specification, Testing and Verification, PSTV 1994 - Vancouver, Canada
    Duration: 7 Jun 199410 Jun 1994
    Conference number: 14

    Publication series

    NameIFIP Advances in Information and Communication Technology
    PublisherSpringer
    ISSN (Print)1868-4238
    ISSN (Electronic)1868-422X

    Conference

    Conference14th International IFIP W.G. 6.1 Symposium on Protocol Specification, Testing and Verification, PSTV 1994
    Abbreviated titlePSTV XIV
    CountryCanada
    CityVancouver
    Period7/06/9410/06/94

      Fingerprint

    Keywords

    • Behaviour expression
    • Label transition system
    • Local cache
    • Process definition
    • Sequential consistency

    Cite this

    Brinksma, E. (1994). Cache consistency by design (Invited Address I). In S. T. Vuong, & S. T. Chanson (Eds.), Protocol Specification, Testing and Verification XIV (pp. 53-67). (IFIP Advances in Information and Communication Technology). London, UK: Chapman & Hall. https://doi.org/10.1007/978-0-387-34867-4_4