Parallel program correctness through refinement

ABSTRACT

We develop a theory for the correctness of asynchronous parallel programs. A program is considered correct if its behavior is in some sense similar to that of an abstract version of the program. We discuss various criteria for this similarity. We then concentrate on one of them and develop a technique for showing that a parallel program is correct with respect to this criterion.

REFERENCES

• 1: P. J. Courtois , F. Heymans , D. L. Parnas, Concurrent control with “readers” and “writers”, Communications of the ACM, v.14 n.10, p.667-668, Oct. 1971 [doi>10.1145/362759.362813]
• 2: Dijkstra, E. W. "Notes on Structured Programming", in Structured Programming, by Dahl, Dijkstra, and Hoare, Academic Press (1972).
• 3: Edsger W. Dijkstra , Leslie Lamport , A. J. Martin , C. S. Scholten , E. F. M. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, v.21 n.11, p.966-975, Nov. 1978 [doi>10.1145/359642.359655]
• 4: Doeppner, T. W., Jr., and Keller, R. M. On the Relevance of Abstract Models in Modeling Semaphore Implementations. Princeton University, Dept. of Electrical Engineering, Computer Science Laboratory Technical Report TR 193 (October 1975).
• 5: Gries, D. On Structured Programming - A Reply to Smoliar. In ACM Forum, Communications of the ACM, vol. 17, no. 11 (November 1974)
• 6: R. Infante , U. Montanary, Proving structured programs correct, level by level, Proceedings of the international conference on Reliable software, p.427-436, April 21-23, 1975, Los Angeles, California
• 7: Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
• 8: Lamport, L. On-the-Fly Garbage Collection: Once More with Rigor. Massachusetts Computer Associates CA-7508-1611 (August 1975).
• 9: Lamport, L. Proving the Correctness of Multi-processing Programs. Massachusetts Computer Associates CA-7508-0111 (August 1975).
• 10: R. J. Lipton, Limitations of synchronization primitives with conditional branching and global variables, Proceedings of the sixth annual ACM symposium on Theory of computing, p.230-241, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803900]
• 11: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 12: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 13: Rosen, B. K. Correctness of Parallel Programs: The Church-Rosser Approach. IBM Research Report RC5107 (October 1974).