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

    13 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

    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.