Document Open Access Logo

Typable Fragments of Polynomial Automatic Amortized Resource Analysis

Authors Long Pham , Jan Hoffmann

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.34.pdf
  • Filesize: 0.58 MB
  • 19 pages

Document Identifiers

Author Details

Long Pham
  • Carnegie Mellon University, Pittsburgh, PA, USA
Jan Hoffmann
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This article is based on research supported by DARPA under AA Contract FA8750-18-C-0092 and by the National Science Foundation under SaTC Award 1801369, CAREER Award 1845514, and SHF Awards 1812876 and 2007784. Any opinions, findings, and conclusions contained in this document are those of the authors and do not necessarily reflect the views of the sponsoring organizations. Long Pham gratefully acknowledges the support of the Funai Overseas Scholarship by the Funai Foundation of Information Technology, Japan.

Cite AsGet BibTex

Long Pham and Jan Hoffmann. Typable Fragments of Polynomial Automatic Amortized Resource Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.34

Abstract

Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to the undecidability of resource analysis. For programmers who are unfamiliar with the technical details of AARA, it is difficult to predict whether a program can be successfully analyzed in AARA. Motivated by this problem, this article identifies classes of programs that can be analyzed in type-based polynomial AARA. Firstly, it is shown that the set of functions that are typable in univariate polynomial AARA coincides with the complexity class PTime. Secondly, the article presents a sufficient condition for typability that axiomatically requires every sub-expression of a given program to be polynomial-time. It is proved that this condition implies typability in multivariate polynomial AARA under some syntactic restrictions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Resource consumption
  • Quantitative analysis
  • Amortized analysis
  • Typability

Metrics

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

Related Versions

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), 2007. Google Scholar
  2. Martin Avanzini and Ugo Dal Lago. Automating sized-type inference for complexity analysis. Proc. ACM Program. Lang., 1(ICFP), August 2017. URL: https://doi.org/10.1145/3110287.
  3. Martin Avanzini and Georg Moser. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA'13), 2013. Google Scholar
  4. Spephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the polytime functions. computational complexity, 2(2):97-110, June 1992. URL: https://doi.org/10.1007/BF01201998.
  5. Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In 20th Int. Conf. on Tools and Alg. for the Constr. and Anal. of Systems (TACAS'14), 2014. Google Scholar
  6. Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. Relational cost analysis. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, page 316–329, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009858.
  7. Krishnendu Chatterjee, Hongfei Fu, and Aniket Murhekar. Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. In Computer Aided Verification - 29th Int. Conf. (CAV'17), 2017. Google Scholar
  8. Karl Crary and Stephnie Weirich. Resource bound certification. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’00, page 184–198, New York, NY, USA, 2000. Association for Computing Machinery. URL: https://doi.org/10.1145/325694.325716.
  9. Nils Anders Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’08, page 133–144, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1328438.1328457.
  10. Florian Frohn, M. Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen Giesl. Lower Runtime Bounds for Integer Programs. In Automated Reasoning - 8th International Joint Conference (IJCAR'16), 2016. Google Scholar
  11. Bernd Grobauer. Cost recurrences for dml programs. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, ICFP ’01, page 253–264, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/507635.507666.
  12. Martin A. T. Handley, Niki Vazou, and Graham Hutton. Liquidate your assets: Reasoning about resource usage in liquid haskell. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371092.
  13. Jan Hoffmann. Types with potential: polynomial resource bounds via automatic amortized analysis. PhD thesis, Ludwig Maximilians University Munich, 2011. URL: http://edoc.ub.uni-muenchen.de/13955/.
  14. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3), November 2012. URL: https://doi.org/10.1145/2362389.2362393.
  15. Jan Hoffmann, Ankush Das, and Shu-Chun Weng. Towards automatic resource bound analysis for ocaml. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, page 359–373, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009842.
  16. Jan Hoffmann and Martin Hofmann. Amortized resource analysis with polynomial potential. In Andrew D. Gordon, editor, Programming Languages and Systems, pages 287-306, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  17. Martin Hofmann. The strength of non-size increasing computation. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '02, pages 260-269, New York, NY, USA, 2002. ACM. URL: https://doi.org/10.1145/503272.503297.
  18. Martin Hofmann and Steffen Jost. Static prediction of heap space usage for first-order functional programs. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’03, page 185–197, New York, NY, USA, 2003. Association for Computing Machinery. URL: https://doi.org/10.1145/604131.604148.
  19. Martin Hofmann and Georg Moser. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14), 2014. Google Scholar
  20. Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. Static determination of quantitative resource usage for higher-order programs. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, page 223–236, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1706299.1706327.
  21. Steffen Jost, Pedro B. Vasconcelos, Mário Florido, and Kevin Hammond. Type-based cost analysis for lazy functional languages. Journal of Automated Reasoning, 59:87-120, 2017. URL: https://doi.org/10.1007/s10817-016-9398-9.
  22. David M. Kahn and Jan Hoffmann. Exponential automatic amortized resource analysis. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures, pages 359-380, Cham, 2020. Springer International Publishing. Google Scholar
  23. G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. Recurrence extraction for functional programs through call-by-push-value. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371083.
  24. Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas Reps. Compositional recurrence analysis revisited. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, page 248–262, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3062341.3062373.
  25. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158142.
  26. Ugo Dal Lago and Marco Gaboardi. Linear Dependent Types and Relative Completeness. In 26th IEEE Symp. on Logic in Computer Science (LICS'11), 2011. Google Scholar
  27. Daniel Leivant and Jean-Yves Marion. Lambda calculus characterizations of poly-time. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, pages 274-288, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  28. V. C. Ngo, M. Dehesa-Azuara, M. Fredrikson, and J. Hoffmann. Verifying and synthesizing constant-resource implementations with types. In 2017 IEEE Symposium on Security and Privacy (SP), pages 710-728, 2017. Google Scholar
  29. Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. Bounded expectations: Resource analysis for probabilistic programs. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, page 496–512, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3192366.3192394.
  30. Long Pham and Jan Hoffmann. Typable fragments of polynomial automatic amortized resource analysis, 2020. URL: http://arxiv.org/abs/2010.16353.
  31. Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger. Monadic refinements for relational cost analysis. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158124.
  32. Robert E. Tarjan. Amortized computational complexity. SIAM Journal on Matrix Analysis and Applications, 6(2):306-13, April 1985. Copyright - Copyright] © 1985 © Society for Industrial and Applied Mathematics; Last updated - 2012-02-28. URL: https://search-proquest-com.proxy.library.cmu.edu/docview/923648267?accountid=9902.
  33. Pedro B. Vasconcelos. Space cost analysis using sized types. PhD thesis, University of St Andrews, UK, 2008. URL: http://hdl.handle.net/10023/564.
  34. Ben Wegbreit. Mechanical program analysis. Commun. ACM, 18(9):528–539, September 1975. URL: https://doi.org/10.1145/361002.361016.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact