Abstract
A parallel program, Dijkstra's on-the-fly garbage collector, is proved correct using a proof method developed by Owicki. The fine degree of interleaving in this program makes it especially difficult to understand, and complicates the proof greatly. Difficulties with proving such parallel programs correct are discussed.
This research was partially supported by the National Science Foundation under grant GJ-42512.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Dijkstra, E.W., et al. On-the-fly garbage collection: an exercise in cooperation. In this volume.
Hoare, C.A.R. An axiomatic basis for computer programming. CACM 12 (Oct 1969), 576–583.
Owicki, S. Axiomatic Proof Techniques for Parallel Programs. TR 75-251, Dept. of Computer Science, Cornell University, July 1975 (PhD thesis).
Dijkstra, E.W. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. CACM 18 (Aug 1975), 453–457.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1976 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gries, D. (1976). An exercise in proving parallel programs correct. In: Bauer, F.L., et al. Language Hierarchies and Interfaces. Lecture Notes in Computer Science, vol 46. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-07994-7_49
Download citation
DOI: https://doi.org/10.1007/3-540-07994-7_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-07994-1
Online ISBN: 978-3-540-37972-0
eBook Packages: Springer Book Archive