Skip to main content
SpringerLink
Log in

An axiomatic proof technique for parallel programs I

  • Published:
Acta Informatica Aims and scope Submit manuscript

Summary

A language for parallel programming, with a primitive construct for synchronization and mutual exclusion, is presented. Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language. The proof method lends insight into how one should understand and present parallel programs. Examples are given using several of the standard problems in the literature. Methods for proving termination and the absence of deadlock are also given.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ashcroft, E. A., Manna, Z.: Formalization of properties of parallel programs. Machine Intelligence 6. Edinburgh: University of Edinburgh Press 1971, p. 17–41

    Google Scholar 

  2. Ashcroft, E. A.: Proving assertions about parallel programs. Dept of Computer Science, University of Waterloo, CS 73-01, 1973

  3. Cadiou, J. M., Levy, J. J.: Mechanical proofs about parallel processes. Proc. 14 Annual IEEE Symposium on Switching and Automata Theory, 1973, p. 34–48

  4. Clint, M.: Program proving: coroutines. Acta Informatica 2, 50–63 (1973)

    Google Scholar 

  5. Cook, S. A.: Axiomatic and interpretive semantics for an Algol fragment. Dept. of Computer Science, Toronto, TR 79, 1975.

    Google Scholar 

  6. Dijkstra, E. W. et al.: On-the-fly garbage collection: an exercise in cooperation. In Working Material for the NATO Summer School on Language Hierarchies and Interfaces, Munich, 1975

  7. Gries, D.: An exercise in proving properties of parallel programs. (Submitted to Comm. ACM)

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

    Google Scholar 

  9. Hoare, C. A. R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580 (1969)

    Google Scholar 

  10. Hoare, C. A. R.: Towards a theory of parallel programming. In: Hoare, C. A. R., Perrot, R. H. (eds.): Operating systems techniques. New York: Academic Press 1972

    Google Scholar 

  11. Hoare, C. A. R., Lauer, P. E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica 3, 135–153 (1974)

    Google Scholar 

  12. Lauer, P. E.: Consistent formal theories of the semantics of programming languages. IBM Laboratory Vienna, TR 25.121, 1971

    Google Scholar 

  13. Lipton, R. J.: On synchronization primitive systems. Carnegie Mellon University, PhD Thesis, 1974

  14. Lipton, R. J.: Reduction: a new method for proving properties of systems of processes. Yale Computer Science Research Report 30, 1974

  15. Newton, G.: Proving properties of interacting processes. Acta Informatica

  16. Owicki, S.: Axiomatic proof techniques for parallel programs. Computer Science Dept., Cornell University, PhD thesis, 1975

  17. Rosen, B. K.: Correctness of parallel programs: the Church-Rosser approach. T. J. Watson Research Center, Yorktown Heights (N. Y.), IBM Research Report RC5107, 1974

  18. Dijkstra, E. W.: The structure of the THE multiprogramming system. Comm. ACM 11, 341–347 (1968)

    Google Scholar 

  19. Owicki, S., Gries, D.: Axiomatic proof techniques for parallel programs II. In preparation

Download references

Author information

Authors and Affiliations

  1. Computer Science Dept., Cornell University, 14853, Ithaca, NY, USA

    Susan Owicki

  2. Dept. of Computer Science, Cornell University, Upson Hall, 14850, Ithaca, N.Y., USA

    David Gries

Authors
  1. Susan Owicki
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Gries
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This research was partially supported by National Science Foundation grant GJ-42512.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Owicki, S., Gries, D. An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976). https://doi.org/10.1007/BF00268134

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00268134

Keywords

Search

Navigation