Skip to main content
SpringerLink
Log in

Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9995))

Included in the following conference series:

Abstract

Resource analysis aims at statically obtaining bounds on the resource consumption of programs in terms of input parameters. A well known approach to resource analysis is based on transforming the target program into a set of cost relations, then solving these into a closed-form bound. In this paper we develop a new analysis for computing upper and lower cost bounds of programs expressed as cost relations. The analysis is compositional: it computes the cost of each loop or function separately and composes the obtained expressions to obtain the total cost. Despite being modular, the analysis can obtain precise upper and lower bounds of programs with amortized cost. The key is to obtain bounds that depend on the values of the variables at the beginning and at the end of each program part. In addition we use a novel cost representation called cost structure. It allows to reduce the inference of complex polynomial expressions to a set of linear problems that can be solved efficiently. We implemented our method and performed an extensive experimental evaluation that demonstrates its power.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/aeflores/CoFloCo.

  2. 2.

    This can be easily seen by distinguishing cases (\(l(\overline{y})\ge 0\) and \(l(\overline{y})\le 0\)).

  3. 3.

    We could also approximate to \(\lfloor iv \rfloor _k* smiv _p\) and \(\lceil iv \rceil _k* smiv _p\) but in general the chosen approximation works better. The variable \( iv _k\) usually represents an outer loop and \( iv _p\) and inner loop (See basic product strategy in Sect. 5.2).

  4. 4.

    This transformation is not valid for constraints with multiple variables on the left side. The constraints with \(\le \) can be split (\(\sum _{k=1}^m iv _k \le SE \) implies \( iv _k \le SE \) for \(1\le k\le m\)). But this is not the case for the constraints with \(\ge \).

  5. 5.

    The class Rst will be used and explained in the Max-Min strategy.

  6. 6.

    \( smiv _{it_{3.1}}\) and \( smiv _{it_{3.2}}\) are actually not needed for computing the cost of the program in this case. Therefore, these constraints are never added to the pending sets.

References

  1. Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G., COSTABS: a cost and termination analyzer for ABS. In: Kiselyov,O., Thompson, S., (eds.) Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, 23–24 January 2012, Philadelphia, Pennsylvania, USA, pp. 151–154. ACM Press (2012)

    Google Scholar 

  2. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Cost relation systems: a language-independent target language for cost analysis. In: Spanish Conference on Programming and Computer Languages (PROLE 2008). Electronic Notes in Theoretical Computer Science, vol. 248, pp. 31–46. Elsevier (2009)

    Google Scholar 

  3. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46(2), 161–203 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  4. Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D., COSTA: a cost and termination analyzer for Java Bytecode. In: Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode). Electronic Notes in Theoretical Computer Science, Budapest, Hungary. Elsevier, April 2008

    Google Scholar 

  5. Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper, lower bounds. ACM Trans. Comput. Logic 14(3), 1–35 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  6. Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_8

    Chapter  Google Scholar 

  7. Alonso-Blas, D.E., Arenas, P., Genaim, S.: Precise cost analysis via local reasoning. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 319–333. Springer, Heidelberg (2013). doi:10.1007/978-3-319-02444-8_23

    Chapter  Google Scholar 

  8. Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 405–421. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33125-1_27

    Chapter  Google Scholar 

  9. Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 140–155. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_10

    Chapter  Google Scholar 

  10. Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 467–478. ACM, New York (2015)

    Google Scholar 

  11. Debray, S.K., Lin, N.W.: Cost analysis of logic programs. ACM Trans. Program. Lang. Syst. 15(5), 826–875 (1993)

    Article  Google Scholar 

  12. Debray, S.K., López-García, P., Hermenegildo, M., Lin, N.-W.: Lower bound cost estimation for logic programs. In: 1997 International Logic Programming Symposium, pp. 291–305. MIT Press, Cambridge, October 1997

    Google Scholar 

  13. Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schauß, M. (ed.) RTA 2011. Leibniz International Proceedings in Informatics (LIPIcs), vol. 10, pp. 41–50. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2011)

    Google Scholar 

  14. Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. Technical report, Technische Universität Darmstadt, September 2016. http://www.informatik.tu-darmstadt.de/fileadmin/user_upload/Group_SE/Publications/FM2016_extended.pdf

  15. Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275–295. Springer, Heidelberg (2014). doi:10.1007/978-3-319-12736-1_15

    Google Scholar 

  16. Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 550–567. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40229-1_37

    Chapter  Google Scholar 

  17. Garcia, A., Laneve, C., Lienhardt, M.: Static analysis of cloud elasticity. In: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 14–16 July 2015, Siena, Italy, pp. 125–136. ACM (2015)

    Google Scholar 

  18. Grech, N., Georgiou, K., Pallister, J., Kerrison, S., Morse, J., Eder, K.: Static analysis of energy consumption for LLVM IR programs. In Proceedings of the 18th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2015, pp. 12–21. ACM, New York (2015)

    Google Scholar 

  19. Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI (2009)

    Google Scholar 

  20. Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127–139. ACM, New York (2009)

    Google Scholar 

  21. Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI 2010, pp. 292–304. ACM, New York (2010)

    Google Scholar 

  22. Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. SIGPLAN Not. 46(1), 357–370 (2011)

    Article  MATH  Google Scholar 

  23. Hoffmann, J., Shao, Z.: Type-based amortized resource analysis with integers and arrays. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 152–168. Springer, Heidelberg (2014). doi:10.1007/978-3-319-07151-0_10

    Chapter  Google Scholar 

  24. Serrano, A., López-García, P., Hermenegildo, M.V.: Resource usage analysis of logic programs via abstract interpretation using sized types. TPLP 14(4–5), 739–754 (2014)

    MATH  Google Scholar 

  25. Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745–761. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_50

    Google Scholar 

  26. Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. In: Formal Methods in Computer-Aided Design, FMCAD 2015, 27–30 September 2015, Austin, Texas, USA, pp. 144–151 (2015)

    Google Scholar 

  27. Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  28. Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23702-7_22

    Chapter  Google Scholar 

Download references

Acknowledgements

Research partly funded by the EU project FP7-610582 ENVISAGE: Engineering Virtualized Services. I thank the anonymous reviewers, R. Hähnle, F. Zuleger, M. Sinn and S. Genaim for their careful reading.

Author information

Authors and Affiliations

  1. Department of Computer Science, TU Darmstadt, Darmstadt, Germany

    Antonio Flores-Montoya

Authors
  1. Antonio Flores-Montoya
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Antonio Flores-Montoya .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Flores-Montoya, A. (2016). Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation