×

zbMATH — the first resource for mathematics

Closed-form upper bounds in static cost analysis. (English) Zbl 1213.68200
Summary: The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, the analysis first produces cost relations (CRs), i.e., recursive equations which capture the cost of the program in terms of the size of its input data. Second, CRs are converted into closed form, i.e., without recurrences. Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has been comparatively less studied. This article presents, to our knowledge, the first practical framework for the generation of closed-form upper bounds for CRs which (1) is fully automatic, (2) can handle the distinctive features of CRs, originating from cost analysis of realistic programming languages, (3) is not restricted to simple complexity classes, and (4) produces reasonably accurate solutions. A key idea in our approach is to view CRs as programs, which allows applying semantic-based static analyses and transformations to bound them, namely our method is based on the inference of ranking functions and loop invariants and on the use of partial evaluation.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N01 General topics in the theory of software
Software:
ACE; Ciao; CiaoPP; COSTA; PPL; PURRS; Refal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974) · Zbl 0326.68005
[2] Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java bytecode. In: 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS’08). Lecture Notes in Computer Science, vol. 5051, pp. 2–18. Springer, Heidelberg (2008)
[3] Albert, E., Arenas, P., Genaim, S., Herraiz, I., Puebla, G.: Comparing cost functions in resource analysis. In: 1st International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA’09). Lecture Notes in Computer Science. Springer, Heidelberg (2009)
[4] Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: 15th International Symposium on Static Analysis (SAS’08). Lecture Notes in Computer Science, vol. 5079, pp. 221–237 (2008) · Zbl 1149.68345
[5] Albert, E., Arenas, P., Genaim, S., Puebla, G.: Cost relation systems: a language–independent target language for cost analysis. In: 8th Spanish Conference on Programming and Computer Languages (PROLE’08), vol. 17615 of Electronic Notes in Theoretical Computer Science. Elsevier (2008) · Zbl 1149.68345
[6] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: 16th European Symposium on Programming, (ESOP’07). Lecture Notes in Computer Science, vol. 4421, pp. 157–172. Springer (2007) · Zbl 1236.68042
[7] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for Java bytecode. In: 6th International Symposioum on Formal Methods for Components and Objects (FMCO’08). Lecture Notes in Computer Science, no. 5382, pp. 113–133. Springer (2007)
[8] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Experiments in cost analysis of Java bytecode. In 2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE’07), vol. 190, Issue 1 of Electronic Notes in Theoretical Computer Science. Elsevier (2007) · Zbl 1236.68042
[9] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Resource usage analysis and its application to resource certification. In: 9th International School on Foundations of Security Analysis and Design (FOSAD’09). Lecture Notes in Computer Science, no. 5705, pp. 258–288. Springer (2009)
[10] Albert, E., Genaim, S., Gómez-Zamalloa, M.: Heap space analysis of Java bytecode. In: 6th International Symposium on Memory Management (ISMM’07), pp. 105–116. ACM Press (2007)
[11] Albert, E., Genaim, S., Gómez-Zamalloa, M.: Live Heap space analysis for languages with garbage collection. In: 8th International Symposium on Memory management (ISMM’09). ACM Press (2009)
[12] Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS’04). Lecture Notes in Computer Science, vol. 3362, pp. 1–27. Springer (2005)
[13] Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008) · Zbl 05312355 · doi:10.1016/j.scico.2007.08.001
[14] Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: towards computer algebra support for fully automatic worst-case complexity analysis. Technical report (2005). http://arXiv.org./abs/cs/0512056
[15] Batchelder, P.M.: An introduction to linear difference equations. Dover Publications (1967) · JFM 53.0430.10
[16] Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3), 31 (2008) (Article 16) · Zbl 05459426 · doi:10.1145/1353445.1353450
[17] Ben-Amram, A.M., Jones, N.D., Kristiansen L.: Linear, polynomial or exponential? Complexity inference in polynomial time. In: Logic and Theory of Algorithms, 4th Conference on Computability in Europe, (CiE’08). Lecture Notes in Computer Science, vol. 5028, pp. 67–76. Springer (2008) · Zbl 1142.68369
[18] Benzinger, R.: Automated higher-order complexity analysis. Theor. Comp. Sci. 318(1–2), 79–103 (2004) · Zbl 1071.68029 · doi:10.1016/j.tcs.2003.10.022
[19] Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: Quasi-interpretations and small space bounds. In: 16th International Conference on Rewriting Techniques and Applications (RTA’05). Lecture Notes in Computer Science, vol. 3467, pp. 150–164 (2005) · Zbl 1078.68041
[20] Braverman, M.: Termination of integer linear programs. In: 18th Computer Aided Verification (CAV’06). Lecture Notes in Computer Science, vol. 4144, pp. 372–385. Springer (2006) · Zbl 1188.68183
[21] Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.: Enforcing resource bounds via static verification of dynamic checks. In: 14th European Symposium on Programming (ESOP’05). Lecture Notes in Computer Science, vol. 3444, pp. 311–325. Springer (2005) · Zbl 1108.68419
[22] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages (POPL’77), pp. 238–252. ACM Press (1977)
[23] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM Symposium on Principles of Programming Languages (POPL’78), pp. 84–97. ACM Press (1978)
[24] Craig, S.-J., Leuschel, M.: Self-tuning resource aware specialisation for prolog. In: 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’05), pp. 23–34. ACM Press (2005)
[25] Crary, K., Weirich, S.: Resource bound certification. In: 27th ACM Symposium on Principles of Programming Languages (POPL’05), pp. 184–198. ACM Press (2000) · Zbl 1323.68368
[26] Debray, S.K., Lin, N.W.: Cost Analysis of Logic Programs. ACM Trans. Program. Lang. Syst. 15(5), 826–875 (1993) · doi:10.1145/161468.161472
[27] Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposium in Applied Mathematics, vol. 19, Mathematical Aspects of Computer Science, pp. 19–32. American Mathematical Society, Providence, RI (1967) · Zbl 0189.50204
[28] Gómez, G., Liu, Y.A.: Automatic time-bound analysis for a higher-order language. In: Proceedings of the ACM SIGPLAN 2002 Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pp. 75–88. ACM Press (2002)
[29] Hermenegildo, M., Puebla, G., Bueno, F., López-García, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and The Ciao System Preprocessor). Sci. Comput. Program. 58(1–2), 115–140 (2005) · Zbl 1076.68540 · doi:10.1016/j.scico.2005.02.006
[30] Hickey, T., Cohen, J.: Automating program analysis. J. ACM 35(1), 185–220 (1988) · Zbl 0632.68013 · doi:10.1145/42267.42275
[31] Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: 30th Symposium on Principles of Programming Languages (POPL’03), pp. 185–197. ACM Press, New York (2003) · Zbl 1321.68180
[32] Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Log. Program. 19/20, 503–581 (1994) · Zbl 00639141 · doi:10.1016/0743-1066(94)90033-7
[33] Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation. Prentice Hall, New York (1993) · Zbl 0875.68290
[34] Komorovski, J.: An introduction to partial deduction. In: Meta Programming in Logic (META’92). Lecture Notes in Computer Science, vol. 649, pp. 49–69. Springer, Heidelberg (1992)
[35] Kristiansen, L., Jones, N.D.: The flow of data and the complexity of algorithms. In: 1st Conference on Computability in Europe (CiE’05). Lecture Notes in Computer Science, vol. 3526, pp. 263–274 (2005) · Zbl 1115.68052
[36] Le Metayer, D.: ACE: an automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248–266 (1988) · doi:10.1145/42190.42347
[37] Leuschel, M.: A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 26(3), 413–463 (2004) · Zbl 05459298 · doi:10.1145/982158.982159
[38] Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: control issues. Theory Pract. Log. Program. 2(4 & 5), 461–515 (2002) · Zbl 1105.68331 · doi:10.1017/S147106840200145X
[39] Lloyd, J.W., Shepherdson, J.C.: Partial evaluation in logic programming. J. Log. Program. 11(3–4), 217–242 (1991) · Zbl 0741.68030 · doi:10.1016/0743-1066(91)90027-M
[40] Luca, B., Andrei, S., Anderson, H., Khoo, S.-C.: Program transformation by solving recurrences. In: ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM ’06), pp. 121–129. ACM (2006)
[41] Marion, J.-Y., Péchoux, R.: Sup-interpretations, a semantic method for static analysis of program resources. ACM Trans. Comput. Log. 10(4), 31 (2009) (Article 27) · Zbl 1351.68061 · doi:10.1145/1555746.1555751
[42] Navas, J., Mera, E., López-García, P., Hermenegildo, M.: User-definable resource bounds analysis for logic programs. In: 23rd International Conference on Logic Programming (ICLP’07), vol. 4670 of LNCS, pp. 348–363. Springer, Heidelberg (2007)
[43] Necula, G.: Proof-carrying code. In: ACM Symposium on Principles of Programming Languages (POPL 1997), pp. 106–119. ACM Press, New York (1997)
[44] Niggl, K.-H., Wunderlich, H.: Certifying polynomial time and linear/polynomial space for imperative programs. SIAM J. Comput. 35(5), 1122–1147 (2006) · Zbl 1100.68035 · doi:10.1137/S0097539704445597
[45] Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’04). Lecture Notes in Computer Science, pp. 239–251. Springer, Heidelberg (2004) · Zbl 1202.68109
[46] Puebla, G., Ochoa, C.: Poly-controlled partial evaluation. In: 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP’06), pp. 261–271. ACM Press, New York (2006)
[47] Rosendahl, M.: Automatic complexity analysis. In: 4th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA’89), pp. 144–156. ACM Press (1989)
[48] Rosendahl, M.: Simple driving techniques. In: Mogensen, T., Schmidt, D., Hal Sudborough, I. (eds.) The Essence of Computation. Lecture Notes in Computer Science, vol. 2566, pp. 404–419. Springer, Heidelberg (2002) · Zbl 1026.68512
[49] Sands, D.: A naïve time analysis and its theory of cost equivalence. J. Log. Comput. 5(4), 495–541 (1995) · Zbl 0942.68623 · doi:10.1093/logcom/5.4.495
[50] Shamir, A.: A linear time algorithm for finding minimum cutsets in reducible graphs. SIAM J. Comput. 8(4), 645–655 (1979) · Zbl 0422.05029 · doi:10.1137/0208051
[51] Spoto, F., Hill, P.M., Payet, E.: Path-length analysis of object-oriented programs. In: 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI’06), Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2006)
[52] Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. 8(3), 292–325 (1986) · Zbl 0598.68016 · doi:10.1145/5956.5957
[53] Wadler, P.: Strictness analysis aids time analysis. In: ACM Symposium on Principles of Programming Languages (POPL’88), pp. 119–132. ACM Press (1988)
[54] Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 69–73 (1975) · Zbl 0306.68008 · doi:10.1145/361002.361016
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.