research-article

Static determination of quantitative resource usage for higher-order programs

Authors:

Hans-Wolfgang Loidl,

Martin HofmannAuthors Info & Claims

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 223 - 236

https://doi.org/10.1145/1706299.1706327

Published: 17 January 2010 Publication History

Abstract

We describe a new automatic static analysis for determining upper-bound functions on the use of quantitative resources for strict, higher-order, polymorphic, recursive programs dealing with possibly-aliased data. Our analysis is a variant of Tarjan's manual amortised cost analysis technique. We use a type-based approach, exploiting linearity to allow inference, and place a new emphasis on the number of references to a data object. The bounds we infer depend on the sizes of the various inputs to a program. They thus expose the impact of specific inputs on the overall cost behaviour.

The key novel aspect of our work is that it deals directly with polymorphic higher-order functions without requiring source-level transformations that could alter resource usage . We thus obtain safe and accurate compile-time bounds. Our work is generic in that it deals with a variety of quantitative resources. We illustrate our approach with reference to dynamic memory allocations/deallocations, stack usage, and worst-case execution time, using metrics taken from a real implementation on a simple micro-controller platform that is used in safety-critical automotive applications.

References

[1]

A. Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006.

[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.

Digital Library

[3]

R. Benzinger. Automated Complexity Analysis of Nuprl Extracted Programs. Journal of Functional Programming, 11(1):3--31, 2001.

Digital Library

[4]

M. Berkelaar, K. Eikland, and P. Notebaert. lp solve: Open Source (Mixed-Integer) Linear Programming System. Published under GNU LGPL (Lesser General Public Licence). http://lpsolve.sourceforge.net/5.5.

[5]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A Static Analyzer for Large Safety-Critical Software. In Proc. PLDI'03: Conf. on Programming Language Design and Implementation, pages 196--207, San Diego, USA, June 2003. ACM.

Digital Library

[6]

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

Digital Library

[7]

W.-N. Chin and S.-C. Khoo. Calculating Sized Types. Higher-Order and Symbolic Computing, 14(2,3):261--300, 2001.

Digital Library

[8]

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.

Digital Library

[9]

K. Crary and S. Weirich. Resource Bound Certification. In Proc. POPL'00: Symp. on Princ. of Prog. Langs, pages 184--198, Boston, USA, 2000. ACM.

Digital Library

[10]

N. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proc. POPL'08: Symp. on Princ. of Prog. Langs, pages 133--144, San Francisco, USA, 2008.

Digital Library

[11]

C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling, S. Thesing, and R.Wilhelm. Reliable and Precise WCET Determination for a Real-Life Processor. In Proc EMSOFT'01: Intl Workshop on Embedded Software, LNCS 2211, pages 469--485, Tahoe City, USA, Oct. 2001. Springer.

Digital Library

[12]

G. Gomez and Y. Liu. Automatic Time-Bound Analysis for a Higher-Order Language. In Proc. LCTES'98: Conf. on Languages, Compilers and Tools for Embedded Systems, LNCS 1474, pages 31--40,Montreal, Canada, June 1998. Springer.

Digital Library

[13]

S. Gulwani, K. Mehra, and T. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In Proc. POPL'09: Symp. on Princ. of Prog. Langs, pages 127--139, Savannah, USA, Jan. 2009. ACM.

Digital Library

[14]

K. Hammond and G. Michaelson. Hume: a Domain-Specific Language for Real-Time Embedded Systems. In Proc. GPCE 2003: Intl. Conf. on Generative Prog. and Component Eng., LNCS 2830, pages 37--56, Erfurt, Germany, Sept. 2003. Springer.

Digital Library

[15]

F. Henglein. Type Inference with Polymorphic Recursion. ACM TOPLAS: Trans. Prog. Langs. Systs, 15(2):253--289, April 1993.

Digital Library

[16]

J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential. In preparation.

[17]

M. Hofmann. A Type System for Bounded Space and Functional In-Place Update. Nordic Journal of Computing, 7(4):258--289, 2000.

Digital Library

[18]

M. Hofmann. The Strength of non Size-Increasing Computation. In Proc. POPL'02: Symp. on Princ. of Prog. Langs, pages 260--269, Portland, USA, Jan. 2002. ACM.

Digital Library

[19]

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

Digital Library

[20]

L. Huelsbergen, J. Larus, and A. Aiken. Using the Run-Time Sizes of Data Structures to Guide Parallel Thread Creation. In Proc. LFP'94: Symp. on Lisp and Functional Programming, pages 79--90, Orlando, USA, June 1994. ACM.

Digital Library

[21]

R. Hughes and L. Pareto. Recursion and Dynamic Data Structures in Bounded Space: Towards Embedded ML Programming. In Proc. ICFP '99: Intl. Conf. on Functional Programming, pages 70--81, Paris, France, Sept. 1999. ACM.

Digital Library

[22]

R. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In Proc. POPL'96: Symp. on Princ. of Prog. Langs, pages 410--423, St. Petersburg Beach, USA, Jan. 1996. ACM.

Digital Library

[23]

S. Ishtiaq and P. O'Hearn. BI as an Assertion Language for Mutable Data Structures. In Proc. POPL'01: Symp. on Princ. of Prog. Langs., pages 14--26. ACM, Jan. 2001.

Digital Library

[24]

H. Jonkers. Abstract Storage Structures. In Algorithmic Languages, pages 321--343. IFIP, North Holland, 1981.

[25]

S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. "Carbon Credits" for Resource-Bounded Computations using Amortised Analysis. In Proc. FM '09: Intl. Symp. on Formal Methods, LNCS 5850, Eindhoven, the Netherlands, Nov. 2009. Springer.

Digital Library

[26]

A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type Reconstruction in the Presence of Polymorphic Recursion. ACM TOPLAS: Trans. Prog. Langs. Systs, 15(2):290--311, April 1993.

Digital Library

[27]

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

Digital Library

[28]

D. Le Métayer. ACE: An Automatic Complexity Evaluator. ACM TOPLAS: Trans. on Prog. Langs. and Systs, 10(2), April 1988.

Digital Library

[29]

B. Lisper. Fully Automatic, Parametric Worst-Case Execution Time Analysis. In Proc. WCET '03: Intl. Workshop on Worst-Case Execution Time Analysis, pages 99--102, 2003.

[30]

H.-W. Loidl and S. Jost. Improvements to a Resource Analysis for Hume. In Proc. FOPARA '09: Intl. Workshop on Foundational and Practical Aspects of Resource Analysis, Nov. 2009. Submitted.

Digital Library

[31]

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

Digital Library

[32]

R. Pena, C. Segura, and M. Montenegro. A Sharing Analysis for Safe. In Proc TFP'06: Symp. on Trends in Functional Programming, pages 109--128, Nottingham, UK, Apr. 2006. Intellect.

[33]

J. C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. In Proc of the 25th ACMNational Conference, pages 717--740. ACM, 1972.

Digital Library

[34]

N. Rinetzky, J. Bauer, T. Reps,M. Sagiv, and R.Wilhelm. A Semantics for Procedure Local Heaps and its Abstractions. In Proc. POPL'05: Symp. on Princ. of Prog. Langs, pages 296--309. ACM, Jan. 2005.

Digital Library

[35]

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

Digital Library

[36]

W. Taha, S. Ellner, and H. Xi. Generating Heap-Bounded Programs in a Functional Setting. In Proc. EMSOFT '03: Intl. Conf. on Embedded Software, LNCS 2855, pages 340--355. Springer, 2003.

[37]

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

Digital Library

[38]

P. Vasconcelos. Cost Inference and Analysis for Recursive Functional Programs. PhD thesis, University of St Andrews, Feb. 2008.

[39]

P. Vasconcelos and K. Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In Proc. IFL 2003: Intl. Workshop on Impl. of Functional Languages, LNCS 3145, pages 86--101, Edinburgh, UK, Sept. 2003. Springer.

Digital Library

[40]

D. Walker and G. Morrisett. Alias Types for Recursive Data Structures. In Proc. TIL'00: Types in Compilation, LNCS 2071, pages 177--206. Springer, 2000.

Digital Library

Cited By

Pham LSaad FHoffmann J(2024)Robust Resource Bounds with Static Analysis and Bayesian InferenceProceedings of the ACM on Programming Languages10.1145/36563808:PLDI(76-101)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656380
Elsman M(2023)Garbage-Collection Safety for Region-Based Type-Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/35912297:PLDI(221-243)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591229
Shaikhha AKelepeshis MGhorbani MDubach CBruening DHardekopf B(2023)Fine-Tuning Data Structures for Query ProcessingProceedings of the 21st ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3579990.3580016(149-161)Online publication date: 17-Feb-2023
https://dl.acm.org/doi/10.1145/3579990.3580016
Show More Cited By

Index Terms

Static determination of quantitative resource usage for higher-order programs
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Static determination of quantitative resource usage for higher-order programs
POPL '10

We describe a new automatic static analysis for determining upper-bound functions on the use of quantitative resources for strict, higher-order, polymorphic, recursive programs dealing with possibly-aliased data. Our analysis is a variant of Tarjan's ...
Static Resource Analysis for Java Bytecode Using Amortisation and Separation Logic

In this paper we describe a static analyser for Java bytecode which uses a combination of amortised analysis and Separation Logic due to Robert Atkey. With the help of Java annotations we are able to give precise resource utilisation constraints for ...
Simple relational correctness proofs for static analyses and program transformations
POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotationaltechniques. The key ingredients are an interpretation ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2010

520 pages

ISBN:9781605584799

DOI:10.1145/1706299

General Chair:
Manuel Hermenegildo
IMDEA-Software and T.U. of Madrid, Spain
,
Program Chair:
Jens Palsberg
UCLA, University of California, Los Angeles

ACM SIGPLAN Notices Volume 45, Issue 1
POPL '10
January 2010
500 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1707801
Issue’s Table of Contents

Copyright © 2010 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

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '10

Sponsor:

SIGPLAN

POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 17 - 23, 2010

Madrid, Spain

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

85
Total Citations
View Citations
575
Total Downloads

Downloads (Last 12 months)23
Downloads (Last 6 weeks)4

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pham LSaad FHoffmann J(2024)Robust Resource Bounds with Static Analysis and Bayesian InferenceProceedings of the ACM on Programming Languages10.1145/36563808:PLDI(76-101)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656380
Elsman M(2023)Garbage-Collection Safety for Region-Based Type-Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/35912297:PLDI(221-243)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591229
Shaikhha AKelepeshis MGhorbani MDubach CBruening DHardekopf B(2023)Fine-Tuning Data Structures for Query ProcessingProceedings of the 21st ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3579990.3580016(149-161)Online publication date: 17-Feb-2023
https://dl.acm.org/doi/10.1145/3579990.3580016
Grosen JKahn DHoffmann J(2023)Automatic Amortized Resource Analysis with Regular Recursive Types2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175720(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175720
Niu YSterling JGrodin HHarper R(2022)A cost-aware logical frameworkProceedings of the ACM on Programming Languages10.1145/34986706:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498670
Dal Lago U(2022)Implicit computation complexity in higher-order programming languagesMathematical Structures in Computer Science10.1017/S0960129521000505(1-17)Online publication date: 15-Mar-2022
https://doi.org/10.1017/S0960129521000505
Hoffmann JJost S(2022)Two decades of automatic amortized resource analysisMathematical Structures in Computer Science10.1017/S096012952100048732:6(729-759)Online publication date: 16-Mar-2022
https://doi.org/10.1017/S0960129521000487
DANNER NLICATA D(2022)Denotational semantics as a foundation for cost recurrence extraction for functional languagesJournal of Functional Programming10.1017/S095679682200003X32Online publication date: 5-Jul-2022
https://doi.org/10.1017/S095679682200003X
Avanzini MBarthe GDal Lago U(2021)On continuation-passing transformations and expected cost analysisProceedings of the ACM on Programming Languages10.1145/34735925:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473592
Rajani VGaboardi MGarg DHoffmann J(2021)A unifying type-theory for higher-order (amortized) cost analysisProceedings of the ACM on Programming Languages10.1145/34343085:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434308
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