Access Restriction

Author Gilbert, Philip ♦ Chandler, W. J.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Concurrent programming control ♦ Operating systems ♦ Cooperating processes ♦ Parallel processes ♦ Interference ♦ Formal programs ♦ Mutual exclusion
Abstract Various kinds of interference between communicating parallel processes have been examined by Dijkstra, Knuth, and others. Solutions have been given for the mutual exclusion problem and associated subproblems, in the form of parallel programs, and informal proofs of correctness have been given for these solutions.In this paper a system of parallel processes is regarded as a machine which proceeds from one state S (i.e. a collection of pertinent data values and process configurations) to a next state S′ in accordance with a transition rule S ⇒ S′.A set of such rules yields sequences of states, which dictate the system's behavior. The mutual exclusion problem and the associated subproblems are formulated as questions of inclusion between sets of states, or of the existence of certain sequences. A mechanical proof procedure is shown, which will either verify (prove the correctness of) or discredit (prove the incorrectness of) an attempted solution, with respect to any of the interference properties.It is shown how to calculate transition rules from the “partial rules” by which the individual processes operate. The formation of partial rules and the calculation of transition rules are both applicable to hardware processes as well as to software processes, and symmetry between processes is not required.
Description Affiliation: Univ. of Southern California, Los Angeles (Gilbert, Philip; Chandler, W. J.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 15
Issue Number 6
Page Count 11
Starting Page 427
Ending Page 437

Open content in new tab

   Open content in new tab
Source: ACM Digital Library