Small domains spell fast strictness analysis

ABSTRACT

Use of strictness analysis in parallel evaluation and optimization of lazy functional languages is well known. The first formal treatment of strictness analysis appeared in Mycroft's seminal work which however dealt only with flat domains. Unlike flat domains, strictness analysis on non-flat domains involves determining how a function transforms a demand (degree of strictness) on its output into a demand on its arguments. Solutions to this problem in its full generality require large domains and appear both complex and expensive to implement. However, only two kinds of demands arise naturally in lazy normalization of terms, viz., e-demand (normal form needed) and d-demand (root stable or head normal form needed). Based on this observation, we identify three useful forms of strictness for non-flat domains - ee, dd and de. Each of these three forms of strictness play an important role in evaluation of functional programs. Specifically, ee strictness is used for transforming call-by-need to call-by-value and dd strictness is useful in repairing violations of strong sequentiality of equational programs as well as in a critical optimization step used in rewriting implementations of such languages. We present intuitively simple methods to compute them. Our methods are computationally efficient as they are based on small domains (1 point for ee and dd and 2 points for de). They are powerful enough to extract all useful strictness information in practice and are general enough to handle functions defined by rewrite rules. We are able to reason about all user defined data types within a single framework and also handle polymorphism.

REFERENCES

• Aug84: Lennart Augustsson, A compiler for lazy ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.218-227, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802038]
• Burn85: G. L. Burn , C. L. Hankin , S. Abramsky, The theory of strictness analysis for higher order functions, on Programs as data objects, p.42-62, April 1986, Copenhagen, Denmark
• Burs80: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• Cla85: Chris Clack , Simon L. Peyton Jones, Strictness analysis—a practical approach, Proc. of a conference on Functional programming languages and computer architecture, p.35-49, January 1985, Nancy, France
• Cou77: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• Fut85: Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318610]
• Hall87: C. V. Hall , D. S. Wise, Compiling strictness into streams, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41637]
• HD82: Christoph M. Hoffman , Michael J. O'Donnell, Programming with Equations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.1, p.83-112, Jan. 1982 [doi>10.1145/357153.357158]
• Hud86: Paul Hudak , Jonathan Young, Higher-order strictness analysis in untyped lambda calculus, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-109, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512653]
• Huet79: HUET, G. AND LEVY, J.J., Computations in Nonambiguous Linear Term Rewriting Systems, Tech. Rap. No. 359(1979), INRIA, Le Chesney, France.
• Hug85: John Hughes, Strictness detection in non-flat domains, on Programs as data objects, p.112-135, April 1986, Copenhagen, Denmark
• Kel80: KELLER, It.M, Semantics and Applications of Function Graphs~ Technical Report UUCS-80-11~, Univ. of Utah, 1980.
• Kuo89: Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
• Lin86: Gary Lindstrom, Static evaluation of functional programs, ACM SIGPLAN Notices, v.21 n.7, p.196-206, July 1986
• Mar87: Chris Martin , Chris Hankin, Finding fixed points in finite lattices, Proc. of a conference on Functional programming languages and computer architecture, p.426-445, October 1987, Portland, Oregon, United States
• Myc80: Alan Mycroft, The Theory and Practice of Transforming Call-by-need into Call-by-value, Proceedings of the Fourth 'Colloque International sur la Programmation' on International Symposium on Programming, p.269-281, April 22-24, 1980
• OD77: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• OD85: Michael J. O'Donnell, Equational logic as a programming language, Massachusetts Institute of Technology, Cambridge, MA, 1985
• OD87: M. J. O'Donnell, Term-rewriting implementation of equational logic programming, on Rewriting techniques and applications, p.1-12, May 1987, Bordeaux, France
• Sek89: R. C. Sekar , S. Pawagi , I. V. Ramakrishnan, Transforming strongly sequential rewrite systems with constructors for efficient parallel execution, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.404-418, January 1989
• Str87: ROBBltT STRANDff, Optimizing Equational Programs, Rewriting Techniques and Applications, Springer-Verla9 LNCS ~56, 1987, pp. iS-e4.
• That84: SATISH THATTE, Demand driven Evaluation with Equations, Technical Report CRL. TR-34-84, University oJ Michigan Computing Research Laboratory, Ann Arbor.
• Tur85: D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France
• Wad87: Philip Wadler , R. J. M. Hughes, Projections for strictness analysis, Proc. of a conference on Functional programming languages and computer architecture, p.385-407, October 1987, Portland, Oregon, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Languages, Theory, Verification