Summary
A class of parallel coordination programs for a shared memory asynchronous parallel processor is considered. These programs use the operation Fetch & Add which is the basic primitive for the NYU-Ultracomputer. A correctness proof for the considered programs must be done for arbitrary number N of processing elements since the Ultracomputer design includes thousands of PEs.
A reachability set description (RSD) is introduced, in which all reachable states of a program (exponential function of N) are collapsed into a fixed number of metastates. The transitions between these metastates are then specified. By using such notation, it becomes feasible to prove various temporal properties of a parallel program, in particular, the absence of livelock. The concept of a compact parallel program is introduced. Roughly speaking a parallel program executed by N PEs is compact if there exists a boundary T independent of N such that any state of this program is reachable within time T. Compactness may also be understood as the finiteness of the expansion for the strongest invariant in the least fixpoint theory, where such finiteness is uniform over N. A program that builds RSDs for compact parallel programs and examples of proofs generated by this program are discussed.
Similar content being viewed by others
References
Ashcroft, E.A.: Proving assertions about parallel programs. Journ. Comput. System Sci. 10, 110–135 (1975)
Ben-Ari, M.: Temporal logic proofs of concurrent programs. Dept. Appl. Math., Weizmann Institute of Science, Report CS82-12, 1982
Clarke, E.M.: Synthesis of resource invariants for concurrent programs. ACM Trans. on Programming Languages and Systems. 2 (3), 338–358 (1980)
Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with ‘readers’ and ‘writers’. Comm. ACM 14, 667–668 (1971)
Dijkstra, E.M.: Hierarchical orderings of sequential processes. Acta Informat. 1, 115–138 (1971)
Genrich, H.J., Lautenbach, K.: System modeling with high-level Petri Nets. Theor. Comput. Sci. 13, 109–136 (1981)
Gottlieb, A., Grishman, R., Kruskal, C.P., McAuliffe, K.P., Rudolph, L., Snir, M.: The NYU Ultracomputer-designing an MIMD shared memory parallel computer. IEEE Trans. Computers, Vol. C-32, No. 2, February 1983
Gottlieb, A., Lubachevsky, B.D., Rudolph, L.: Basic techniques for the efficient coordination of very large numbers of cooperating sequential processors. ACM Trans, on Comput. Lang. Sys. 5 (2), 164–189 (1983)
Habermann, A.N.: Synchronization of communicating processes. Comm. ACM. 15 (3), 171–176 (1972)
Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135–159 (1979)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. System. Sci. 3, 147–195 (1969)
Kwong, Y.S.: On the absence of livelocks in parallel programs. In: Semantics of Concurrent Computation. (G. Goos, J. Hartmanis, eds.) Proc. of the Int. Symp., Lecture Notes in Computer Science 70, pp. 172–190. Berlin-Heidelberg-New York: Springer 1979
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125–143 (1977)
Lubachevsky, B.D.: Verification of several parallel coordination programs based on descriptions of their reachability sets. Ultracomputer Note # 33, Courant Institute, New York University, July, 1981
Morris, J.M.: A starvation-free solution to the mutual exclusion problem. Information Processing Lett. 8, 76–80 (1979)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, No. 5, p. 279–285 (May 1976)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. I. Acta Informat. 6, 319–340 (1976)
Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang, and Syst. 3, vol. 4 (July 1982)
Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence (B. Meltzer and D. Michie, eds.) 5, 59–78. Edinburgh: University Press 1969
Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput Sci. 13, 45–60 (1981)
Rudolph, L.: Software structures for ultraparallel computings. Ph.D. Thesis, Courant Inst., NYU, 1982
Schwartz, J.T.: Ultracomputers. ACM Trans, on Prog. Lang. Sys. pp. 484–521 (1980)
Schwartz, R.L., and Melliar-Smith, P.M.: Temporal logic specification of distributed systems. Proc. 2-nd Int. Conf. on Distributed Computing Systems, pp. 446–454. Paris, April 1981
Shaw, A.C.: The logical design of operating systems Englwood Cliffs: Prentice-Hall, 1974
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–309
Thau, R.: Private communication.
van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct concurrent programs. Acta Informat. 12, 1–31 (1979)
Author information
Authors and Affiliations
Additional information
This work was supported in part by the Applied Mathematical Sciences Program of the U.S. Department of Energy under Contract No. DE-AC02-76ER03077, and in part by the National Science Foundation under Grant No. NSF-MCS79-21258
Rights and permissions
About this article
Cite this article
Lubachevsky, B.D. An approach to automating the verification of compact parallel coordination programs. I. Acta Informatica 21, 125–169 (1984). https://doi.org/10.1007/BF00289237
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00289237