Abstract
We consider a parallel Algol-like language, combining the λ-calculus with shared-variable parallelism. We provide a denotational semantics for this language, simultaneously adapting the possible-worlds model of Reynolds and Oles [Rey81, 01e82] to the parallel setting and generalizing the “transition traces” model of [Bro93] to the procedural setting. This semantics supports reasoning about safety and liveness properties of parallel programs, and validates a number of natural laws of program equivalence based on non-interference properties of local variables.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky and T. P. Jensen. A relational approach to strictness analysis for higher-order polymorphic functions. In Conf. Record 18th ACM Symposium on Principles of Programming Languages, pages 49–54. ACM Press, 1991.
S. Brookes. Full abstraction for a shared-variable parallel language. In Proc. 8 th Annual IEEE Symposium on Logic in Computer Science, pages 98–109. IFFF Computer Society Press, June 1993.
J. Y. Halpern, A. R. Meyer, and B. A. Trakhtenbrot. The semantics of local storage, or What makes the free list free? In ACM Symposium on Principles of Programming Languages, pages 245–257, 1983.
J. C. Mitchell and A. Scedrov. Notes on sconing and relators. In E. Boerger, editor, Computer Science Logic ‘82, Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 352–378. Springer-Verlag, 1993.
F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, 1982. See Chapter 11.
P. W. O’Hearn and J.C. Reynolds. From Algol to Polymorphic Linear Lambda-calculus. Talk given at Isaac Newton Institute for Mathematical Sciences, Cambridge, August, 1995.
P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM,42(3):658–709, May 1995. See Chapter 16.
D. Park. On the semantics of fair parallelism. In D. Bjerner, editor, Abstract Software Specifications, volume 86 of Lecture Notes in Computer Science, pages 504–526. Springer-Verlag, 1979.
U. S. Reddy. Global state considered unnecessary: object-based semantics of interference-free imperative programming. In ACM SIGPLAN Workshop on State in Programming Languages. Technical Report YALEU/DCS/RR-968, Department of Computer Science, Yale University, 1993. See Chapter 19.
J. C. Reynolds. The essence of Algol. In Algorithmic Languages,pages 345–372. North-Holland, Amsterdam, 1981. See Chapter 3.
J. C. Reynolds. Types, abstraction, and parametric polymorphism In Information Processing 83,pages 513–523. North-Holland, Amsterdam, 1983.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media New York
About this chapter
Cite this chapter
Brookes, S. (1997). The Essence of Parallel Algol . In: O’Hearn, P.W., Tennent, R.D. (eds) Algol-like Languages. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4757-3851-3_11
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3851-3_11
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4757-3853-7
Online ISBN: 978-1-4757-3851-3
eBook Packages: Springer Book Archive