zbMATH — the first resource for mathematics

Cost analysis of object-oriented bytecode programs. (English) Zbl 1236.68042
Summary: Cost analysis statically approximates the cost of programs in terms of their input data size. This paper presents, to the best of our knowledge, the first approach to the automatic cost analysis of object-oriented bytecode programs. In languages such as Java and C#, analyzing bytecode has a much wider application area than analyzing source code since the latter is often not available. Cost analysis in this context has to consider, among others, dynamic dispatch, jumps, the operand stack, and the heap. Our method takes a bytecode program and a cost model specifying the resource of interest, and generates cost relations which approximate the execution cost of the program with respect to such resource. We report on COSTA, an implementation for Java bytecode which can obtain upper bounds on cost for a large class of programs and complexity classes. Our basic techniques can be directly applied to infer cost relations for other object-oriented imperative languages, not necessarily in bytecode form.

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N99 Theory of software
Full Text: DOI
[1] Adachi, A.; Kasai, T.; Moriya, E., A theoretical study of the time analysis of programs, (), 201-207
[2] Aho, A.V.; Hopcroft, J.E.; Ullman, J.D., The design and analysis of computer algorithms, (1974), Addison-Wesley · Zbl 0207.01701
[3] Aho, A.V.; Sethi, R.; Ullman, J.D., Compilers – principles, techniques and tools, (1986), Addison-Wesley
[4] Albert, E.; Arenas, P.; Codish, M.; Genaim, S.; Puebla, G.; Zanardini, D., Termination analysis of Java bytecode, (), 2-18
[5] Albert, E.; Arenas, P.; Genaim, S.; Herraiz, I.; Puebla, G., Comparing cost functions in resource analysis, (), 1-17 · Zbl 1305.68051
[6] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G., Field-sensitive value analysis by field-insensitive analysis, (), 370-386
[7] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G., Closed-form upper bounds in static cost analysis, Journal of automated reasoning, 46, 2, 161-203, (2011) · Zbl 1213.68200
[8] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Ramírez, D., From object fields to local variables: a practical approach to field-sensitive analysis, (), 100-116 · Zbl 1306.68016
[9] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Zanardini, D., Cost analysis of Java bytecode, (), 157-172
[10] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Zanardini, D., Experiments in cost analysis of Java bytecode, Proc. of BYTECODE’07, Entcs, 190, 67-83, (2007)
[11] Albert, E.; Arenas, P.; Genaim, S.; Zanardini, D., Task-level analysis for a language with async-finish parallelism, (), 21-30
[12] Albert, E.; Genaim, S.; Gómez-Zamalloa, M., Heap space analysis for Java bytecode, (), 105-116
[13] Albert, E.; Genaim, S.; Gómez-Zamalloa, M., Parametric inference of memory requirements for garbage collected languages, (), 121-130
[14] Albert, E.; Genaim, S.; Masud, A.N., More precise yet widely applicable cost analysis, (), 38-53 · Zbl 1317.68027
[15] Aspinall, D.; Gilmore, S.; Hofmann, M.; Sannella, D.; Stark, I., Mobile resource guarantees for smart devices, (), 1-27
[16] 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, Science of computer programming, 72, 1-2, (2008)
[17] Ben-Amram, A.M.; Jones, N.D.; Kristiansen, L., Linear, polynomial or exponential? complexity inference in polynomial time, (), 67-76 · Zbl 1142.68369
[18] Benoy, F.; King, A., Inferring argument size relationships with CLP(R), (), 204-223
[19] Benzinger, R., Automated higher-order complexity analysis, Theoretical computer science, 318, 1-2, (2004)
[20] Blanchet, B., Escape analysis for object oriented languages. application to Java (TM), (), 20-34
[21] Braberman, V.; Fernández, F.; Garbervetsky, D.; Yovine, S., Parametric prediction of heap memory requirements, (), 141-150
[22] Brauer, J.; King, A., Automatic abstraction for intervals using Boolean formulae, (), 167-183 · Zbl 1306.68020
[23] Bruynooghe, M.; Codish, M.; Gallagher, J.P.; Genaim, S.; Vanhoof, W., Termination analysis of logic programs through combination of type-based norms, ACM transactions on programming languages and systems, 29, 2, (2007)
[24] Cachera, D.; Jensen, T.; Pichardie, D.; Schneider, G., Certified memory usage analysis, (), 91-106 · Zbl 1120.68385
[25] Cachera, D.; Jensen, T.P.; Jobin, A; Long-run, P., Cost analysis by approximation of linear operators over dioids, Mathematical structures in computer science, 20, 4, 589-624, (2010) · Zbl 1209.68124
[26] Chander, A.; Espinosa, D.; Islam, N.; Lee, P.; Necula, G., Enforcing resource bounds via static verification of dynamic checks, (), 311-325 · Zbl 1108.68419
[27] Chen, L.; Miné, A.; Cousot, P., A sound floating-point polyhedra abstract domain, (), 3-18
[28] Chin, W.-N.; Nguyen, H.H.; Popeea, C.; Qin, S., Analysing memory resource bounds for low-level programs, (), 151-160
[29] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (), 238-252
[30] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (), 84-97
[31] Craig, S.J.; Leuschel, M., Self-tuning resource aware specialisation for prolog, (), 23-34
[32] Crary, K.; Weirich, S., Resource bound certification, (), 184-198 · Zbl 1323.68368
[33] Debray, S.K.; Lin, N.W., Cost analysis of logic programs, ACM transactions on programming languages and systems, 15, 5, (1993)
[34] R. DeLine, K.R.M. Leino, BoogiePL: a typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, 2005.
[35] A. Ermedahl, J. Gustafsson, B. Lisper, Experiences from industrial wcet analysis case studies, in: Proc. of WCET’05, volume 1 of OASICS, 2005.
[36] S. Genaim, F. Spoto, Constancy analysis, in: 10th Workshop on Formal Techniques for Java-like Programs, 2008. · Zbl 1111.68505
[37] Goodrich, M.; Tamassia, R., Data structures and algorithms in Java, (2004), John Wiley · Zbl 1059.68022
[38] M.T. Goodrich, R. Tamassia, R. Zamore, The net.datastructures Package, version 3. Available at http://net3.datastructures.net, 2003.
[39] Gulavani, B. S.; Gulwani, S., A numerical abstract domain based on expression abstraction and MAX operator with application in timing analysis, (), 370-384 · Zbl 1155.68366
[40] Halbwachs, N.; Péron, M., Discovering properties about arrays in simple programs, (), 339-348
[41] Hermenegildo, M.; Albert, E.; López-García, P.; Puebla, G., Abstraction carrying code and resource-awareness, (), 1-11
[42] 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), Science of computer programming, 58, 1-2, (2005) · Zbl 1076.68540
[43] Hofmann, M.; Jost, S., Static prediction of heap space usage for first-order functional programs, (), 185-197 · Zbl 1321.68180
[44] Kristiansen, L.; Jones, N.D., The flow of data and the complexity of algorithms, (), 263-274 · Zbl 1115.68052
[45] Le Metayer, D., ACE: an automatic complexity evaluator, ACM transactions on programming languages and systems, 10, 2, (1988)
[46] J.-Y. Marion, R. Pèchoux, Resource control of object-oriented programs, in: Proc. of LICS affiliated Workshop LCC’07, 2007.
[47] Miné, A., Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, (), 54-63
[48] Navas, J.; Mera, E.; López-García, P.; Hermenegildo, M., User-definable resource bounds analysis for logic programs, (), 348-363
[49] Necula, G., Proof-carrying code, (), 106-119
[50] Nielson, F.; Nielson, H.R.; Hankin, C., Principles of program analysis, (2005), Springer · Zbl 1069.68534
[51] Niggl, K.-H.; Wunderlich, H., Certifying polynomial time and linear/polynomial space for imperative programs, SIAM journal on computing, 35, 5, (2006) · Zbl 1100.68035
[52] Puebla, G.; Ochoa, C., Poly-controlled partial evaluation, (), 261-271
[53] D. Ramírez, J. Correas, G. Puebla, Modular termination analysis of Java bytecode and its application to phoneme core libraries, in: Proc. of FACS’10, LNCS, vol. 6921, Springer, 2010 (in press).
[54] Rosendahl, M., Automatic complexity analysis, (), 144-156
[55] Rossignoli, S.; Spoto, F., Detecting non-cyclicity by abstract compilation into Boolean functions, (), 95-110 · Zbl 1176.68043
[56] Sands, D., A naïve time analysis and its theory of cost equivalence, Journal of logic and computation, 5, 4, (1995) · Zbl 0942.68623
[57] Secci, S.; Spoto, F., Pair-sharing analysis of object-oriented programs, (), 320-335 · Zbl 1141.68378
[58] F. Spoto, \scJulia: a generic static analyser for the java bytecode, in: Proc. of FTfJP’05, 2005.
[59] F. Spoto, P.M. Hill, E. Payet, Path-length analysis of object-oriented programs, in: Proc. of EAAI’06, 2006. Available at http://profs.sci.univr.it/ spoto/papers.html.
[60] Spoto, F.; Mesnard, F.; Payet, É, A termination analyser for Java bytecode based on path-length, Transactions on programming languages and systems, 32, 3, (2010)
[61] Vallee-Rai, R.; Hendren, L.; Sundaresan, V.; Lam, P.; Gagnon, E.; Co, P., Soot — a Java optimization framework, (), 125-135
[62] Wadler, P., Strictness analysis aids time analysis, (), 119-132
[63] Wegbreit, B., Mechanical program analysis, Communications of the ACM, 18, 9, (1975) · Zbl 0306.68008
[64] Wilhelm, R.; Engblom, J.; Ermedahl, A.; Holsti, N.; Thesing, S.; Whalley, D.; Bernat, G.; Ferdinand, C.; Heckmann, R.; Mitra, T.; Mueller, F.; Puaut, I.; Puschner, P.; Staschulat, J.; Stenström, P., The worst-case execution-time problem — overview of methods and survey of tools, ACM transactions on embedded computing systems, 7, 36, (2008)
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.