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