Vincent Dornic
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.
- 1 BACKUS, J.W. Can programming be liberated from Von Neumann style? A functional style and its algebra of programs. Commun. ACM 21, 8 (Aug. 1978), 613-641. Google Scholar
Digital Library
- 2 CONSEL, C. Binding time analysis for higher-order untyped functional languages. In Proceedings of the ACM Lisp and Functional Programming (Nice, June 1990), pp. 264-273. Google ScholarDigital Library
- 3 DORNIC, V. Analyse de complexit~ des algorithmes: v~rification et inference. Ph.D. thesis, Ecole des Mines de Paris (in preparation). Expected 1992.Google Scholar
- 4 FLAJOLET, P. AND VITTER, Jo S. Average-case analysis of algorithms and data structures. Research report INRIA 718, Aug. 1987.Google Scholar
- 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.Google Scholar
- 6 GOLDBERG, F. S. Multiprocessor execution of functional programs. Res. Rep., Yale, DCS/RR-618, Apr. 1988.Google Scholar
- 7 GRAY, S.L. Using futures to exploit parallelism in Lisp. MIT SB Masters thesis, 1983.Google Scholar
- 8 HICKEY, T. AND COHEN, J. Automating program analysis. J. ACM 35, 1 (Jan. 1988), 185-220. Google ScholarDigital Library
- 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.Google Scholar
- 10 JOUVELOT, P. AND GIFFORD, D.K. Algebraic reconstruction of types and effects. In Proceedings of the ACM Principles of Programming Languages (Orlando, Fla., Jan. 1991), pp. 303-310. Google ScholarDigital Library
- 11 KOZEN, D. Semantics of probabilistic programs. J. Comput. Syst. Sci. 22 (1981), 328-350.Google ScholarCross Ref
- 12 LE METAYER, D. ACE: An automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10, 2 (Apr. 1988), 248-266. Google ScholarDigital Library
- 13 LUCASSEN, J.M. Types and effects, towards the integration of functional and imperative programming. Ph.D. dissertation, MIT-LCS, Sept. 1987.Google Scholar
- 14 LUCASSEN, J. M. AND GIFFORD, D. K. Polymorphic effect systems. In Proceedings of the ACM Conference on Principles of Programming Languages (San Diego, Calif., Jan. 1988), pp. 47-57. Google ScholarDigital Library
- 15 RAMSHAW, L. H. Formalizing the analysis of algorithms. Rep. SL-79-5, Xerox Palo Alto Research Center, Palo Alto, Calif., 1979.Google Scholar
- 16 ROSENDAHL, M. Automatic complexity analysis. In Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture (London, Sept. 11-13, 1989), pp. 144-156. Google ScholarDigital Library
- 17 SANDS, D. Complexity analysis for higher order languages. Res. Rep. DOC 88/14, imperial College, London, Oct. 1988.Google Scholar
- 18 SANDS, D. Complexity analysis for a lazy high-order language. In Proceedings of LNCS European Symposium On Programming (Copenhagen, May 15-18, 1990), pp. 361-376. Google ScholarDigital Library
- 19 TOFTE, M. Operational semantics and polymorphic type inference. Thesis, CST-52-88, Univ. of Edinburgh, 1988.Google Scholar
- 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.Google Scholar
- 21 WADLER, P. Strictness analysis aids time analysis. In Proceedings of the ACM Principles on Programming Languages, 1988 (San Diego, Calif., Jan. 1988), pp. 119-132. Google ScholarDigital Library
- 22 WEGBREIT, B. Mechanical program analysis. Commun. ACM 18, 9 (Sept. 1975), 528-539. Google ScholarDigital Library
Index Terms
- Polymorphic time systems for estimating program complexity
Recommendations
Recursive type generativity
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingExistential types provide a simple and elegant foundation for understanding generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found ...
Recursive type generativity
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingExistential types provide a simple and elegant foundation for understanding generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found ...
Lightweight monadic regions
Haskell '08: Proceedings of the first ACM SIGPLAN symposium on HaskellWe present Haskell libraries that statically ensure the safe use of resources such as file handles. We statically prevent accessing an already closed handle or forgetting to close it. The libraries can be trivially extended to other resources such as ...
Comments