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