Abstract
Automatic amortized resource analysis (AARA) is a type-based technique for inferring concrete (non-asymptotic) bounds on a program’s resource usage. Existing work on AARA has focused on bounds that are polynomial in the sizes of the inputs. This paper presents and extension of AARA to exponential bounds that preserves the benefits of the technique, such as compositionality and efficient type inference based on linear constraint solving. A key idea is the use of the Stirling numbers of the second kind as the basis of potential functions, which play the same role as the binomial coefficients in polynomial AARA. To formalize the similarities with the existing analyses, the paper presents a general methodology for AARA that is instantiated to the polynomial version, the exponential version, and a combined system with potential functions that are formed by products of Stirling numbers and binomial coefficients. The soundness of exponential AARA is proved with respect to an operational cost semantics and the analysis of representative example programs demonstrates the effectiveness of the new analysis.
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, SHF Award 1812876, and CAREER Award 1845514. 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.
Chapter PDF
Similar content being viewed by others
Keywords
References
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: 16th Euro. Symp. on Prog. (ESOP’07) (2007)
Albert, E., Fernández, J.C., Román-Díez, G.: Non-cumulative Resource Analysis. In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, (TACAS’15) (2015)
Albert, E., Genaim, S., Masud, A.N.: On the Inference of Resource Usage Upper and Lower Bounds. ACM Transactions on Computational Logic 14(3) (2013)
Atkey, R.: Amortised Resource Analysis with Separation Logic. In: 19th Euro. Symp. on Prog. (ESOP’10) (2010)
Avanzini, M., Lago, U.D., Moser, G.: Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In: 29th Int. Conf. on Functional Programming (ICFP’15) (2012)
Avanzini, M., Moser, G.: A Combination Framework for Complexity. In: 24th International Conference on Rewriting Techniques and Applications (RTA’13) (2013)
Blanc, R., Henzinger, T.A., Hottelier, T., Kovács, L.: ABC: Algebraic Bound Computation for Loops. In: Logic for Prog., AI., and Reasoning - 16th Int. Conf. (LPAR’10) (2010)
Carbonneaux, Q., Hoffmann, J., Reps, T., Shao, Z.: Automated Resource Analysis with Coq Proof Objects. In: 29th International Conference on Computer-Aided Verification (CAV’17) (2017)
Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional Certified Resource Bounds. In: 36th Conference on Programming Language Design and Implementation (PLDI’15) (2015), artifact submitted and approved
Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. In: Computer Aided Verification - 29th International Conference (CAV ’17). pp. 41–63 (2017)
Dal Lago, U., Gaboardi, M.: Linear Dependent Types and Relative Completeness. In: 26th IEEE Symp. on Logic in Computer Science (LICS’11) (2011)
Danner, N., Licata, D.R., Ramyaa, R.: Denotational Cost Semantics for Functional Languages with Inductive Types. In: 29th Int. Conf. on Functional Programming (ICFP’15) (2012)
Das, A., Hoffmann, J., Pfenning, F.: Work analysis with resource-aware session types. In: 33th ACM/IEEE Symposium on Logic in Computer Science (LICS’18) (2018)
Fagin, R.: Generalized First-Order Spectra, and Polynomial-Time Recognizable Sets. SIAM-AMS Proc. 7 (01 1974)
Flajolet, P., Salvy, B., Zimmermann, P.: Automatic Average-case Analysis of Algorithms. Theoret. Comput. Sci. 79(1), 37–109 (1991)
Flores-Montoya, A., Hähnle, R.: Resource Analysis of Complex Programs with Cost Equations. In: Programming Languages and Systems - 12th Asian Symposiu (APLAS’14) (2014)
Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower Runtime Bounds for Integer Programs. In: Automated Reasoning - 8th International Joint Conference (IJCAR’16) (2016)
Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: 36th ACM Symp. on Principles of Prog. Langs. (POPL’09) (2009)
Guéneau, A., Charguéraud, A., Pottier, F.: A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 10801, pp. 533–560. Springer (Apr 2018)
Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press (2016)
Hindley, R.: The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society 146, 29–60 (1969), http://www.jstor.org/stable/1995158
Hoffmann, J.: Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Ph.D. thesis, Ludwig-Maximilians-Universität München (2011)
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis. In: 38th Symposium on Principles of Programming Languages (POPL’11) (2011)
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis. ACM Trans. Program. Lang. Syst. (2012)
Hoffmann, J., Das, A., Weng, S.C.: Towards Automatic Resource Bound Analysis for OCaml. In: 44th Symposium on Principles of Programming Languages (POPL’17) (2017)
Hoffmann, J., Hofmann, M.: Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In: 8th Asian Symposium on Programming Languages (APLAS’10) (2010)
Hoffmann, J., Hofmann, M.: Amortized Resource Analysis with Polynomial Potential. In: 19th European Symposium on Programming (ESOP’10) (2010)
Hoffmann, J., Shao, Z.: Type-Based Amortized Resource Analysis with Integers and Arrays. In: 12th International Symposium on Functional and Logic Programming (FLOPS’14) (2014)
Hoffmann, J., Shao, Z.: Automatic Static Cost Analysis for Parallel Programs. In: 24th European Symposium on Programming (ESOP’15) (2015)
Hoffmann, J., Shao, Z.: Type-Based Amortized Resource Analysis with Integers and Arrays. J. Funct. Program. (2015)
Hofmann, M., Jost, S.: Static Prediction of Heap Space Usage for First-Order Functional Programs. In: 30th ACM Symp. on Principles of Prog. Langs. (POPL’03) (2003)
Hofmann, M., Moser, G.: Analysis of logarithmic amortised complexity (2018)
Jost, S., Hammond, K., Loidl, H.W., Hofmann, M.: Static Determination of Quantitative Resource Usage for Higher-Order Programs. In: 37th ACM Symp. on Principles of Prog. Langs. (POPL’10) (2010)
Jost, S., Loidl, H.W., Hammond, K., Scaife, N., Hofmann, M.: Carbon Credits for Resource-Bounded Computations using Amortised Analysis. In: 16th Symp. on Form. Meth. (FM’09) (2009)
Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs. In: Proceedings of the European Symposium on Programming Languages and Systems (ESOP’16). Springer (2016)
Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.: Compositional recurrence analysis revisited. In: Conference on Programming Language Design and Implementation (PLDI’17) (2017)
Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), 54:1–54:33 (Dec 2017)
Lichtman, B., Hoffmann, J.: Arrays and References in Resource Aware ML. In: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD’17) (2017)
Madhavan, R., Kulal, S., Kuncak, V.: Contract-based resource verification for higher-order functions with memoization. In: Proceedings of the 44th Symposium on Principles of Programming Languages (POPL’17) (2017)
Matiyasevich, Y.V.: The Diophantineness of Enumerable Sets. In: Doklady Akademii Nauk. vol. 191, pp. 279–282. Russian Academy of Sciences (1970)
Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 348–375 (1978)
Mével, G., Jourdan, J.H., Pottier, F.: Time credits and time receipts in Iris. In: Caires, L. (ed.) European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 11423, pp. 1–27. Springer (Apr 2019)
Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. In: 39th Conference on Programming Language Design and Implementation (PLDI’18) (2018)
Ngo, V.C., Dehesa-Azuara, M., Fredrikson, M., Hoffmann, J.: Verifying and Synthesizing Constant-Resource Implementations with Types. In: 38th IEEE Symposium on Security and Privacy (S&P ’17) (2017)
Nipkow, T., Brinkop, H.: Amortized complexity verified. J. Autom. Reasoning 62(3), 367–391 (2019)
Niu, Y., Hoffmann, J.: Automatic space bound analysis for functional programs with garbage collection. In: 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR’18) (2018)
Noschinski, L., Emmes, F., Giesl, J.: Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Autom. Reasoning 51(1), 27–56 (2013)
Radiček, I., Barthe, G., Gaboardi, M., Garg, D., Zuleger, F.: Monadic Refinements for Relational Cost Analysis. Proc. ACM Program. Lang. 2(POPL) (2017)
Sinn, M., Zuleger, F., Veith, H.: A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In: Computer Aided Verification - 26th Int. Conf. (CAV’14) (2014)
Stirling, J.: The Differential Method: Or, A Treatise Concerning Summation and Interpolation of Infinite Series. E. Cave (1749)
Tarjan, R.E.: Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods 6(2), 306–318 (1985)
Vasconcelos, P.B., Jost, S., Florido, M., Hammond, K.: Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In: 24th European Symposium on Programming (ESOP’15) (2015)
Wang, P., Wang, D., Chlipala, A.: TiML: A Functional Language for Practical Complexity Analysis with Invariants. In: Object-Oriented Prog., Syst., Lang., and Applications (OOPSLA’17) (2017)
Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’19). pp. 204–220 (2019)
Wegbreit, B.: Mechanical Program Analysis. Commun. ACM 18(9), 528–539 (1975)
Çiçek, E., Barthe, G., Gaboardi, M., Garg, D., Hoffmann, J.: Relational Cost Analysis. In: 44th Symposium on Principles of Programming Languages (POPL’17) (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Kahn, D.M., Hoffmann, J. (2020). Exponential Automatic Amortized Resource Analysis. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)