Verifying Sequentially Consistent Memory

Ed Brinksma, Jim Davies, Rob Gerth, Susanne Graf, Wil Janssen, Bengt Jonsson, Shmuel Katz, Gavin Lowe, Mannes Poel, Amir Pnueli, Camilla Rump, Job Zwiers

    Research output: Book/ReportBookProfessional

    5 Downloads (Pure)

    Abstract

    In distributed shared memory architectures, memory usually obeys weaker constraints than that of ordinary memory in (cache-less) single processor systems. One popular weakening is that of sequential consistency. Proving that a memory is sequentialy consistent does not easily fit the standard refinement and verification strategies. This paper takes a sequential consistent memory-the lazy caching protocol-and verifies it using a number of verification approaches. In almost all cases, existing approaches have to be generalized first.
    Original languageEnglish
    Place of PublicationEindhoven
    PublisherTechnische Universiteit Eindhoven, Wiskunde & Informatica
    Number of pages160
    Publication statusPublished - 1994

    Publication series

    NameComputing Science Report
    PublisherEindhoven University of Technology
    No.94/44
    ISSN (Print)0926-4515

    Fingerprint

    Data storage equipment
    Memory architecture
    Network protocols

    Cite this

    Brinksma, E., Davies, J., Gerth, R., Graf, S., Janssen, W., Jonsson, B., ... Zwiers, J. (1994). Verifying Sequentially Consistent Memory. (Computing Science Report; No. 94/44). Eindhoven: Technische Universiteit Eindhoven, Wiskunde & Informatica.
    Brinksma, Ed ; Davies, Jim ; Gerth, Rob ; Graf, Susanne ; Janssen, Wil ; Jonsson, Bengt ; Katz, Shmuel ; Lowe, Gavin ; Poel, Mannes ; Pnueli, Amir ; Rump, Camilla ; Zwiers, Job. / Verifying Sequentially Consistent Memory. Eindhoven : Technische Universiteit Eindhoven, Wiskunde & Informatica, 1994. 160 p. (Computing Science Report; 94/44).
    @book{3e8ebeadb46d453bb7ba1db8b2d08f06,
    title = "Verifying Sequentially Consistent Memory",
    abstract = "In distributed shared memory architectures, memory usually obeys weaker constraints than that of ordinary memory in (cache-less) single processor systems. One popular weakening is that of sequential consistency. Proving that a memory is sequentialy consistent does not easily fit the standard refinement and verification strategies. This paper takes a sequential consistent memory-the lazy caching protocol-and verifies it using a number of verification approaches. In almost all cases, existing approaches have to be generalized first.",
    author = "Ed Brinksma and Jim Davies and Rob Gerth and Susanne Graf and Wil Janssen and Bengt Jonsson and Shmuel Katz and Gavin Lowe and Mannes Poel and Amir Pnueli and Camilla Rump and Job Zwiers",
    year = "1994",
    language = "English",
    series = "Computing Science Report",
    publisher = "Technische Universiteit Eindhoven, Wiskunde & Informatica",
    number = "94/44",

    }

    Brinksma, E, Davies, J, Gerth, R, Graf, S, Janssen, W, Jonsson, B, Katz, S, Lowe, G, Poel, M, Pnueli, A, Rump, C & Zwiers, J 1994, Verifying Sequentially Consistent Memory. Computing Science Report, no. 94/44, Technische Universiteit Eindhoven, Wiskunde & Informatica, Eindhoven.

    Verifying Sequentially Consistent Memory. / Brinksma, Ed; Davies, Jim; Gerth, Rob; Graf, Susanne; Janssen, Wil; Jonsson, Bengt; Katz, Shmuel; Lowe, Gavin; Poel, Mannes; Pnueli, Amir; Rump, Camilla; Zwiers, Job.

    Eindhoven : Technische Universiteit Eindhoven, Wiskunde & Informatica, 1994. 160 p. (Computing Science Report; No. 94/44).

    Research output: Book/ReportBookProfessional

    TY - BOOK

    T1 - Verifying Sequentially Consistent Memory

    AU - Brinksma, Ed

    AU - Davies, Jim

    AU - Gerth, Rob

    AU - Graf, Susanne

    AU - Janssen, Wil

    AU - Jonsson, Bengt

    AU - Katz, Shmuel

    AU - Lowe, Gavin

    AU - Poel, Mannes

    AU - Pnueli, Amir

    AU - Rump, Camilla

    AU - Zwiers, Job

    PY - 1994

    Y1 - 1994

    N2 - In distributed shared memory architectures, memory usually obeys weaker constraints than that of ordinary memory in (cache-less) single processor systems. One popular weakening is that of sequential consistency. Proving that a memory is sequentialy consistent does not easily fit the standard refinement and verification strategies. This paper takes a sequential consistent memory-the lazy caching protocol-and verifies it using a number of verification approaches. In almost all cases, existing approaches have to be generalized first.

    AB - In distributed shared memory architectures, memory usually obeys weaker constraints than that of ordinary memory in (cache-less) single processor systems. One popular weakening is that of sequential consistency. Proving that a memory is sequentialy consistent does not easily fit the standard refinement and verification strategies. This paper takes a sequential consistent memory-the lazy caching protocol-and verifies it using a number of verification approaches. In almost all cases, existing approaches have to be generalized first.

    M3 - Book

    T3 - Computing Science Report

    BT - Verifying Sequentially Consistent Memory

    PB - Technische Universiteit Eindhoven, Wiskunde & Informatica

    CY - Eindhoven

    ER -

    Brinksma E, Davies J, Gerth R, Graf S, Janssen W, Jonsson B et al. Verifying Sequentially Consistent Memory. Eindhoven: Technische Universiteit Eindhoven, Wiskunde & Informatica, 1994. 160 p. (Computing Science Report; 94/44).