Static prediction of heap space usage for first-order functional programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Static prediction of heap space usage for first-order functional programs

Full text

Pdf (287 KB)

Source

ACM SIGPLAN Notices archive
Volume 38 , Issue 1 (January 2003) table of contents

Pages: 185 - 197

Year of Publication: 2003

ISSN:0362-1340

Also published in ...

Authors

Martin Hofmann	LMU München, Institut für Informatik, München, Germany
Steffen Jost	LMU München, Institut für Informatik, München, Germany

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 50, Citation Count: 26

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/640128.604148 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Mobile resource guarantees. EU Project No. IST-2001-33149, see http://www.dcs.ed.ac.uk/home/mrg/.
	2	David Aspinall , Martin Hofmann, Another Type System for In-Place Update, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.36-52, April 08-12, 2002
	3	Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
	4	Philippe Flajolet , Bruno Salvy , Paul Zimmermann, Lambda - Upsilon - Omega: An Assistant Algorithms Analyzer, Proceedings of the 6th International Conference, on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.201-212, July 04-08, 1988
	5	Yanhong A. Liu , Gustavo Gomez, Automatic Accurate Time-Bound Analysis for High-Level Languages, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.31-40, June 01, 1998
	6	Gustavo Gómez , Yanhong A. Liu, Automatic time-bound analysis for a higher-order language, Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.75-86, January 14-15, 2002, Portland, Oregon
	7	Bernd Grobauer. Topics in Semantics-based Program Manipulation. PhD thesis, BRICS Aarhus, 2001.
	8	Martin Hofmann, A type system for bounded space and functional in-place update, Nordic Journal of Computing, v.7 n.4, p.258-289, Winter 2000
	9	Martin Hofmann, The strength of non-size increasing computation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.260-269, January 16-18, 2002, Portland, Oregon
	10	John Hughes , Lars Pareto, Recursion and dynamic data-structures in bounded space: towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.70-81, September 27-29, 1999, Paris, France
	11	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.
	12	Naoki Kobayashi, Quasi-linear types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.29-42, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292546]
	13	H.-W. Loidl. Granularity in Large-Scale Parallel Functional Programming. PhD thesis, Department of Computing Science, University of Glasgow, 1998.
	14	George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
	15	Martin Odersky, Observers for linear types, Symposium proceedings on 4th European symposium on programming, p.390-407, January 1992, Rennes, France
	16	Lars Pareto. Types for crash prevention. PhD thesis, Chalmers University, Göteborg, Sweden, 2000.
	17	John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
	18	Natarajan Shankar. Efficiently executing PVS. Technical report, Computer Science Laboratory, SRI International, 1999.
	19	Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
	20	Leena Unnikrishnan , Scott D. Stoller , Yanhong A. Liu, Automatic Accurate Live Memory Analysis for Garbage-Collected Languages, Proceedings of the ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems, p.102-111, August 2001, Snow Bird, Utah, United States

CITED BY 26

	Martin Hofmann, Linear types and non-size-increasing polynomial time computation, Information and Computation, v.183 n.1, p.57-85, May 25, 2003
	Mads Tofte , Lars Birkedal , Martin Elsman , Niels Hallenberg, A Retrospective on Region-Based Memory Management, Higher-Order and Symbolic Computation, v.17 n.3, p.245-265, September 2004
	Joseph C. Vanderwaart , Karl Crary, Automated and certified conformance to responsiveness policies, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.79-90, January 10-10, 2005, Long Beach, California, USA
	Olha Shkaravska, Types with semantics: soundness proof assistant, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.50-57, September 30-30, 2005, Tallinn, Estonia
	Wei-Ngan Chin , Siau-Cheng Khoo , Shengchao Qin , Corneliu Popeea , Huu Hai Nguyen, Verifying safety policies with size properties and alias controls, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
	James Cheney , Morten Dahl, Resource bound analysis for database queries, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, June 07-13, 2008, Tucson, AZ, USA
	Kevin Hammond , Christian Ferdinand , Reinhold Heckmann, Towards formally verifiable resource bounds for real-time embedded systems, ACM SIGBED Review, v.3 n.4, p.27-36, October 2006
	Joan Krone , William F. Ogden , Murali Sitaraman, Performance analysis based upon complete profiles, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon
	Franco Barbanera , Michele Bugliesi , Mariangiola Dezani-Ciancaglini , Vladimiro Sassone, Space-aware ambients and processes, Theoretical Computer Science, v.373 n.1-2, p.41-69, March, 2007
	David Aspinall , Lennart Beringer , Martin Hofmann , Hans-Wolfgang Loidl , Alberto Momigliano, A program logic for resources, Theoretical Computer Science, v.389 n.3, p.411-445, December, 2007
	Manuel Montenegro , Ricardo Peña , Clara Segura, A type system for safe memory management and its proof of correctness, Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, July 15-17, 2008, Valencia, Spain
	Víctor Braberman , Federico Fernández , Diego Garbervetsky , Sergio Yovine, Parametric prediction of heap memory requirements, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA
	Armelle Bonenfant , Zezhi Chen , Kevin Hammond , Greg Michaelson , Andy Wallace , Iain Wallace, Towards resource-certified software: a formal cost model for time and its application to an image-processing example, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
	Jurriaan Hage , Stefan Holdermans, Heap recycling for lazy languages, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA
	Elvira Albert , Samir Genaim , Miguel Gomez-Zamalloa, Heap space analysis for java bytecode, Proceedings of the 6th international symposium on Memory management, October 21-22, 2007, Montreal, Quebec, Canada
	Roberto M. Amadio, Synthesis of max-plus quasi-interpretations, Fundamenta Informaticae, v.65 n.1-2, p.29-60, January 2005
	Ajay Chander , David Espinosa , Nayeem Islam , Peter Lee , George C. Necula, Enforcing resource bounds via static verification of dynamic checks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.28-es, August 2007
	Wei-Ngan Chin , Huu Hai Nguyen , Corneliu Popeea , Shengchao Qin, Analysing memory resource bounds for low-level programs, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA
	Sumit Gulwani , Krishna K. Mehra , Trishul Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Sumit Gulwani , Tal Lev-Ami , Mooly Sagiv, A combination framework for tracking partition sizes, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	David Aspinall , Martin Hofmann , Michal KoneČnÝ, A type system with usage aspects, Journal of Functional Programming, v.18 n.2, p.141-178, March 2008
	Conor McBride, Clowns to the left of me, jokers to the right (pearl): dissecting data structures, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Jaroslav Ševčík, Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.1, p.133-147, July, 2007
	Patrick Baillot , Kazushige Terui, Light types for polynomial time computation in lambda calculus, Information and Computation, v.207 n.1, p.41-62, January, 2009
	Leena Unnikrishnan , Scott D. Stoller, Parametric heap usage analysis for functional programs, Proceedings of the 2009 international symposium on Memory management, June 19-20, 2009, Dublin, Ireland
	Elvira Albert , Samir Genaim , Miguel Gómez-Zamalloa Gil, Live heap space analysis for languages with garbage collection, Proceedings of the 2009 international symposium on Memory management, June 19-20, 2009, Dublin, Ireland