Reduction: a new method of proving properties of systems of processes

ABSTRACT

When proving that a system of processes has a given property it is often convenient to assume that a routine is uninterruptible, i.e. that the routine cannot be interleaved with the rest of the system. Here sufficient conditions are obtained to show that the assumption that a routine is uninterruptible can be relaxed and still preserve basic properties such as halting and determinacy. Thus correctness proofs of a system of processes can often be greatly simplified. This technique - called reduction - is viewed as the replacement of an interruptible routine by an uninterruptible one.

REFERENCES

• 1: R. W. Floyd. Assigning meanings to programs. Mathematical Aspects of Computer Science. American Mathematics Society: 19-32 (1967).
• 2: K. N. Levitt. The application of program-proving techniques to the verification of synchronization processes. AFIPS (1972): 33-47.
• 3: Hugh Conrad Lauer, Correctness in operating systems, 1973
• 4: E. A. Ashcroft. Proving Assertions about Parallel Programs, Research Report CS-73-01, Department of Applied Analysis and Computer Science, University of Waterloo, 1973.
• 5: R. J. Lipton, Limitations of Synchronization Primitives. Yale Computer Science Report no. 31, 1974.
• 6: E. W. Dijkstra. Cooperating Sequential Processes, Programming Languages. Edited by F. Genuys. 43-112.
• 7: Barbara H. Liskov, The design of the Venus operating system, Communications of the ACM, v.15 n.3, p.144-149, March 1972 [doi>10.1145/361268.361272]
• 8: R. M. Karp, R. E. Miller. Parallel Program Schemata. JCSS 3(2): 147-195.
• 9: R. J. Lipton. On Synchronization Primitive Systems. Yale Computer Science Report no. 22, 1974.
• 10: A. Nico Habermann, Synchronization of communicating processes, Communications of the ACM, v.15 n.3, p.171-176, March 1972 [doi>10.1145/361268.361277]