Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-20T03:32:47.319Z Has data issue: false hasContentIssue false
  • English
  • Français

Type-based amortized resource analysis with integers and arrays*

Part of: JFP Research Articles

Published online by Cambridge University Press:  29 October 2015

JAN HOFFMANN  and
ZHONG SHAO
JAN HOFFMANN
Affiliation:
Department of Computer Science, Yale University, 51 Prospect St., New Haven, CT 06511, USA (e-mail: jan.hoffmann@yale.edu, zhong.shao@yale.edu)
ZHONG SHAO
Affiliation:
Department of Computer Science, Yale University, 51 Prospect St., New Haven, CT 06511, USA (e-mail: jan.hoffmann@yale.edu, zhong.shao@yale.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Proving bounds on the resource consumption of a program by statically analyzing its source code is an important and well-studied problem. Automatic approaches for numeric programs with side effects usually apply abstract interpretation-based invariant generation to derive bounds on loops and recursion depths of function calls. This article presents an alternative approach to resource-bound analysis for numeric and heap-manipulating programs that uses type-based amortized resource analysis. As a first step towards the analysis of imperative code, the technique is developed for a first-order ML-like language with unsigned integers and arrays. The analysis automatically derives bounds that are multivariate polynomials in the numbers and the lengths of the arrays in the input. Experiments with example programs demonstrate two main advantages of amortized analysis over current abstract interpretation–based techniques. For one thing, amortized analysis can handle programs with non-linear intermediate values like f((n + m)2). For another thing, amortized analysis is compositional and works naturally for compound programs like f(g(x)).

Type
Articles
Information
Journal of Functional Programming , Volume 25 , 2015 , e17
Copyright
Copyright © Cambridge University Press 2015 

Footnotes

*

This research is based on work supported in part by NSF grants 1319671 and 1065451, and DARPA grants FA8750-10-2-0254 and FA8750-12-2-0293. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies.

References

Aehlig, K., Hofmann, M. & Hoffmann, J. (2010–2013) RAML Web Site. Available at: http://raml.tcs.ifi.lmu.de.Google Scholar
Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M. & Puebla, G. (2012a) Automatic inference of resource consumption bounds. In Logic for Programming, Artificial Intelligence, and Reasoning, 18th Conference (LPAR'18), Mérida, Venezuela, pp. 1–11.*CrossRefGoogle Scholar
Albert, E., Arenas, P., Genaim, S. & Puebla, G. (2011) Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46 (2), 161–203.CrossRefGoogle Scholar
Albert, E., Arenas, P., Genaim, S., Puebla, G. & Zanardini, D. (2012b) Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413 (1), 142–159.CrossRefGoogle Scholar
Alias, C., Darte, A., Feautrier, P. & Gonnord, L. (2010) Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of 17th International Static Analysis Symposium (SAS'10), Perpignan, France, pp. 117–133.CrossRefGoogle Scholar
Alonso-Blas, D. E., Arenas, P. & Genaim, S. (2011) Handling non-linear operations in the value analysis of COSTA. Electr. Notes Theor. Comput. Sci. 279 (1), 3–17.CrossRefGoogle Scholar
Alonso-Blas, D. E. & Genaim, S. (2012) On the limits of the classical approach to cost analysis. In Proceedings of 19th International Static Analysis Symposium (SAS'12), Deauville, France, pp. 405–421.CrossRefGoogle Scholar
Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C. & Giesl, J. (2014) Alternating runtime and size complexity analysis of integer programs. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. (TACAS'14), Held as Part of the European Joint Conferences on Theory and Practice of Software, (ETAPS'14), Grenoble, France, pp. 140–155.CrossRefGoogle Scholar
Carbonneaux, Q., Hoffmann, J., Ramananandro, T. & Shao, Z. (2014) End-to-end verification of stack-space bounds for C programs. In Proceedings of the Conference on Programming Language Design and Implementation. (PLDI'14), Edinburgh, Scotland, p. 30.CrossRefGoogle Scholar
Carbonneaux, Q., Hoffmann, J. & Shao, Z. (2015) Compositional certified resource bounds. In Proceedings of 36th Conference on Programming Language Design and Implementation (PLDI'15). Portland, OR, USA, pp. 467–478. Forthcoming.CrossRefGoogle Scholar
Cousot, P. & Halbwachs, N. (1978) Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM Symposium on Principles Programming Languages. (POPL'78), Tucson, Arizona, USA, pp. 84–96.CrossRefGoogle Scholar
Gulavani, B. S. & Gulwani, S. (2008) A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In Proceedings of the 20th International Conference Computer Aided Verification. (CAV '08), Princeton, NJ, USA, pp. 370–384.CrossRefGoogle Scholar
Gulwani, S., Mehra, K. K. & Chilimbi, T. M. (2009) SPEED: Precise and efficient static estimation of program computational complexity. In Proceedings of 36th ACM Symposium on Principles of Programming Languages. (POPL'09), Savannah, GA, USA, pp. 127–139.CrossRefGoogle Scholar
Hoffmann, J. & Hofmann, M. (2010a) Amortized resource analysis with polynomial potential. In Proceedings of the 19th European Symposium on Programming. (ESOP'10), Paphos, Cyprus, pp. 287–306.CrossRefGoogle Scholar
Hoffmann, J. & Hofmann, M. (2010b) Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In Proceedings of the 8th Asian Symposium on Programming Languages and Systems. (APLAS'10). Shanghai, China, pp. 172–187.CrossRefGoogle Scholar
Hoffmann, J. & Shao, Z. (2014) Type-based amortized resource analysis with integers and arrays. In Proceedings of 12th International Symposium on Functional and Logic Programming. (FLOPS'14), Kanazawa, Japan, pp. 152–168.CrossRefGoogle Scholar
Hoffmann, J., Aehlig, K. & Hofmann, M. (2011) Multivariate amortized resource analysis. In Proceedings of 38th ACM Symposium on Principles of Programming Languages. (POPL'11), Austin, TX, USA, pp. 357–370.CrossRefGoogle Scholar
Hoffmann, J., Aehlig, K. & Hofmann, M. (2012a) Multivariate amortized resource analysis. Acm Trans. Program. Lang. Syst. 34 (3), 14.CrossRefGoogle Scholar
Hoffmann, J., Aehlig, K. & Hofmann, M. (2012b) Resource aware ML. In Proceedings of 24th International Conference on Computer Aided Verification. (CAV'12), Berkeley, CA, USA, pp. 781–786.CrossRefGoogle Scholar
Hofmann, M. & Jost, S. (2003) Static prediction of heap space usage for first-order functional programs. In Proceedings of 30th ACM Symposium on Principles of Programming Languages. (POPL'03), New Orleans, Louisisana, pp. 185–197.CrossRefGoogle Scholar
Leroy, X. (2006) Coinductive big-step operational semantics. In Proceedings of 15th European Symposium on Programming. (ESOP'06), Vienna, Austria, pp. 54–68.CrossRefGoogle Scholar
Miné, A. (2004) Weakly Relational Numerical Abstract Domains. Ph.D. thesis, École Polytechnique, Paris, France.Google Scholar
Riordan, J. & Stein, P. R. (1972) Arrangements on chessboards. J. Comb. Theory, Ser. A 12 (1), 72–80.CrossRefGoogle Scholar
Sankaranarayanan, S., Ivancic, F., Shlyakhter, I. & Gupta, A. (2006) Static analysis in disjunctive numerical domains. Proceedings of 13th International Static Analysis Symposium. (SAS'06), Seoul, Korea, pp. 3–17.CrossRefGoogle Scholar
Sinn, M., Zuleger, F. & Veith, H. (2014) A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proceedings of 26th International Conference on Computer Aided Verification. (CAV'14), Vienna, Austria, pp. 743–759.CrossRefGoogle Scholar
Vanderbei, R. J. (2001) Linear Programming: Foundations and Extensions. USA: Springer.CrossRefGoogle Scholar
Zuleger, F., Sinn, M., Gulwani, S. & Veith, H. (2011) Bound analysis of imperative programs with the size-change abstraction. In Proceedings of 18th International Static Analysis Symposium. (SAS'11), Venice, Italy, pp. 280–297.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.