Interference Between Communicating Parallel Processes

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.

CACM June, 1972

Gilbert, P.
Chandler, W. J.

concurrent programming control, cooperating processes,
formal programs, interference, mutual exclusion, 
operating systems, parallel processes

4.0 4.10 4.30 4.32 4.42 5.24 6.20

CA720603 JB January 31, 1978  8:44 AM

1781	4	2342
1828	4	2342
1854	4	2342
1877	4	2342
1960	4	2342
2150	4	2342
2150	4	2342
2150	4	2342
2228	4	2342
2228	4	2342
2256	4	2342
2256	4	2342
2317	4	2342
2317	4	2342
2319	4	2342
2377	4	2342
2342	4	2342
2342	4	2342
2342	4	2342
2376	4	2342
2376	4	2342
2379	4	2342
2424	4	2342
2482	4	2342
2618	4	2342
2618	4	2342
2618	4	2342
2632	4	2342
2704	4	2342
2723	4	2342
2738	4	2342
2740	4	2342
2741	4	2342
2867	4	2342
3184	4	2342
3184	4	2342
1198	5	2342
1338	5	2342
1749	5	2342
2342	5	2342
2342	5	2342
2342	5	2342