Arrays and References in Resource Aware ML

Authors Benjamin Lichtman, Jan Hoffmann



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.26.pdf
  • Filesize: 0.59 MB
  • 20 pages

Document Identifiers

Author Details

Benjamin Lichtman
Jan Hoffmann

Cite AsGet BibTex

Benjamin Lichtman and Jan Hoffmann. Arrays and References in Resource Aware ML. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.26

Abstract

This article introduces a technique to accurately perform static prediction of resource usage for ML-like functional programs with references and arrays. Previous research successfully integrated the potential method of amortized analysis with a standard type system to automatically derive parametric resource bounds. The analysis is naturally compositional and the resource consumption of functions can be abstracted using potential-annotated types. The soundness theorem of the analysis guarantees that the derived bounds are correct with respect to the resource usage defined by a cost semantics. Type inference can be efficiently automated using off-the-shelf LP solvers, even if the derived bounds are polynomials. However, side effects and aliasing of heap references make it notoriously difficult to derive bounds that depend on mutable structures, such as arrays and references. As a result, existing automatic amortized analysis systems for ML-like programs cannot derive bounds for programs whose resource consumption depends on data in such structures. This article extends the potential method to handle mutable structures with minimal changes to the type rules while preserving the stated advantages of amortized analysis. To do so, we introduce a swap operation for references and arrays that users can use to make programs suitable for automatic analysis. We prove the soundness of the analysis introducing a potential-annotated memory typing, which gathers all unique locations reachable from a reference. Apart from the design of the system, the main contribution is the proof of soundness for the extended analysis system.
Keywords
  • Resource Analysis
  • Functional Programming
  • Static Analysis
  • OCaml
  • Amortized Analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Cost Analysis of Java Bytecode. In 16th Euro. Symp. on Prog. (ESOP'07), pages 157-172, 2007. Google Scholar
  2. Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, and Guillermo Román-Díez. Verified Resource Guarantees for Heap Manipulating Programs. In 15th Int. Conf. on Fundamental Approaches to Software Engineering (FASE'12), pages 130-145, 2012. Google Scholar
  3. Elvira Albert, Jesús Correas Fernández, and Guillermo Román-Díez. Non-cumulative Resource Analysis. In Tools and Algorithms for the Construction and Analysis of Systems - 21st Int. Conf., (TACAS'15), pages 85-100, 2015. Google Scholar
  4. Robert Atkey. Amortised Resource Analysis with Separation Logic. In 19th Euro. Symp. on Prog. (ESOP'10), pages 85-103, 2010. Google Scholar
  5. Martin Avanzini, Ugo Dal Lago, and Georg Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In 29th Int. Conf. on Functional Programming (ICFP'15), 2012. Google Scholar
  6. Ralph Benzinger. Automated Higher-Order Complexity Analysis. Theor. Comput. Sci., 318(1-2):79-103, 2004. Google Scholar
  7. Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, and Laura Kovács. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int. Conf. (LPAR'10), pages 103-118, 2010. Google Scholar
  8. Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int. Conf. (TACAS'14), pages 140-155, 2014. Google Scholar
  9. Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao. Compositional Certified Resource Bounds. In 36th Conference on Programming Language Design and Implementation (PLDI'15), 2015. Artifact submitted and approved. Google Scholar
  10. Pavol Cerný, Thomas A. Henzinger, Laura Kovács, Arjun Radhakrishna, and Jakob Zwirchmayr. Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP'15), pages 105-131, 2015. Google Scholar
  11. Ezgi Çiçek, Deepak Garg, and Umut A. Acar. Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP'15), pages 406-431, 2015. Google Scholar
  12. Nils Anders Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th ACM Symp. on Principles Prog. Langs. (POPL'08), pages 133-144, 2008. Google Scholar
  13. Norman Danner, Daniel R. Licata, and Ramyaa Ramyaa. Denotational Cost Semantics for Functional Languages with Inductive Types. In 29th Int. Conf. on Functional Programming (ICFP'15), 2012. Google Scholar
  14. Antonio Flores-Montoya. Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. In Formal Methods - 21st International Symposium (FM'16), pages 254-273, 2016. Google Scholar
  15. Antonio Flores-Montoya and Reiner Hähnle. Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems - 12th Asian Symposiu (APLAS'14), pages 275-295, 2014. Google Scholar
  16. Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th ACM Symp. on Principles of Prog. Langs. (POPL'09), pages 127-139, 2009. Google Scholar
  17. Sumit Gulwani and Florian Zuleger. The Reachability-Bound Problem. In Conf. on Prog. Lang. Design and Impl. (PLDI'10), pages 292-304, 2010. Google Scholar
  18. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate Amortized Resource Analysis. In 38th Symposium on Principles of Programming Languages (POPL'11), 2011. Google Scholar
  19. Jan Hoffmann, Ankush Das, and Shu-Chun Weng. Towards Automatic Resource Bound Analysis for OCaml. In 44th Symposium on Principles of Programming Languages (POPL'17), 2017. Google Scholar
  20. Jan Hoffmann and Martin Hofmann. Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP'10), 2010. Google Scholar
  21. Jan Hoffmann and Zhong Shao. Type-Based Amortized Resource Analysis with Integers and Arrays. In 12th International Symposium on Functional and Logic Programming (FLOPS'14), 2014. Google Scholar
  22. Martin Hofmann and Steffen Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In 30th ACM Symp. on Principles of Prog. Langs. (POPL'03), pages 185-197, 2003. Google Scholar
  23. Martin Hofmann and Steffen Jost. Type-Based Amortised Heap-Space Analysis. In 15th Euro. Symp. on Prog. (ESOP'06), pages 22-37, 2006. URL: http://dx.doi.org/10.1007/11693024_3.
  24. Martin Hofmann and Georg Moser. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14), pages 272-286, 2014. Google Scholar
  25. Martin Hofmann and Georg 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. Google Scholar
  26. Martin Hofmann and Dulma Rodriguez. Efficient Type-Checking for Amortised Heap-Space Analysis. In 18th Conf. on Comp. Science Logic (CSL'09). LNCS, 2009. Google Scholar
  27. Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In 37th ACM Symp. on Principles of Prog. Langs. (POPL'10), pages 223-236, 2010. Google Scholar
  28. Ugo Dal Lago and Marco Gaboardi. Linear Dependent Types and Relative Completeness. In 26th IEEE Symp. on Logic in Computer Science (LICS'11), pages 133-142, 2011. Google Scholar
  29. Ugo Dal Lago and Barbara Petit. The Geometry of Types. In 40th ACM Symp. on Principles Prog. Langs. (POPL'13), pages 167-178, 2013. Google Scholar
  30. Benjamin Lichtman and Jan Hoffmann. Arrays and references in resource aware ml. Technical report, Carnegie Mellon University, 2017. Google Scholar
  31. Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. Contract-based resource verification for higher-order functions with memoization. In 44th Symposium on Principles of Programming Languages POPL'17, 2017. Google Scholar
  32. Greg Morrisett, Amal Ahmed, and Matthew Fluet. L3: A linear language with locations. In Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings, pages 293-307, 2005. Google Scholar
  33. Lars Noschinski, Fabian Emmes, and Jürgen Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Autom. Reasoning, 51(1):27-56, 2013. Google Scholar
  34. Benjamin C. Pierce. Advanced Topics in Types and Programming Languages. The MIT Press, 2004. Google Scholar
  35. Moritz Sinn, Florian Zuleger, and Helmut Veith. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification - 26th Int. Conf. (CAV'14), pages 743-759, 2014. Google Scholar
  36. Frederick Smith, David Walker, and J. Gregory Morrisett. Alias types. In Proceedings of the 9th European Symposium on Programming Languages and Systems, ESOP'00, pages 366-381, London, UK, UK, 2000. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=645394.651903.
  37. Pedro B. Vasconcelos, Steffen Jost, Mário Florido, and Kevin Hammond. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP'15), pages 787-811, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail