Formal verification of parallel programs

ABSTRACT

Two formal models for parallel computation are presented: an abstract conceptual model and a parallel-program model. The former model does not distinguish between control and data states. The latter model includes the capability for the representation of an infinite set of control states by allowing there to be arbitrarily many instruction pointers (or processes) executing the program. An induction principle is presented which treats the control and data state sets on the same ground. Through the use of “place variables,” it is observed that certain correctness conditions can be expressed without enumeration of the set of all possible control states. Examples are presented in which the induction principle is used to demonstrate proofs of mutual exclusion. It is shown that assertions-oriented proof methods are special cases of the induction principle. A special case of the assertions method, which is called parallel place assertions, is shown to be incomplete. A formalization of “deadlock” is then presented. The concept of a “norm” is introduced, which yields an extension, to the deadlock problem, of Floyd's technique for proving termination. Also discussed is an extension of the program model which allows each process to have its own local variables and permits shared global variables. Correctness of certain forms of implementation is also discussed. An Appendix is included which relates this work to previous work on the satisfiability of certain logical formulas.

REFERENCES

• 1: Ashcroft, E., and Manna, Z. Formalization of properties of parallel programs. Machine Intelligence 6 (1970) 17-41.
• 2: Ashcroft, E.A. Proving assertions about parallel programs. J. Comp. Sys. Sci. 10, 1 (Jan. 1975), 110-135.
• 3: Brinch Hansen, P. A comparison of two synchronizing concepts. Acta lnformatica 1 (1972), 190-199.
• 4: Conway, M. A multiprocessor system design. AFIPS Conf. Proc., VoL 24, AFIPS Press, Montvale, N.J., 1963, pp. 139-148.
• 5: 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]
• 6: Dijkstra, E.W. Hierarchical ordering of sequential processes. Acta Informatica I (1971), 115-138.
• 7: Floyd, R.W. Assigning meanings to programs. Proc. Syrup. in Appl. Math, Vol. 19, Amer. Math. Sot., Provincetown, R.I., 1967, pp. 19-32.
• 8: A. N. Habermann, Prevention of system deadlocks, Communications of the ACM, v.12 n.7, p.373-ff., July 1969 [doi>10.1145/363156.363160]
• 9: 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]
• 10: Hoare, C.A.R. Towards a theory of parallel programming. In Operating Systems Techniques, Hoare and Perrot (Eds.), Academic Press, New York, 1972, pp. 61-71.
• 11: Holt, A., and Commoner, F. Events and conditions. Record of the Project MAC Conference on Concurrent Systems and Parallel Computation, June 1970, pp. 3-52.
• 12: Holt, R.C. On deadlock in computer systems. Tech. Rep. CSRG-6, Computer Systems Research Group, U. of Toronto, Apil 1971.
• 13: IBM PL/I Reference Manual, Form C28-8201-1, March 1968.
• 14: Karp, R.M., and Miller, R.E. Parallel program schemata, J. Computer Sci. 3 (May 1969), 147-195.
• 15: Robert M. Keller, Parallel Program Schemata and Maximal Parallelism I. Fundamental Results, Journal of the ACM (JACM), v.20 n.3, p.514-537, July 1973 [doi>10.1145/321765.321782]
• 16: Keller, R.M. Vector replacement systems: a formalism for modeling asynchronous systems. TR 117, Computer Sci. Lab., Dep. of Electrical Eng., Princeton U., Dec. 1972 (revised Jan. 1974).
• 17: Robert M. Keller, A Fundamental Tehoerem of Asynchronous Parallel Computation, Proceedings of the Sagamore Computer Conference on Parallel Processing, p.102-112, August 20-23, 1974
• 18: Keller, R.M. Generalized Petri nets as models for system verification (to appear).
• 19: Hugh Conrad Lauer, Correctness in operating systems, 1973
• 20: Levitt, K.N. The application of program-proving techniques to the verification of synchronization processes, AFIPS Conference Proc., Vol. 41, 1972 FJCC, AFIPS Press, Montvale, N.J., 1972, pp. 33-47.
• 21: Lipton, R.J. Reduction: A method of proving properties of systems of processes. Research Rep. No. 40, Yale U. Dep. of Computer Sci., March 1975.

INDEX TERMS

Keywords:
Petri nets, assertions, correctness, deadlock, mutual exclusion, parallel program, verification