The Essence of Parallel Algol

  • Stephen Brookes
Part of the Progress in Theoretical Computer Science book series (PTCS)

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.

Keywords

Natural Transformation Complete Lattice Parallel Setting Liveness Property Type Judgement 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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
  2. [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
  3. [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
  4. [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
  5. [01e82]
    F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, 1982. See Chapter 11.Google Scholar
  6. [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
  7. [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
  8. [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
  9. [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
  10. [Rey81]
    J. C. Reynolds. The essence of Algol. In Algorithmic Languages,pages 345–372. North-Holland, Amsterdam, 1981. See Chapter 3.Google Scholar
  11. [Rey83]
    J. C. Reynolds. Types, abstraction, and parametric polymorphism In Information Processing 83,pages 513–523. North-Holland, Amsterdam, 1983.Google Scholar
  12. [Tar55]
    A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.Google Scholar

Copyright information

© Springer Science+Business Media New York 1997

Authors and Affiliations

  • Stephen Brookes

There are no affiliations available

Personalised recommendations