Martin Hofmann
ABSTRACT
We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort.The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system.We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.
- Mobile resource guarantees. EU Project No. IST-2001-33149, see http://www.dcs.ed.ac.uk/home/mrg/.Google Scholar
- David Aspinall and Martin Hofmann. Another Type System for In-Place Update. In D. Le Metayer, editor, Programming Languages and Systems (Proc. ESOP'02), volume Springer LNCS 2305, 2002. Google ScholarDigital Library
- K. Crary and S. Weirich. Resource bound certification. In Proc. 27th Symp. Principles of Prog. Lang. (POPL), pages 184--198. ACM, 2000. Google ScholarDigital Library
- P. Flajolet, B. Salvy, and P. Zimmermann. Lambda-Upsilon-Omega: An assistant algorithms analyzer. In T. Mora, editor, Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, volume 357 of Lecture Notes in Computer Science, pages 201--212, 1989. Proceedings AAECC'6, Rome, July 1988. Google ScholarDigital Library
- Gustavo Gómez and Yanhong A. Liu. Automatic accurate cost-bound analysis for high-level languages. In Frank Mueller and Azer Bestavros, editors, Languages, Compilers, and Tools for Embedded Systems, ACM SIGPLAN Workshop LCTES'98, Montreal, Canada. Springer, 1998. LNCS 1474. Google ScholarDigital Library
- Gustavo Gómez and Yanhong A. Liu. Automatic time-bound analysis for a higher-order language. In Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, pages 75--86. ACM Press, 2002. Google ScholarDigital Library
- Bernd Grobauer. Topics in Semantics-based Program Manipulation. PhD thesis, BRICS Aarhus, 2001.Google Scholar
- Martin Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4):258--289, 2000. An extended abstract has appeared in Programming Languages and Systems, G. Smolka, ed., Springer LNCS, 2000. Google ScholarDigital Library
- Martin Hofmann. The strength of non size-increasing computation. 2002. Proc. ACM Symp. on Principles of Programming Languages (POPL), Portland, Oregon. Google ScholarDigital Library
- J. Hughes and L. Pareto. Recursion and dynamic data structures in bounded space: towards embedded ML programming. In Proc. International Conference on Functional Programming (ACM). Paris, September '99., pages 70--81, 1999. Google ScholarDigital Library
- Steffen Jost. Static prediction of dynamic space usage of linear functional programs, 2002. Diploma thesis at Darmstadt University of Technology, Department of Mathematics. Available at www.tcs.informatik.uni-muenchen.de/~jost/da_sj_28-02-2002.ps.Google Scholar
- Naoki Kobayashi. Quasi-linear types. In Proceedings ACM Principles of Programming Languages, pages 29--42, 1999. Google ScholarDigital Library
- H.-W. Loidl. Granularity in Large-Scale Parallel Functional Programming. PhD thesis, Department of Computing Science, University of Glasgow, 1998.Google Scholar
- George Necula. Proof-carrying code. In Proc. 24th Symp. Principles of Prog. Lang. (POPL). ACM, 1997. Google ScholarDigital Library
- Martin Odersky. Observers for linear types. In B. Krieg-Brückner, editor, ESOP '92: 4th European Symposium on Programming, Rennes, France, Proceedings, pages 390--407. Springer-Verlag, February 1992. Lecture Notes in Computer Science 582. Google ScholarDigital Library
- Lars Pareto. Types for crash prevention. PhD thesis, Chalmers University, Göteborg, Sweden, 2000.Google Scholar
- John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the 25th ACM National Conference, pages 717--740, 1972. Google ScholarDigital Library
- Natarajan Shankar. Efficiently executing PVS. Technical report, Computer Science Laboratory, SRI International, 1999.Google Scholar
- M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109--176, 1997. Google ScholarDigital Library
- Leena Unnikrishnan, Scott D. Stoller, and Yanhong A. Liu. Automatic accurate live memory analysis for garbage-collected languages. In Proceedings of The Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES 2001), June 22--23, 2001 The Workshop on Optimization of Middleware and Distributed Systems (OM 2001), June 18, 2001, Snowbird, Utah, USA. Google ScholarDigital Library
Index Terms
- Static prediction of heap space usage for first-order functional programs
Recommendations
Static prediction of heap space usage for first-order functional programs
We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the ...
Parametric heap usage analysis for functional programs
ISMM '09: Proceedings of the 2009 international symposium on Memory managementThis paper presents an analysis that derives a formula describing the worst-case live heap space usage of programs in a functional language with automated memory management (garbage collection). First, the given program is automatically transformed into ...
Controlling garbage collection and heap growth to reduce the execution time of Java applications
In systems that support garbage collection, a tension exists between collecting garbage too frequently and not collecting it frequently enough. Garbage collection that occurs too frequently may introduce unnecessary overheads at the risk of not ...
Comments