nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

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

verfasst von : Antonio Flores-Montoya

Erschienen in: FM 2016: Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Recovering High-Level Conditions from Binary Programs

Nächstes Kapitel Exploring Model Quality for ACAS X

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

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

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).

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 \).

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

\( 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.

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)

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)

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

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

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)MathSciNetCrossRefMATH

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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)

11.

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

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

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)

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

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 CrossRef

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)

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)

19.

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

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)

21.

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

22.

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

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 CrossRef

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

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

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)

27.

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

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 CrossRef

Titel: Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
verfasst von: Antonio Flores-Montoya
Verlag: Springer International Publishing
Buch: FM 2016: Formal Methods
Print ISBN: 978-3-319-48988-9

Electronic ISBN: 978-3-319-48989-6

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-48989-6_16

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"