Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

We present a new approach to static program analysis that permits each expression in a program to be assigned an execution time estimate. Our approach uses a time system in conjunction with a conventional type system to compute both the type and the time of an expression. The time of an expression is either an integer upper bound on the number of ticks the expression will execute, or the distinguished element long that indicates that the expression contains a loop, and thus may run for an arbitrary length of time. Every function type includes a latent time that is used to communicate its expected execution time from the point of its definition to the points of its use. Unlike previous approaches, a time system works in the presence of first-class functions and separate compilation. In addition, time polymorphism allows the time of a function to depend on the times of any functions that it takes as arguments. Time estimates are useful when compiling programs for multiprocessors in order to balance the overhead of initiating a concurrent computation against the expected execution time of the computation. The correctness of our time system is proven with respect to a dynamic semantics.

REFERENCES

• 1: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 2: Charles Consel, Binding time analysis for high order untyped functional languages, Proceedings of the 1990 ACM conference on LISP and functional programming, p.264-272, June 27-29, 1990, Nice, France [doi>10.1145/91556.91668]
• 3: DORNIC, V. Analyse de complexit~ des algorithmes: v~rification et inference. Ph.D. thesis, Ecole des Mines de Paris (in preparation). Expected 1992.
• 4: FLAJOLET, P. AND VITTER, Jo S. Average-case analysis of algorithms and data structures. Research report INRIA 718, Aug. 1987.
• 5: GIFFORD, D. K., JOUVELOT, P., LUCASSEN, J. M., AND SHELDON, M.A. The FX-87 reference manual. Res. Rep. MIT/LCS/TR-407, 1987.
• 6: GOLDBERG, F. S. Multiprocessor execution of functional programs. Res. Rep., Yale, DCS/RR-618, Apr. 1988.
• 7: GRAY, S.L. Using futures to exploit parallelism in Lisp. MIT SB Masters thesis, 1983.
• 8: Timothy Hickey , Jacques Cohen, Automating program analysis, Journal of the ACM (JACM), v.35 n.1, p.185-220, Jan. 1988 [doi>10.1145/42267.42275]
• 9: JOUVELOT, P. AND GIFFORD, D. K. The FX-87 interpreter. In Proceedings of the IEEE International Conference on Computer Languages (Miami Beach, Fla., Oct. 1988), pp. 65-72.
• 10: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 11: KOZEN, D. Semantics of probabilistic programs. J. Comput. Syst. Sci. 22 (1981), 328-350.
• 12: Daniel Le Métayer, ACE: an automatic complexity evaluator, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.248-266, April 1988 [doi>10.1145/42190.42347]
• 13: LUCASSEN, J.M. Types and effects, towards the integration of functional and imperative programming. Ph.D. dissertation, MIT-LCS, Sept. 1987.
• 14: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 15: RAMSHAW, L. H. Formalizing the analysis of algorithms. Rep. SL-79-5, Xerox Palo Alto Research Center, Palo Alto, Calif., 1979.
• 16: Mads Rosendahl, Automatic complexity analysis, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.144-156, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99381]
• 17: SANDS, D. Complexity analysis for higher order languages. Res. Rep. DOC 88/14, imperial College, London, Oct. 1988.
• 18: D. Sands, Complexity analysis for a lazy higher-order language, Proceedings of the third European symposium on programming on ESOP '90, p.361-376, May 1990, Copenhagen, Denmark
• 19: TOFTE, M. Operational semantics and polymorphic type inference. Thesis, CST-52-88, Univ. of Edinburgh, 1988.
• 20: TURING, A.M. On computable numbers, with an application to the Entscheidungsproblem. In Proceedings of the London Mathematical Society 42, 2 (1936), 230-265 and 43, (1936), 544-546.
• 21: P. Wadler, Strictness analysis aids time analysis, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-132, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73571]
• 22: Ben Wegbreit, Mechanical program analysis, Communications of the ACM, v.18 n.9, p.528-539, Sept. 1975 [doi>10.1145/361002.361016]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES

General Terms:
Languages, Performance, Verification

Keywords:
complexity analysis, effect systems, fixpoint operator, polymorphic typed language, time and type checker, time system, type systems