The spineless tagless G-machine, naturally

ABSTRACT

The application of natural semantic specifications of lazy evaluation to areas such as usage analysis, formal profiling and abstract machine construction has shown it to be a useful formalism. This paper introduces several variants and extensions of this specification.The first variant is derived from observations of the Spineless Tagless G-machine (STG), used in the Glasgow Haskell compiler. We present a modified natural semantic specification which can be formally manipulated to derive an STG-like machine.The second variant is the development of a natural semantic specification which allows functions to be applied to more than one argument at once. The STG and TIM abstract machines both allow this kind of behaviour, and we illustrate a use of this semantics by again modifying this semantics following observations of the STG machine. The resulting semantics can be used to formally derive the STG machine. This effectively proves the STG machine correct with respect to Launchbury's semantics.En route, we also show that update markers in the STG machine are necessary for termination, and show how well-known abstract machine instructions, such as the squeeze operation, appear quite naturally as optimisations of the derived abstract machine.

REFERENCES

• 1: 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]
• 2: Diehl, S. (1996), Semantics-directed generation of compilers and abstract machines, PhD thesis, Universitiit des Saarlandes.
• 3: Douence, R. & Fradet, P. (1996), A taxonomy of functional languages implementations, part Ih Call-by-name, callby-need and graph reduction, Technical Report 3050, Institut National de recherche en Informatique et Automatique (INRIA).
• 4: John Fairbairn , Stuart Wray, TIM: A simple, lazy abstract machine to execute supercombinators, Proc. of a conference on Functional programming languages and computer architecture, p.34-45, October 1987, Portland, Oregon, United States
• 5: John Hannan, Making abstract machines less abstract, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.618-635, June 1991, Cambridge, Massachusetts, United States
• 6: Thomas Johnsson, Efficient compilation of lazy evaluation, Proceedings of the 1984 SIGPLAN symposium on Compiler construction, p.58-69, June 17-22, 1984, Montreal, Canada
• 7: 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]
• 8: Rafael D. Lins, Categorical multi-combinators, Proc. of a conference on Functional programming languages and computer architecture, p.60-79, October 1987, Portland, Oregon, United States
• 9: Lins, R. D., Thompson, S. J. & Peyton Jones, S. (1994), '(h~ t}?.e ~,quivalence between CMC and TIM', Journal of Functional Programming 4(1), 47-63.
• 10: Meijer, E. (1988), A taxonomy of function evaluating machines, in T. Johnsson, S. Peyton Jones & K. Karlsson, eds, 'Proceedings of the workshop on Implementation of Function al Languages', Chalmers University of Technology, Tect~nical Report 53.
• 11: Peyton Jones, S. L. (1992), 'Implementing lazy functional languages on stock hardware: The STG machine', .Journal (.,f lVv, nctional Programming 2(2), 127-202.
• 12: Simon L. Peyton Jones, Compiling Haskell by Program Transformation: A Report from the Trenches, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.18-44, April 22-24, 1996
• 13: Simon L. Peyton Jones , David R. Lester, Implementing functional languages, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 14: Sansom, P. M. (1994), Execution Profiling for Non-strict Functionai Languages, PhD thesis, University of Glasgow
• 15: Patrick M. Sansom , Simon L. Peyton Jones, Formally based profiling for higher-order functional languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.334-385, March 1997 [doi>10.1145/244795.244802]
• 16: Jill M. Seaman, An operational semantics of lazy evaluation for analysis, Pennsylvania State University, University Park, PA, 1993
• 17: Jill Seaman , S. Purushothaman Iyer, An operational semantics of sharing in lazy evaluation, Science of Computer Programming, v.27 n.3, p.289-322, Nov. 1996 [doi>10.1016/0167-6423(96)00012-3 ]
• 18: Peter Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming, v.7 n.3, p.231-264, May 1997 [doi>10.1017/S0956796897002712]
• 19: David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224168]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

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