Reduction: A Method of Proving Properties of Parallel Programs When proving that a parallel program has a given property it is often convenient to assume that a statement is indivisible, i.e. that the statement cannot be interleaved with the rest of the program. Here sufficient conditions are obtained to show that the assumption that a statement is indivisible can be relaxed and still preserve properties such as halting. Thus correctness proofs of a parallel system can often be greatly simplified. CACM December, 1975 Lipton, R. J. deadlock free, reduction, interruptible, indivisible, parallel program, semaphore, verification method, process, computation sequence 4.32 4.35 5.24 CA751207 JB January 5, 1978 3:59 PM 2700 4 2700 3128 4 2700 2376 5 2700 2700 5 2700 2700 5 2700 2700 5 2700