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

research-article

Public Access

Towards automatic resource bound analysis for OCaml

Authors:

Shu-Chun WengAuthors Info & Claims

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Pages 359 - 373

https://doi.org/10.1145/3009837.3009842

Published: 01 January 2017 Publication History

Abstract

This article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and can derive bounds for time, memory allocations and energy usage. The derived bounds are multivariate resource polynomials which are functions of different size parameters that depend on the standard OCaml types. Bound inference is fully automatic and reduced to a linear optimization problem that is passed to an off-the-shelf LP solver. Technically, the analysis system is based on a novel multivariate automatic amortized resource analysis (AARA). It builds on existing work on linear AARA for higher-order programs with user-defined inductive types and on multivariate AARA for first-order programs with built-in lists and binary trees. This is the first amortized analysis, that automatically derives polynomial bounds for higher-order functions and polynomial bounds that depend on user-defined inductive types. Moreover, the analysis handles a limited form of side effects and even outperforms the linear bound inference of previous systems. At the same time, it preserves the expressivity and efficiency of existing AARA techniques. The practicality of the analysis system is demonstrated with an implementation and integration with Inria's OCaml compiler. The implementation is used to automatically derive resource bounds for 411 functions and 6018 lines of code derived from OCaml libraries, the CompCert compiler, and implementations of textbook algorithms. In a case study, the system infers bounds on the number of queries that are sent by OCaml programs to DynamoDB, a commercial NoSQL cloud database service.

References

[1]

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In 16th European Symposium on Programming (ESOP’07), pages 157–172, 2007.

Digital Library

[2]

E. Albert, P. Arenas, S. Genaim, and G. Puebla. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning, pages 161–203, 2011.

Digital Library

[3]

E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, and G. Puebla. Automatic Inference of Resource Consumption Bounds. In Logic for Programming, Artificial Intelligence, and Reasoning, 18th Conference (LPAR’12), pages 1–11, 2012.

Digital Library

[4]

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science, 413(1):142 – 159, 2012.

Digital Library

[5]

E. Albert, J. C. Fernández, and G. Román-Díez. Non-cumulative Resource Analysis. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, (TACAS’15), pages 85–100, 2015.

Digital Library

[6]

C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In 17th International Static Analysis Symposium (SAS’10), pages 117–133, 2010.

Digital Library

[7]

D. E. Alonso-Blas and S. Genaim. On the limits of the classical approach to cost analysis. In 19th International Static Analysis Symposium (SAS’12), pages 405–421, 2012.

Digital Library

[8]

R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th European Symposium on Programming (ESOP’10), pages 85–103, 2010.

Digital Library

[9]

M. Avanzini and G. Moser. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA’13), pages 55–70, 2013.

[10]

M. Avanzini, U. D. Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In 29th International Conference on Functional Programming (ICFP’15), pages 152–164, 2012.

Digital Library

[11]

R. Benzinger. Automated Higher-Order Complexity Analysis. Theoretical Computer Science, 318(1-2):79–103, 2004.

Digital Library

[12]

R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács. ABC: Algebraic Bound Computation for Loops. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference (LPAR’10), pages 103–118, 2010.

Digital Library

[13]

G. E. Blelloch and J. Greiner. A Provable Time and Space Efficient Implementation of NESL. In First International Conference on Functional Programming (ICFP’96), pages 213–225, 1996.

Digital Library

[14]

G. E. Blelloch and R. Harper. Cache and I/O Efficent Functional Algorithms. In 40th Symposium on Principles of Programming Languages (POPL’13), pages 39–50, 2013.

Digital Library

[15]

M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference (TACAS’14), pages 140–155, 2014.

[16]

B. Campbell. Amortised Memory Analysis using the Depth of Data Structures. In 18th European Symposium on Programming (ESOP’09), pages 190–204, 2009.

Digital Library

[17]

Q. Carbonneaux, J. Hoffmann, and Z. Shao. Compositional Certified Resource Bounds. In 36th Conference on Programming Language Design and Implementation (PLDI’15), pages 467–478, 2015.

Digital Library

[18]

P. Cerný, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr. Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP’15), pages 105– 131, 2015.

[19]

E. Çiçek, D. Garg, and U. A. Acar. Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP’15), pages 406–431, 2015.

[20]

K. Crary and S. Weirich. Resource Bound Certification. In 27th Symposium on Principles of Programming Languages (POPL’00), pages 184–198, 2000.

