More Web Proxy on the site http://driver.im/

research-article

Automatic amortised analysis of dynamic memory allocation for lazy functional programs

Authors:

Pedro Vasconcelos,

Mário Florido,

Kevin HammondAuthors Info & Claims

ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming

Pages 165 - 176

https://doi.org/10.1145/2364527.2364575

Published: 09 September 2012 Publication History

Abstract

This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this paper, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of lazy potential. We present our analysis as a proof system for predicting heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury's natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis.

References

[1]

E. Albert, J. Silva, and G. Vidal. Time Equations for Lazy Functional (Logic) Languages. In Proc. AGP-2003: 2003 Joint Conf. on Declarative Prog., Reggio Calabria, Italy, Sept. 3-5, 2003, pages 13--24, 2003.

[2]

E. Albert, S. Genaim, and M. Gómez-Zamalloa. Live Heap Space Analysis for Languages with Garbage Collection. In Proc. ISMM 2009: Intl. Symp. on Memory Management, pages 129--138, Dublin, Ireland, June 2009. ACM. ISBN 978-1-60558-347-1.

Digital Library

[3]

E. Albert, S. Genaim, and M. Gómez-Zamalloa. Parametric Inference of Memory Requirements for Garbage Collected Languages. In Proc. 2010 International Symposium on Memory Management, ISMM '10, pages 121--130, New York, NY, USA, 2010. ACM.

Digital Library

[4]

Z. M. Ariola and M. Felleisen. The Call-by-Need Lambda Calculus. J. Funct. Program., 7:265--301, May 1997.

Digital Library

[5]

A. Bakewell and C. Runciman. A Model for Comparing the Space Usage of Lazy Evaluators. In Proc. PPDP 2000: Intl. Conf. on Principles and Practice of Declarative Prog., Quebec, Canada, pages 151--162, 2000.

Digital Library

[6]

A. Bakewell and C. Runciman. A Space Semantics for Core Haskell. Electr. Notes Theor. Comput. Sci., 41(1), 2000.

[7]

B. Bjerner and S. Holmström. A Compositional Approach to Time Analysis of First Order Lazy Functional Programs. In Proc. FPCA '89: Conf. on Functional Prog. Langs. and Comp. Arch., pages 157--165, 1989.

Digital Library

[8]

V. Braberman, F. Fernández, D. Garbervetsky, and S. Yovine. Parametric Prediction of Heap Memory Requirements. In Proc. ISMM 2008: Intl. Symp. on Memory Management, pages 141--150, New York, NY, USA, June 2008.

Digital Library

[9]

B. Campbell. Amortised Memory Analysis Using the Depth of Data Structures. In G. Castagna, editor, Proc. ESOP 2009: 18th European Symposium on Programming, York, UK, pages 190--204. Springer LNCS 5502, 2009.

Digital Library

[10]

W.-N. Chin, H. Nguyen, C. Popeea, and S. Qin. Analysing Memory Resource Bounds for Low-Level Programs. In Proc. ISMM'08: Intl. Symp. on Memory Management, pages 151--160, Tucson, USA, June 2008. ACM. ISBN 978-1-60558-134-7.

Digital Library

[11]

K. Crary and S. Weirich. Resource Bound Certification. In Proc. POPL 2000: ACM Symp. on Principles of Prog. Langs., pages 184--198, Jan. 2000.

Digital Library

[12]

N. A. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proc. POPL 2008: Symp. on Principles of Prog. Langs., San Francisco, USA, January 7-12, 2008, pages 133--144. ACM, 2008.

Digital Library

[13]

A. de la Encina and R. Peña-Marí. Proving the Correctness of the STG Machine. In Proc. IFL '01: Impl. of Functional Langs., Stockholm, Sweden, Sept. 24-26, 2001, pages 88--104. Springer LNCS 2312, 2002.

Digital Library

[14]

A. de la Encina and R. Peña-Marí. Formally Deriving an STG Machine. In Proc. 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 102--112. ACM, 2003.

Digital Library

[15]

A. de la Encina and R. Peña-Marí. From Natural Semantics to C: a Formal Derivation of two STG Machines. J. Funct. Program., 19(1): 47--94, 2009.

Digital Library

[16]

P. Fradet and D. L. Métayer. Compilation of functional languages by program transformation. ACM Transactions on Programming Languages and Systems, 13(1):21--51, January 1991.

Digital Library

[17]

J. Gustavsson and D. Sands. A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science, 26, 1999.

[18]

