Abstract
One of the main features of programs is the amount of resources which are needed in order to run them. Different resources can be taken into consideration, such as the number of execution steps, amount of memory allocated, number of calls to certain methods, etc. Unfortunately, manually determining the resource consumption of programs is difficult and error-prone. We provide an overview of a state of the art framework for automatically obtaining both upper and lower bounds on the resource consumption of programs. The bounds obtained are functions on the size of the input arguments to the program and are obtained statically, i.e., without running the program. Due to the approximations introduced, the framework can fail to obtain (non-trivial) bounds even if they exist. On the other hand, modulo implementation bugs, the bounds thus obtained are valid for any execution of the program. The framework has been implemented in the COSTA system and can provide useful bounds for realistic object-oriented and actor-based concurrent programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley (1974)
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers – Principles, Techniques and Tools. Addison-Wesley (1986)
Albert, E., Alonso, D., Arenas, P., Genaim, S., Puebla, G.: Asymptotic Resource Usage Bounds. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 294–310. Springer, Heidelberg (2009)
Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G.: Cost Analysis of Concurrent OO Programs. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 238–254. Springer, Heidelberg (2011)
Albert, E., Arenas, P., Genaim, S., Herraiz, I., Puebla, G.: Comparing Cost Functions in Resource Analysis. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 1–17. Springer, Heidelberg (2010)
Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008)
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)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Removing Useless Variables in Cost Analysis of Java Bytecode. In: ACM Symposium on Applied Computing (SAC) - Software Verification Track (SV 2008), Fortaleza, Brasil, pp. 368–375. ACM Press, New York (2008)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science 413(1), 142–159 (2012)
Albert, E., Arenas, P., Genaim, S., Zanardini, D.: Task-Level Analysis for a Language with Async-Finish parallelism. In: Vitek, J., De Sutter, B. (eds.) Proceedings of the ACM SIGPLAN/SIGBED 2011 Conference on Languages, Compilers, and Tools for Embedded Systems, LCTES 2011, Chicago, IL, USA, April 11-14, pp. 21–30. ACM (2011)
Albert, E., Bubel, R., Genaim, S., Hähnle, R., Román-Díez, G.: Verified Resource Guarantees for Heap Manipulating Programs. In: Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering, FASE 2012, Tallinn, Estonia. Springer, Heidelberg (to appear, 2012)
Albert, E., Correas, J., Puebla, G., Román-Díez, G.: Incremental Resource Usage Analysis. In: Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23-24. ACM Press (to appear, 2012)
Albert, E., Genaim, S., Gómez-Zamalloa, M.: Heap Space Analysis of Java Bytecode. In: 6th International Symposium on Memory Management (ISMM 2007), pp. 105–116. ACM Press (2007)
Albert, E., Genaim, S., Gómez-Zamalloa, M.: Parametric Inference of Memory Requirements for Garbage Collected Languages. In: 9th International Symposium on Memory Management (ISMM 2010), pp. 121–130. ACM Press, New York (2010)
Albert, E., Genaim, S., Masud, A.N.: More Precise Yet Widely Applicable Cost Analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 38–53. Springer, Heidelberg (2011)
Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G.: COSTABS: A Cost and Termination Analyzer for ABS. In: Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23-24, ACM Press (to appear, 2012)
Albert, E., Bubel, R., Genaim, S., Hähnle, R., Puebla, G., Román-Díez, G.: Verified resource guarantees using costa and key. In: Khoo, S.-C., Siek, J.G. (eds.) PEPM, pp. 73–76. ACM (2011)
Braberman, V., Fernández, F., Garbervetsky, D., Yovine, S.: Parametric Prediction of Heap Memory Requirements. In: ISMM. ACM Press (2008)
Chin, W.-N., Nguyen, H.H., Popeea, C., Qin, S.: Analysing Memory Resource Bounds for Low-Level Programs. In: ISMM. ACM Press (2008)
Debray, S.K., Lin, N.W.: Cost Analysis of Logic Programs. ACM Transactions on Programming Languages and Systems 15(5), 826–875 (1993)
Debray, S.K., Lin, N.W.: Cost analysis of logic programs. ACM TOPLAS 15(5), 826–875 (1993)
Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: The 36th Symposium on Principles of Programming Languages (POPL 2009), pp. 127–139. ACM (2009)
Hoffmann, J., Hofmann, M.: Amortized Resource Analysis with Polynomial Potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287–306. Springer, Heidelberg (2010)
Hofmann, M., Hoffmann, J., Aehlig, K.: Multivariate Amortized Resource Analysis. In: The 38th Symposium on Principles of Programming Languages (POPL 2011), pp. 357–370. ACM (2011)
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A Core Language for Abstract Behavioral Specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)
Lee, J.K., Palsberg, J.: Featherweight X10: A Core Calculus for Async-Finish Parallelism. In: Principles and Practice of Parallel Programming (PPoPP 2010), pp. 25–36. ACM, New York (2010)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley (1996)
Necula, G.: Proof-Carrying Code. In: ACM Symposium on Principles of programming languages (POPL 1997). ACM Press (1997)
Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Ramírez-Deantes, D., Correas, J., Puebla, G.: Modular Termination Analysis of Java Bytecode and Its Application to phoneME Core Libraries. In: Barbosa, L.S. (ed.) FACS 2010. LNCS, vol. 6921, pp. 218–236. Springer, Heidelberg (2010)
Sands, D.: Complexity Analysis for a Lazy Higher-Order Language. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol. 432, pp. 361–376. Springer, Heidelberg (1990)
Sands, D.: A Naïve Time Analysis and its Theory of Cost Equivalence. Journal of Logic and Computation 5(4) (1995)
Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing Active Objects to Concurrent Components. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275–299. Springer, Heidelberg (2010)
Srinivasan, S., Mycroft, A.: Kilim: Isolation-Typed Actors for Java. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 104–128. Springer, Heidelberg (2008)
Unnikrishnan, L., Stoller, S.D., Liu, Y.A.: Optimized Live Heap Bound Analysis. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 70–85. Springer, Heidelberg (2002)
Wegbreit, B.: Mechanical Program Analysis. Communications of the ACM 18(9) (1975)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G. (2012). Automatic Inference of Resource Consumption Bounds. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-28717-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28716-9
Online ISBN: 978-3-642-28717-6
eBook Packages: Computer ScienceComputer Science (R0)