article

An approach to automating the verification of compact parallel coordination programs. I

Author:

Boris D. LubachevskyAuthors Info & Claims

Acta Informatica, Volume 21, Issue 2

Pages 125 - 169

https://doi.org/10.1007/BF00289237

Published: 01 August 1984 Publication History

Abstract

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.

References

[1]

Ashcroft, E.A.: Proving assertions about parallel programs. Journ. Comput. System Sci. 10, 110---135 (1975)

Digital Library

[2]

Ben-Ari, M.: Temporal logic proofs of concurrent programs. Dept. Appl. Math., Weizmann Institute of Science, Report CS82-12, 1982

[3]

Clarke, E.M.: Synthesis of resource invariants for concurrent programs. ACM Trans. on Programming Languages and Systems. 2 (3), 338---358 (1980)

Digital Library

[4]

Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with `readers' and `writers'. Comm. ACM 14, 667---668 (1971)

Digital Library

[5]

Dijkstra, E.M.: Hierarchical orderings of sequential processes. Acta Informat. 1, 115---138 (1971)

Digital Library

[6]

Genrich, H.J., Lautenbach, K.: System modeling with high-level Petri Nets. Theor. Comput. Sci. 13, 109---136 (1981)

[7]

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

[8]

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)

Digital Library

[9]

Habermann, A.N.: Synchronization of communicating processes. Comm. ACM. 15 (3), 171---176 (1972)

Digital Library

[10]

Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135---159 (1979)

[11]

Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. System. Sci. 3, 147---195 (1969)

Digital Library

[12]

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

[13]

Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125---143 (1977)

Digital Library

[14]

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

[15]

Morris, J.M.: A starvation-free solution to the mutual exclusion problem. Information Processing Lett. 8, 76---80 (1979)

[16]

Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, No. 5, p. 279---285 (May 1976)

Digital Library

[17]

Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. I. Acta Informat. 6, 319---340 (1976)

Digital Library

[18]

Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang, and Syst. 3, vol. 4 (July 1982)

[19]

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

[20]

Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput Sci. 13, 45---60 (1981)

[21]

Rudolph, L.: Software structures for ultraparallel computings. Ph.D. Thesis, Courant Inst., NYU, 1982

[22]

Schwartz, J.T.: Ultracomputers. ACM Trans, on Prog. Lang. Sys. pp. 484---521 (1980)

[23]

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

[24]

Shaw, A.C.: The logical design of operating systems Englwood Cliffs: Prentice-Hall, 1974

[25]

Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285---309

[26]

Thau, R.: Private communication.

[27]

van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct concurrent programs. Acta Informat. 12, 1---31 (1979)

Digital Library

Cited By

Wagner CJaber NSamanta R(2023)Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded RegionsProceedings of the ACM on Programming Languages10.1145/35860337:OOPSLA1(172-200)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586033
Lowe G(2022)Parameterized verification of systems with component identities, using view abstractionInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-022-00648-024:2(287-324)Online publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1007/s10009-022-00648-0
Farooqi MPericàs M(2021)Vectorized Barrier and Reduction in LLVM OpenMP RuntimeOpenMP: Enabling Massive Node-Level Parallelism10.1007/978-3-030-85262-7_2(18-32)Online publication date: 14-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-85262-7_2
Show More Cited By

An approach to automating the verification of compact parallel coordination programs. I
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
2. Theory of computation
  1. Models of computation
    1. Concurrency

Recommendations

Formal verification of parallel programs

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 ...
Protocol-based verification of message-passing parallel programs
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as ...
Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Acta Informatica

Acta Informatica Volume 21, Issue 2

August 1984

100 pages

ISSN:0001-5903

Issue’s Table of Contents

Copyright © Copyright © 1984 Springer-Verlag.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 August 1984

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wagner CJaber NSamanta R(2023)Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded RegionsProceedings of the ACM on Programming Languages10.1145/35860337:OOPSLA1(172-200)Online publication date: 6-Apr-2023
Lowe G(2022)Parameterized verification of systems with component identities, using view abstractionInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-022-00648-024:2(287-324)Online publication date: 1-Apr-2022
Farooqi MPericàs M(2021)Vectorized Barrier and Reduction in LLVM OpenMP RuntimeOpenMP: Enabling Massive Node-Level Parallelism10.1007/978-3-030-85262-7_2(18-32)Online publication date: 14-Sep-2021
Konnov ILazić MVeith HWidder J(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/3093333.300986052:1(719-734)Online publication date: 1-Jan-2017
Konnov ILazić MVeith HWidder JCastagna GGordon A(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009860(719-734)Online publication date: 1-Jan-2017
Konnov IVeith HWidder J(2017)On the completeness of bounded model checking for threshold-based distributed algorithmsInformation and Computation10.1016/j.ic.2016.03.006252:C(95-109)Online publication date: 1-Feb-2017
Konnov ILazić MVeith HWidder J(2017)Para$$^2$$2Formal Methods in System Design10.1007/s10703-017-0297-451:2(270-307)Online publication date: 1-Nov-2017
Castagna GGordon A(2017)Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesundefinedOnline publication date: 1-Jan-2017
Plotkin GBjørner NLopes NRybalchenko AVarghese G(2016)Scaling network verification using symmetry and surgeryACM SIGPLAN Notices10.1145/2914770.283765751:1(69-83)Online publication date: 11-Jan-2016
Plotkin GBjørner NLopes NRybalchenko AVarghese GBodik RMajumdar R(2016)Scaling network verification using symmetry and surgeryProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837657(69-83)Online publication date: 11-Jan-2016
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents