DocumentCode :
2718575
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
fYear :
1990
fDate :
4-7 Jun 1990
Firstpage :
450
Lastpage :
463
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;
fLanguage :
English
Publisher :
ieee
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
Type :
conf
DOI :
10.1109/LICS.1990.113769
Filename :
113769
Link To Document :
بازگشت