The Essence of Parallel Algol
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.
KeywordsNatural Transformation Complete Lattice Parallel Setting Liveness Property Type Judgement
Unable to display preview. Download preview PDF.
- [AJ91]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.Google Scholar
- [Bro93]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.Google Scholar
- [HMT83]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.Google Scholar
- [MS93]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.Google Scholar
- [01e82]F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, 1982. See Chapter 11.Google Scholar
- [OR95]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.Google Scholar
- [OT95]P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM,42(3):658–709, May 1995. See Chapter 16.Google Scholar
- [Par79]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.Google Scholar
- [Red93]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.Google Scholar
- [Rey81]J. C. Reynolds. The essence of Algol. In Algorithmic Languages,pages 345–372. North-Holland, Amsterdam, 1981. See Chapter 3.Google Scholar
- [Rey83]J. C. Reynolds. Types, abstraction, and parametric polymorphism In Information Processing 83,pages 513–523. North-Holland, Amsterdam, 1983.Google Scholar
- [Tar55]A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.Google Scholar