Logic in Computer Science (LICS 1990)

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

Authors: Goldman, K.J. Lynch, N.A.

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 = 	 {Goldman, K.J. and Lynch, N.A.},
    title = 	 {Modelling shared state in a shared action model},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {450--463},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }