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

    81 Downloads (Pure)


    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
    ISSN (Print)0926-4515


    Dive into the research topics of 'Verifying Sequentially Consistent Memory'. Together they form a unique fingerprint.

    Cite this