Title :
Modelling shared state in a shared action model
Author :
Goldman, Kenneth J. ; Lynch, Nancy A.
Author_Institution :
Lab. for Comput. Sci., MIT, Cambridge, MA, USA
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
Keywords :
automata theory; I/O automation model; asynchronous concurrent systems; atomic accesses to shared memory; read-modify-write; shared action communication; shared action model; shared memory mutual exclusion algorithm; shared memory systems; system description; verification; Automata; Computer science; Contracts; Distributed algorithms; Interleaved codes; Laboratories; Message passing; Out of order; Read-write memory; Safety;
Conference_Titel :
Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
Conference_Location :
Philadelphia, PA
Print_ISBN :
0-8186-2073-0
DOI :
10.1109/LICS.1990.113769