Digital Library

[21]

S. A. Crosby and D. S. Wallach. Denial of service via algorithmic complexity attacks. In 12th USENIX Security Symposium (USENIX’12), pages 3–3, 2003.

Digital Library

[22]

N. A. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th Symposium on Principles of Programming Languauges (POPL’08), pages 133–144, 2008.

Digital Library

[23]

N. Danner, D. R. Licata, and R. Ramyaa. Denotational Cost Semantics for Functional Languages with Inductive Types. In 29th International Conference on Functional Programming (ICFP’15), pages 140–151, 2012.

Digital Library

[24]

N. Danner, J. Paykin, and J. S. Royer. A Static Cost Analysis for a Higher-Order Language. In 7th Workshop on Programming Languages Meets Program Verification (PLPV’13), pages 25–34, 2013.

Digital Library

[25]

A. Flores-Montoya and R. Hähnle. Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems - 12th Asian Symposium (APLAS’14), pages 275–295, 2014.

[26]

B. Grobauer. Cost Recurrences for DML Programs. In 6th International Conference on Functional Programming (ICFP’01), pages 253–264, 2001.

Digital Library

[27]

S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th Symposium on Principles of Programming Languauges (POPL’09), pages 127–139, 2009.

Digital Library

[28]

J. Hoffmann. RAML Web Site. http://raml.co, 2016.

[29]

J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP’10), pages 287–306, 2010.

Digital Library

[30]

J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In Programming Languages and Systems - 8th Asian Symposium (APLAS’10), pages 172–187, 2010.

Digital Library

[31]

J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. In 38th Symposium on Principles of Programming Languages (POPL’11), pages 357–370, 2011.

Digital Library

[32]

J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. ACM Transactions on Programming Languages and Systems, 34:14:1–14:62, 2012.

Digital Library

[33]

J. Hoffmann, A. Das, and S.-C. Weng. Towards Automatic Resource Bound Analysis for OCaml. ArXiv e-prints, 2016.

[34]

M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In 30th Symposium on Principles of Programming Languages (POPL’03), pages 185–197, 2003.

Digital Library

[35]

M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis. In 15th European Symposium on Programming (ESOP’06), pages 22– 37, 2006.

Digital Library

[36]

M. Hofmann and G. Moser. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14), pages 272–286, 2014.

[37]

M. Hofmann and G. Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA’15), pages 241–256, 2015.

[38]

M. Hofmann and D. Rodriguez. Automatic Type Inference for Amortised Heap-Space Analysis. In 22nd European Symposium on Programming (ESOP’13), pages 593–613, 2013.

Digital Library

[39]

J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In 23rd Symposium on Principles of Programming Languages (POPL’96), pages 410–423, 1996.

Digital Library

[40]

G. Jin, L. Song, X. Shi, J. Scherpelz, and S. Lu. Understanding and Detecting Real-World Performance Bugs. In 33rd Conference on Programming Language Design and Implementation PLDI’12, pages 77–88, 2012.

Digital Library

[41]

S. Jost, K. Hammond, H.-W. Loidl, and M. Hofmann. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In 37th Symposium on Principles of Programming Languages (POPL’10), pages 223–236, 2010.

Digital Library

[42]

P. C. Kocher. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Advances in Cryptology - 16th Annual International Cryptology Conference (CRYPTO’96), pages 104– 113, 1996.

Digital Library

[43]

U. D. Lago and M. Gaboardi. Linear Dependent Types and Relative Completeness. In 26th IEEE Symposium on Logic in Computer Science (LICS’11), pages 133–142, 2011.

Digital Library

[44]

U. D. Lago and B. Petit. The Geometry of Types. In 40th Symposium on Principles of Programming Languages (POPL’13), pages 167–178, 2013.

Digital Library

[45]

X. Leroy. The ZINC Experiment: An Economical Implementation of the ML Language. Technical report 117, INRIA, 1990.

[46]

X. Leroy. From Krivine’s Machine to the Caml Implementation. http://pauillac.inria.fr/~xleroy/talks/zam-kazam05.pdf, 2005. Invited talk, May 17, Workshop on the Krivine and ZINC Abstract Machines.

[47]

X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7):107–115, 2009.

Digital Library

[48]

X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy, and J. Vouillon. The OCaml system release 4.02. Technical report, Institut National de Recherche en Informatique et en Automatique, 2014.

[49]

