×

Resource analysis driven by (conditional) termination proofs. (English) Zbl 1434.68101

Summary: When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named \(\mathsf {MaxCore}\), that is guided by the \(\mathsf {VeryMax}\) termination analyzer and uses \(\mathsf {CoFloCo}\) and \(\mathsf {PUBS}\) as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that \(\mathsf {MaxCore}\) outperforms all other resource analysis tools.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

AProVE
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Albert, E., Arenas, P., Genaim, S., and Puebla, G.2008. Automatic inference of upper bounds for recurrence relations in cost analysis. In Proc. of SAS 2008. LNCS, vol. 5079. Springer, 221-237. · Zbl 1149.68345
[2] Albert, E., Arenas, P., Genaim, S., Puebla, G., and Zanardini, D.2007. Cost Analysis of Java Bytecode. In Proc. of ESOP’07. LNCS, vol. 4421. Springer, 157-172. · Zbl 1236.68042
[3] Albert, E., Correas, J., Ka I Pun, E. B. J., and Román-Díez, G.2018. Parallel Cost Analysis. ACM Trans. Comput. Log. 19,4, 1-37. · Zbl 1407.68062
[4] Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., and Rubio, A.2017. Proving termination through conditional termination. In Proc. TACAS 2017. LNCS, vol. 10205. Springer, 99-117. · Zbl 1452.68046
[5] Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., and Giesl, J.2016. Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38, 4, 13:1-13:50.
[6] Cousot, P. and Halbwachs, N.1978. Automatic discovery of linear restraints among variables of a program. In Proc. POPL 1978. ACM, 84-96.
[7] Debray, S. K. and Lin, N.1993. Cost analysis of logic programs. ACM Trans. Program. Lang. Syst. 15,5, 826-875.
[8] Debray, S. K., López-Garca, P., Hermenegildo, M. V., and Lin, N.1994. Estimating the computational cost of logic programs. In Proc. SAS 1994. LNCS, vol. 864. Springer, 255-265.
[9] Flores-Montoya, A.2017. Cost analysis of programs based on the refinement of cost relations. Ph.D. thesis, Darmstadt University of Technology, Germany.
[10] Flores-Montoya, A. and Hähnle, R.2014. Resource analysis of complex programs with cost equations. In Proc. APLAS 2014. LNCS, vol. 8858. Springer, 275-295. · Zbl 1453.68047
[11] Garcia, A., Laneve, C., and Lienhardt, M.2015. Static analysis of cloud elasticity. In Proc. PPDP 2015. ACM, 125-136.
[12] Giesl, J., Thiemann, R., Schneider-Kamp, P., and Falke, S.2004. Automated termination proofs with aprove. In Proc. RTA 2004. LNCS, vol. 3091. Springer, Aachen, Germany, 210-220.
[13] Grech, N., Georgiou, K., Pallister, J., Kerrison, S., Morse, J., and Eder, K.2015. Static analysis of energy consumption for LLVM IR programs. In Proc. SCOPES 2015. ACM, 12-21.
[14] Gulwani, S., Jain, S., and Koskinen, E.2009. Control-flow refinement and progress invariants for bound analysis. In Proc. of PLDI 2009. ACM, 375-385.
[15] Kafle, B., Gallagher, J. P., Gange, G., Schachte, P., Søndergaard, H., and Stuckey, P. J.2018. An iterative approach to precondition inference using constrained horn clauses. Theory Pract. Log. Program. 18,3-4, 553-570. · Zbl 1451.68075
[16] Liqat, U., Georgiou, K., Kerrison, S., López-Garca, P., Gallagher, J. P., Hermenegildo, M. V., and Eder, K.2015. Inferring parametric energy consumption functions at different software levels: ISA vs. LLVM IR. In Proc. FOPARA 2015, Selected Papers. LNCS, vol. 9964. Springer, 81-100.
[17] Navas, J. A., Mera, E., López-Garca, P., and Hermenegildo, M. V.2007. User-definable resource bounds analysis for logic programs. In Proc. ICLP 2007. LNCS, vol. 4670. Springer, 348-363.
[18] Serrano, A., López-Garca, P., Bueno, F., and Hermenegildo, M. V.2013. Sized type analysis for logic programs. Theory Pract. Log. Program. 13, 4-5-Online-Supplement.
[19] Sharma, R., Dillig, I., Dillig, T., and Aiken, A.2011. Simplifying loop invariant generation using splitter predicates. In Proc. of CAV 2011. Springer, 703-719.
[20] Sinn, M., Zuleger, F., and Veith, H.2014. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proc. CAV 2014. LNCS, vol. 8559. Springer, 745-761.
[21] Spoto, F., Mesnard, F., and Payet, É.2010. A termination analyzer for java bytecode based on path-length. ACM Trans. Program. Lang. Syst. 32, 3, 8:1-8:70.
[22] Wegbreit, B.1975. Mechanical Program Analysis. Communications ACM 18, 9, 528-539. · Zbl 0306.68008
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.