An operational semantics for parallel lazy evaluation

ABSTRACT

We present an operational semantics for parallel lazy evaluation that accurately models the parallel behaviour of the non-strict parallel functional language GpH. Parallelism is modelled synchronously, that is, single reductions are carried out separately then combined before proceeding to the next set of reductions. Consequently the semantics has two levels, with transition rules for individual threads at one level and combining rules at the other. Each parallel thread is modelled by a binding labelled with an indication of its activity status. To the best of our knowledge this is the first semantics that models such thread states. A set of labelled bindings corresponds to a heap and is used to model sharing.The semantics is set at a higher level of abstraction than an abstract machine and is therefore more manageable for proofs about programs rather than implementations. At the same time, it is sufficiently low level to allow us to reason about programs in terms of parallelism (i.e. the number of processors used) as well as work and run-time with different numbers of processors.The framework used by the semantics is sufficiently flexible and general that it can easily be adapted to express other evaluation models such as sequential call-by-need, speculative evaluation, non-deterministic choice and others.

REFERENCES

• 1: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 2: S. Aditya, Arvind, L. Augustsson, J.-W. Maessen, and R. S. Nikhil. Semantics of pH: A parallel dialect of Haskell. In Proceedings of the Haskell Workshop, pages 35-49, La Jolla, California, 1995.
• 3: Zena M. Ariola , John Maraist , Martin Odersky , Matthias Felleisen , Philip Wadler, A call-by-need lambda calculus, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-246, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199507]
• 4: Clement A. Baker-Finch, An Abstract Machine for Parallel Lazy Evaluation, Selected papers from the 1st Scottish Functional Programming Workshop (SFP99), p.154-160, August 29-September 01, 1999
• 5: C. Baker-Finch, D. J. King, J. G. Hall, and P. Trinder. An operational semantics for parallel call-by-need. Technical Report No. 99/1, Department of Computing, The Open University, Milton Keynes, 1999.
• 6: Dave Berry , Robin Milner , David N. Turner, A semantics for ML concurrency primitives, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-129, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143191]
• 7: Guy E. Blelloch , Phillip B. Gibbons , Girija J. Narlikar , Yossi Matias, Space-efficient scheduling of parallelism with synchronization variables, Proceedings of the ninth annual ACM symposium on Parallel algorithms and architectures, p.12-23, June 23-25, 1997, Newport, Rhode Island, United States [doi>10.1145/258492.258494]
• 8: Guy E. Blelloch , John Greiner, A provable time and space efficient implementation of NESL, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.213-225, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 9: Robert D. Blumofe , Charles E. Leiserson, Space-Efficient Scheduling of Multithreaded Computations, SIAM Journal on Computing, v.27 n.1, p.202-229, Feb. 1998 [doi>10.1137/S0097539793259471]
• 10: S. Breitinger, R. Loogen, Y. Ortega-Mallen, and R. Pena. Eden: Language Definition and Operational Semantics. Fachbereich Mathematik und Informatik, Philipps Universit. at Marburg, 1998. Technical Report 96-10.
• 11: Manual M. T. Chakravarty , Yike Guo , Martin Köhler , Hendrik C. R. Lock, GOFFIN: higher-order functions meet concurrent constraints, Science of Computer Programming, v.30 n.1-2, p.157-199, Jan. 1998 [doi>10.1016/S0167-6423(97)00010-5]
• 12: D. L. Eager , J. Zahorjan , E. D. Lozowska, Speedup Versus Efficiency in Parallel Systems, IEEE Transactions on Computers, v.38 n.3, p.408-423, March 1989 [doi>10.1109/12.21127]
• 13: Cormac Flanagan , Matthias Felleisen, The semantics of future and its use in program optimization, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.209-220, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199484]
• 14: J. Greiner. Semantics-based parallel cost models and their use in provably efficient implementations. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, 1997.
• 15: John Greiner , Guy E. Blelloch, A provably time-efficient parallel implementation of full speculation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.2, p.240-285, March 1999 [doi>10.1145/316686.316690]
• 16: J. Gustavsson and D. Sands. A foundation for space-safe transformations of call-by-need programs. In The Third International Workshop on Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.
• 17: Jon G. Hall , Clement A. Baker-Finch , Philip W. Trinder , David J. King, Towards an Operational Semantics for a Parallel Non-Strict Functional Language, Selected Papers from the 10th International Workshop on 10th International Workshop, p.54-71, September 09-11, 1998
• 18: Matthew Hennessy, The semantics of programming languages: an elementary introduction using structural operational semantics, John Wiley & Sons, Inc., New York, NY, 1990
• 19: Mercedes Hidalgo-Herrero , Yolanda Ortega-Mallén, A distributed operational semantics for a parallel functional language, Selected papers from the 2nd Scottish Functional Programming Workshop (SFP00), p.89-102, July 26-28, 2000
• 20: M. B. Josephs, The semantics of lazy functional languages, Theoretical Computer Science, v.68 n.1, p.105-111, Oct. 16, 1989 [doi>10.1016/0304-3975(89)90122-9]
• 21: John Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.144-154, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158618]
• 22: H.-W. Loidl. Granularity in Large-Scale Parallel Functional Programming. PhD thesis, Department of Computing Science, University ofGlasgow, 1998.
• 23: J. McCarthy. A basis for a mathematical theory of computation. In Proc. Western Joint Computer Conference, pages 225-238, 1961.
• 24: Andrew Moran , David Sands, Improvement in a lazy context: an operational theory for call-by-need, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292547]
• 25: A. K. Moran. Call-by-name, Call-by-need, and McCarthy's Amb. PhD thesis, Computing Science Department, Chalmers University, 1998.
• 26: Luc Moreau, The PCKS-Machine: An Abstract Machine for Sound Evaluation of Parallel Functional Programs with First-Class Continuations, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.424-438, April 11-13, 1994
• 27: Luc Moreau, The semantics of Scheme with future, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.146-156, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 28: G. D. Plotkin. Call-by-name, call-by-value and the -calculus. Theoretical Computer Science, 1(2):125-159, 1975.
• 29: S. Purushothaman , Jill Seaman, An adequate operational semantics of sharing in lazy evaluation, Symposium proceedings on 4th European symposium on programming, p.435-450, January 1992, Rennes, France
• 30: J. H. Reppy. An operational semantics of first-class synchronous operations. Technical report, Department of Computer Science, Cornell University, 1991.
• 31: P. Roe.Parallel programming using functional languages. PhD thesis, Department of Computing Science, University of Glasgow, Glasgow, Scotland, 1991.
• 32: C. Runciman and D. Wakeling. Profiling parallel functional computations (without parallel machines). In Proceedings of the 1993 Glasgow Workshop on Functional Programming, pages 236-251, Ayr, Scotland, 1994.
• 33: Peter Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming, v.7 n.3, p.231-264, May 1997 [doi>10.1017/S0956796897002712]
• 34: P. W. Trinder , K. Hammond , H.-W. Loidl , S. L. Peyton Jones, Algorithm + strategy = parallelism, Journal of Functional Programming, v.8 n.1, p.23-60, January 1998 [doi>10.1017/S0956796897002967]
• 35: P. W. Trinder , K. Hammond , J. S. Mattson, Jr. , A. S. Partridge , S. L. Peyton Jones, GUM: a portable parallel implementation of Haskell, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.79-88, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 36: Christopher D. Walton, An Abstract Machine for Memory Management, Selected papers from the 1st Scottish Functional Programming Workshop (SFP99), p.89-97, August 29-September 01, 1999

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Frameworks
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Threads

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Sequencing and scheduling

General Terms:
Design, Languages, Performance, Theory, Verification