Paper: Modelling shared state in a shared action model (at LICS 1990)

Authors: Kenneth J. Goldman Nancy A. Lynch

Abstract

The I/O automation model of N.A. Lynch and M.R. Tuttle (1987) is extended to allow modeling of shared memory systems, as well as systems that include both shared memory and shared action communication. A full range of types of atomic accesses to shared memory is allowed, from basic reads and writes to read-modify-write. The extended model supports system description, verification, and analysis. As an example, E.W. Dijkstra's (1965) classical shared memory mutual exclusion algorithm is presented and proven correct

BibTeX

  @InProceedings{GoldmanLynch-Modellingsharedstat,
    author = 	 {Kenneth J. Goldman and Nancy A. Lynch},
    title = 	 {Modelling shared state in a shared action model},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {450--463},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }