Modelling Shared State in a Shared Action Model
Abstract
The input/output automation model of Lynch and Tuttle is extended to allow modelling 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. As an example, Dijkstra's classical shared memory mutual exclusion algorithm is presented and proved correct. Keywords: Distributed computing; Distributed algorithms; Mutual exclusion; Input/output; Automata.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 15, 1990
- Accession Number
- ADA221279
Entities
People
- Kenneth Goldman
- Nancy Lynch
Organizations
- Massachusetts Institute of Technology