J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. In 38th Symp. on Principles of Prog. Langs. (POPL'11), pages 357--370, 2011.

Digital Library

[19]

M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Proc. POPL 2003: ACM Symp. on Principles of Prog. Langs., pages 185--197, Jan. 2003.

Digital Library

[20]

M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis (for an Object-Oriented Language). In Proc. ESOP '06: European Symposium on Prog., pages 22--37, Mar. 2006.

Digital Library

[21]

M. Hofmann and D. Rodriguez. Efficient type-checking for amortised heap-space analysis. In Proc. CSL '09: 18th EACSL Annual Conf. on Computer Science Logic, pages 317--331, 2009.

Digital Library

[22]

C. Hope. A Functional Semantics for Space and Time. PhD thesis, 2008. University of Nottingham.

[23]

R. Hughes. Why Functional Programming Matters. The Computer Journal, 32(2):98--107, 1989.

Digital Library

[24]

S. L. P. Jones. Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine. J. Funct. Program., 2 (2):127--202, 1992.

[25]

M. B. Josephs. The semantics of lazy functional languages. Theor. Comput. Sci., 68(1):105--111, 1989.

Digital Library

[26]

S. Jost. Static Prediction of Dynamic Space Usage of Linear Functional Programs, Dipl. Thesis, Darmstadt Univ. of Tech., 2002.

[27]

S. Jost. Automated Amortised Analysis. PhD thesis, LMU Munich.

[28]

S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. 'Carbon Credits' for Resource-Bounded Computations Using Amortised Analysis. In Proc. FM 2009: Intl. Conf. on Formal Methods, pages 354--369. Springer LNCS 5850, 2009.

Digital Library

[29]

S. Jost, H.-W. Loidl, K. Hammond, and M. Hofmann. Static determination of quantitative resource usage for higher-order programs. In Proc. POPL 2010: ACM Symp. on Principles of Prog. Langs.,Madrid, Spain, pages 223--236, Jan. 2010.

Digital Library

[30]

J. Launchbury. A Natural Semantics for Lazy Evaluation. In Proc. POPL '93: Symp. on Princ. of Prog. Langs., pages 144--154, 1993.

Digital Library

[31]

J. Maraist, M. Odersky, and P. Wadler. The Call-by-Need Lambda Calculus. J. Funct. Program., 8:275--317, May 1998.

Digital Library

[32]

R. Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Induction Types. PhD thesis, LMU Munich, 1998.

[33]

A. Moran and D. Sands. Improvement in a Lazy Context: An Operational Theory for Call-by-Need. In POPL, pages 43--56, 1999.

Digital Library

[34]

J. Mountjoy. The Spineless Tagless G-machine, naturally. In Proc. ICFP '98: Intl. Conf. on Functional Prog., pages 163--173, 1998.

Digital Library

[35]

C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.

[36]

S. Peyton Jones (ed.), L. Augustsson, B. Boutel, F. Burton, J. Fasel, A. Gordon, K. Hammond, R. Hughes, P. Hudak, T. Johnsson, M. Jones, J. Peterson, A. Reid, and P. Wadler. Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report, Yale University, 1999.

[37]

D. Sands. Complexity Analysis for a Lazy Higher-Order Language. In Proc. ESOP '90: European Symposium on Programming, Copenhagen, Denmark, Springer LNCS 432, pages 361--376, 1990.

Digital Library

[38]

D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, University of London, September 1990.

[39]

D. Sands. Computing with Contexts: A Simple Approach. In Proc. HOOTS II: Higher-Order Operational Techniques in Semantics, Electr. Notes in Theoretical Comp. Sci. 1998.

Digital Library

[40]

P. Sestoft. Deriving a Lazy Abstract Machine. J. Functional Programming, 7(3):231--264, 1997.

Digital Library

[41]

O. Shkaravska, R. van Kesteren, and M. van Eekelen. Polynomial Size Analysis of First-Order Functions. In Proc. TLCA 2007: Typed Lambda Calculi and Applications (TLCA 2007), pages 351--365, Paris, France, June 26-28, June 2007. Springer LNCS 4583.

Digital Library

[42]

R. E. Tarjan. Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306--318, April 1985.

Digital Library

[43]

P. B. Vasconcelos. Space Cost Analysis Using Sized Types. PhD thesis, University of St Andrews, 2008.

[44]

P. B. Vasconcelos and K. Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In Proc. IFL '03: Impl. of Functional Languages, pages 86--101, Edinburgh, UK, 2004. Springer LNCS 3145.

Digital Library

[45]

P.Wadler. Strictness Analysis aids Time Analysis. In Proc. POPL '88: ACM Symp. on Princ. of Prog. Langs., pages 119--132, 1988.

Digital Library

[46]

P. Wadler. The Essence of Functional Programming. In Proc. POPL '92: ACM Symp. on Principles of Prog. Langs., pages 1--14, Jan. 1992.

Digital Library

[47]

P. Wadler and J. Hughes. Projections for Strictness Analysis. In Proc. FPCA'87: Intl. Conf. on Functional Prog. Langs. and Comp. Arch., Springer LNCS 274, pages 385--407, Sept. 1987.

Digital Library

Cited By

Silva ABarbosa MFlorido M(2023)Execution Time Program Verification with Tight BoundsPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_4(56-72)Online publication date: 8-Jan-2023
https://doi.org/10.1007/978-3-031-24841-2_4
Haeri SThompson PDavies NVan Roy PHammond KChapman J(2022)Mind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case StudyComputers10.3390/computers1103004511:3(45)Online publication date: 17-Mar-2022
https://doi.org/10.3390/computers11030045
Madiot JPottier F(2022)A separation logic for heap space under garbage collectionProceedings of the ACM on Programming Languages10.1145/34986726:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498672
Show More Cited By

Index Terms

Automatic amortised analysis of dynamic memory allocation for lazy functional programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

Automatic amortised analysis of dynamic memory allocation for lazy functional programs
ICFP '12

This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and ...
Resource Analysis for Lazy Evaluation with Polynomial Potential
IFL '20: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages

Space and time requirements of lazy functional programs are hard to predict for both programmers and compilers. Previous work in compile-time amortised analyses for lazy functional languages by Simões, Jost et.al. was limited to bounds that are linear ...
A Lazy Language Needs a Lazy Type System: Introducing Polymorphic Contexts
IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages

Most type systems that support polymorphic functions are based on a version of System-F. We argue that this limits useful programming paradigms for languages with lazy evaluation. We motivate an extension of System-F alleviating this limitation.

First, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming

September 2012

392 pages

ISBN:9781450310543

DOI:10.1145/2364527

General Chair:
Peter Thiemann
University of Freiburg, Germany
,
Program Chair:
Robby Findler
Northwestern University, USA

ACM SIGPLAN Notices Volume 47, Issue 9
ICFP '12
September 2012
368 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2398856
Issue’s Table of Contents

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP'12

Sponsor:

SIGPLAN

ICFP'12: ACM SIGPLAN International Conference on Functional Programming

September 9 - 15, 2012

Copenhagen, Denmark

Acceptance Rates

ICFP '12 Paper Acceptance Rate 32 of 88 submissions, 36%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
267
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Silva ABarbosa MFlorido M(2023)Execution Time Program Verification with Tight BoundsPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_4(56-72)Online publication date: 8-Jan-2023
https://doi.org/10.1007/978-3-031-24841-2_4
Haeri SThompson PDavies NVan Roy PHammond KChapman J(2022)Mind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case StudyComputers10.3390/computers1103004511:3(45)Online publication date: 17-Mar-2022
https://doi.org/10.3390/computers11030045
Madiot JPottier F(2022)A separation logic for heap space under garbage collectionProceedings of the ACM on Programming Languages10.1145/34986726:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498672
Hoffmann JJost S(2022)Two decades of automatic amortized resource analysisMathematical Structures in Computer Science10.1017/S0960129521000487(1-31)Online publication date: 16-Mar-2022
https://doi.org/10.1017/S0960129521000487
Fan GChen TYin BChen LWang TWang J(2021)Static Bound Analysis of Dynamically Allocated Resources for C Programs2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE52982.2021.00048(390-400)Online publication date: Oct-2021
https://doi.org/10.1109/ISSRE52982.2021.00048
Das AQadeer S(2021)Exact and Linear-Time Gas-Cost AnalysisStatic Analysis10.1007/978-3-030-65474-0_15(333-356)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-65474-0_15
Moreira SVasconcelos PFlorido M(2020)Resource Analysis for Lazy Evaluation with Polynomial PotentialProceedings of the 32nd Symposium on Implementation and Application of Functional Languages10.1145/3462172.3462196(104-114)Online publication date: 2-Sep-2020
https://dl.acm.org/doi/10.1145/3462172.3462196
Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Knoth TWang DPolikarpova NHoffmann JMcKinley KFisher K(2019)Resource-guided program synthesisProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314602(253-268)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314602
Wang DHoffmann J(2019)Type-guided worst-case input generationProceedings of the ACM on Programming Languages10.1145/32903263:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290326
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents