Principles of proving concurrent programs in Gypsy

ABSTRACT

Concurrency in Gypsy is based on a unique, formal approach to specifying and proving systems of concurrent processes. The specification and proof methods are designed so that proofs of individual processes are totally independent, even when operating concurrently. These methods can be applied both to terminating and non-terminating processes, and the proof methods are well suited to automated verification aids. The basic principles of these methods and their interaction with the design of Gypsy are described.

REFERENCES

• 1: Per Brinch Hansen, Operating System Principles, Prentice Hall PTR, Upper Saddle River, NJ, 1973
• 2: Per Brinch Hansen, The purpose of concurrent Pascal, Proceedings of the international conference on Reliable software, p.305-309, April 21-23, 1975, Los Angeles, California
• 3: {Cohen, 78} R. M. Cohen. "Formal Specifications for Real-time Systems" in Seventh Texas Conference on Computing Systems, October, 1978.
• 4: {Dijkstra, 68} E. W. Dijkstra. "Cooperating Sequential Processes", in Programming Languages, Academic Press, 1968.
• 5: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 6: {Good, 78} D. I. Good, R. M. Cohen, C. G. Hoch, L. W. Hunter, D. F. Hare. "Report on the Language Gypsy, Version 2.0", ICSCA-CMP-10, Certifiable Minicomputer Project, ICSCA, The University of Texas at Austin, May, 1978.
• 7: 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]
• 8: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 9: {Horn, 77} Gary B. Horn. "Specifications for a Secure Computer Communications Network", ICSCA-CMP-8, The University of Texas at Austin, 1977.
• 10: John H. Howard, Proving monitors, Communications of the ACM, v.19 n.5, p.273-279, May 1976 [doi>10.1145/360051.360079]
• 11: Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
• 12: Anita K. Jones , Barbara H. Liskov, A language extension for expressing constraints on data access, Communications of the ACM, v.21 n.5, p.358-367, May 1978 [doi>10.1145/359488.359493]
• 13: {Manna, 78} Z. Manna and R. Waldinger. "Is 'Sometimes' better than 'Always'?", CACM, 21, 2, February, 1978.
• 14: Susan Speer Owicki, Axiomatic proof techniques for parallel programs., 1975
• 15: {Owicki, 76} S. S. Owicki, D. Gries. "An Axiomatic Proof Technique for Parallel Programs I", Acta Informatica, vol. 6, 1976.
• 16: {Wells, 76} R. E. Wells. "Specification and Implementation of a Verifiable Communications System", Master's Thesis, The University of Texas at Austin, December, 1976.
• 17: {Wirth, 77} N. Wirth. "Modula: a Language for Modular Multiprogramming", in Software Practice & Experience, Vol 7, 3-35, 1977.
• 18: W. Wulf , R. Levin , C. Pierson, Overview of the Hydra Operating System development, Proceedings of the fifth ACM symposium on Operating systems principles, p.122-131, November 19-21, 1975, Austin, Texas, United States

INDEX TERMS

Keywords:
concurrency, formal specifications, message buffers, parallel programs, program proving, program verification