V. Nicollet. 99 problems (solved) in ocaml. https://ocaml.org/ learn/tutorials/99problems.html, 2016.

[50]

L. Noschinski, F. Emmes, and J. Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. Journal of Automated Reasoning, 51(1):27–56, 2013.

[51]

O. Olivo, I. Dillig, and C. Lin. Static Detection of Asymptotic Performance Bugs in Collection Traversals. In Conference on Programming Language Design and Implementation (PLDI’15), pages 369–378, 2015.

Digital Library

[52]

H. R. Simões, P. B. Vasconcelos, M. Florido, S. Jost, and K. Hammond. Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. In 17th International Conference on Functional Programming (ICFP’12), pages 165–176, 2012.

Digital Library

[53]

M. Sinn, F. Zuleger, and H. Veith. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification - 26th International Conference (CAV’14), page 743–759, 2014.

Digital Library

[54]

R. E. Tarjan. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods, 6(2):306–318, 1985.

Digital Library

[55]

R. J. Vanderbei. Linear Programming: Foundations and Extensions. Springer US, 2001.

[56]

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

[57]

P. B. Vasconcelos and K. Hammond. Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs. In 15th International Conference on Implementation of Functional Languages (IFL’03), pages 86–101, 2003.

Digital Library

[58]

P. B. Vasconcelos, S. Jost, M. Florido, and K. Hammond. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP’15), pages 787– 811, 2015.

[59]

B. Wegbreit. Mechanical Program Analysis. Communications of the ACM, 18(9):528–539, 1975.

Digital Library

[60]

F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th International Static Analysis Symposium (SAS’11), pages 280–297, 2011.

Digital Library

[61]

E. Çiçek, G. Barthe, M. Gaboardi, D. Garg, and J. Hoffmann. Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL’17), 2017. Forthcoming.

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
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649824
Muller SHoffmann J(2024)Modeling and Analyzing Evaluation Cost of CUDA KernelsACM Transactions on Parallel Computing10.1145/363940311:1(1-53)Online publication date: 12-Jan-2024
https://dl.acm.org/doi/10.1145/3639403
Show More Cited By

Index Terms

Towards automatic resource bound analysis for OCaml
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Compositional certified resource bounds
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

This paper presents a new approach for automatically deriving worst-case resource bounds for C programs. The described technique combines ideas from amortized analysis and abstract interpretation in a unified framework to address four challenges for ...
Multivariate amortized resource analysis
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization, or sized types bound the resource usage or result size of such a procedure by a sum of ...
Towards automatic resource bound analysis for OCaml
POPL '17

This article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

January 2017

901 pages

ISBN:9781450346603

DOI:10.1145/3009837

General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

ACM SIGPLAN Notices Volume 52, Issue 1
POPL '17
January 2017
901 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3093333
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2017 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 the author(s) 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

POPL '17

Sponsor:

SIGPLAN

POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 15 - 21, 2017

Paris, France

Acceptance Rates

Overall Acceptance Rate 800 of 4,009 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

87
Total Citations
View Citations
1,191
Total Downloads

Downloads (Last 12 months)183
Downloads (Last 6 weeks)16

Reflects downloads up to 12 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
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649824
Muller SHoffmann J(2024)Modeling and Analyzing Evaluation Cost of CUDA KernelsACM Transactions on Parallel Computing10.1145/363940311:1(1-53)Online publication date: 12-Jan-2024
https://dl.acm.org/doi/10.1145/3639403
Atkey R(2024)Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages10.1145/36329188:POPL(2288-2317)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632918
Lommen NMeyer ÉGiesl J(2024)Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)Automated Reasoning10.1007/978-3-031-63498-7_14(233-243)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_14
Ishimwe DChandra SBlincoe KTonella P(2023)Inferring Complexity Bounds from Recurrence RelationsProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3617853(2198-2200)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3617853
Chen CZhang ZTian HYan SXu HChandra SBlincoe KTonella P(2023)OOM-Guard: Towards Improving the Ergonomics of Rust OOM Handling via a Reservation-Based ApproachProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616303(733-744)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616303
Zhang TSharma UKapritsos M(2023)Performal: Formal Verification of Latency Properties for Distributed SystemsProceedings of the ACM on Programming Languages10.1145/35912357:PLDI(368-393)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591235
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
Das AWang DHoffmann J(2023)Probabilistic Resource-Aware Session TypesProceedings of the ACM on Programming Languages10.1145/35712597:POPL(1925-1956)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571259
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents