Abstract
This paper describes a semantically-based axiomatic treatment of a parallel programming language with shared variable concurrency and conditional critical regions, essentially the language discussed by Owicki and Gries [20,21]. We use a structural operational semantics for this language, based on work of Hennessy and Plotkin [22,26], and we use the semantic structure to suggest a class of assertions for expressing properties of commands. We then define syntactic operations on assertions which correspond precisely to syntactic constructs of the programming language; in particular, we define sequential and parallel composition of assertions. This enables us to design a truly compositional proof system for program properties. Our proof system is sound and relatively complete. We examine the relationship between our proof system and the Owicki-Gries proof system. Our assertions are more expressive than Owicki's, and her proof outlines correspond roughly to a special subset of our assertion language. Owicki's parallel rule can be thought of as being based on a slightly different form of parallel composition of assertions; our form does not require interference-freedom, and our proof system is relatively complete without the need for auxiliary variables. Connections with other work, including the “Generalized Hoare Logic” of Lamport and Schneider [16,17], and with the Transition Logic of Gerth [11], are discussed briefly.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
8. References
Apt, K. R., Ten Years of Hoare's Logic: A Survey, ACM TOPLAS, vol. 3 no. 4 (October 1981) 431–483.
Apt, K. R., Francez, N., and de Roever, W. P., A proof system for communicating sequential processes, ACM TOPLAS, vol. 2 no. 3 (July 1980), 359–385.
Ashcroft, E. A., Proving assertions about parallel programs, J. Comput. Syst. Sci. 10 (Jan. 1975), 110–135.
Barringer, H., Kuiper, R., and Pnueli, A., Now You May Compose Temporal Logic Assertions, Proc. 16th ACM Symposium on Theory of Computing, Washington, May 1984.
Best, E., A relational framework for concurrent programs using atomic actions, Proc. IFIP TC2 Conference (1982).
Brookes, S. D., On the Relationship of CCS and CSP, Proc. ICALP 83, Springer LNCS (1983).
Brookes, S. D., A Fully Abstract Semantics and Proof System for An ALGOL-like Language with Sharing, CMU Technical Report (1984).
Cook, S., Soundness and Completeness of an Axiom System for Program Verfification, SIAM J. Comput. vol 7. no. 1 (February 1978) 70–90.
Dijkstra, E. W., Cooperating Sequential Processes, in: Programming Languages, F. Genuys (Ed.), Academic Press, NY (1968) 43–112.
Dijkstra, E.W., A Discipline of Programming, Prentice-Hall, New Jersey (1976).
Gerth, R., Transition Logic, Proc. 16th ACM STOC Conference, 1983.
Hoare, C. A. R., An axiomatic basis for computer programming, CACM 12, 10 (Oct. 1969), 576–580.
Hoare, C. A. R., Communicating Sequential Processes, CACM 21, 8 (Aug. 1978).
Jones, C. B., Tentative Steps Towards a Development Method for Interfering Programs, ACM TOPLAS vol. 5 no. 4, (October 1983) 596–619.
Keller, R. M., Formal verification of parallel programs, CACM 19,7 (July 1976).
Lamport, L., The ‘Hoare Logic’ of concurrent programs, Acta Inf. 14 (1980).
Lamport, L., and Schneider, F., The “Hoare Logic” of CSP, and All That, ACM TOPLAS 6, 2 (April 1984), 281–296.
Levin, G. M., and Gries, D., A proof technique for communicating sequential processes, Acta Informatica 15 (1981), 281–302.
Manna, Z., and Pnueli, A., Verification of Concurrent Programs: The Temporal Framework, in: “The Correctness Problem in Computer Science”, ed. R. S. Boyer and J. S. Moore, Academic Press, London (1982).
Owicki, S. S., and Gries, D., An axiomatic proof technique for parallel programs, Acta Informatica 6 (1976), 319–340.
Owicki, S. S., Axiomatic proof techniques for parallel programs, Ph. D. dissertation, Cornell University (Aug. 1975).
Hennessy, M., and Plotkin, G. D., Full Abstraction for a Simple Parallel Programming Language, Proc. MFCS 1979, Springer LNCS vol. 74, pp. 108–120.
Milner, R., Fully Abstract Models of Typed Lambda-Calculi, Theoretical Computer Science (1977).
Milner, R., A Calculus of Communicating Systems, Springer LNCS vol. 92 (1980).
O'Donnell, M., A Critique of the Foundations of Hoare-Style Programming Logic, CACM vol. 25 no. 12 (December 1982) 927–934.
Plotkin, G. D., A Structural Approach to Operational Semantics, DAIMI Report FN-19, Aarhus University (1981).
Plotkin, G. D., An Operational Semantics for CSP, Proceedings of the W. G. 2.2 Conference, 1982.
Winskel, G., Synchronization Trees, Proc. ICALP 1983, Springer LNCS vol. 154.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brookes, S.D. (1985). An axiomatic treatment of a parallel programming language. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_4
Download citation
DOI: https://doi.org/10.1007/3-540-15648-8_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15648-2
Online ISBN: 978-3-540-39527-0
eBook Packages: Springer Book Archive