Elvira Albert
Miguel Gomez-Zamalloa
ABSTRACT
This article presents a heap space analysis for (sequential) Java bytecode. The analysis generates heap space cost relations which define at compile-time the heap consumption of a program as a function of its data size. These relations can be used to obtain upper bounds on the heap space located during the execution of the different methods. In addition, we describe how to refine the cost relations, by relying on escape analysis, in order to take into account the heap space that can be safely deallocated by the garbage collector upon exit from a corresponding method. These refined cost relations are then used to infer upper bounds on the active heap space upon methods return. Example applications for the analysis consider inference of constant heap usage and heap usage proportional to the data size (including polynomial and exponential heap consumption). Our prototype implementation is reported and demonstrated by means of a series of examples which illustrate how the analysis naturally encompasses standard data-structures like lists, trees and arrays with several dimensions written in object-oriented programming style.
- E. Albert, P. Arenas, S. Genaim, and G. Puebla. Automatic Inference of Upper Bounds for Cost Equation Systems. Submitted, 2007.Google Scholar
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of java bytecode. In 16th European Symposium on Programming, ESOP'07, Lecture Notes in Computer Science. Springer, March 2007. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Experiments in Cost Analysis of Java Bytecode. In Proc. of BYTECODE'07, Electronic Notes in Theoretical Computer Science. Elsevier -- North Holland, March 2007. Google ScholarDigital Library
- E. Albert, G. Puebla, and M. Hermenegildo. Abstraction--Carrying Code. In Proc. of LPAR'04, number 3452 in LNAI, pages 380--397. Springer--Verlag, 2005.Google Scholar
- D. Aspinall, S. Gilmore, M. Hofmann, D. Sannella, and I. Stark. Mobile Resource Guarantees for Smart Devices. In CASSIS'04, number 33--62 in LNCS. Springer, 2005. Google ScholarDigital Library
- Gilles Barthe, Mariela Pavlova, and Gerardo Schneider. Precise analysis of memory consumption using program logics. In Bernhard K. Aichernig and Bernhard Beckert, editors, SEFM, pages 8695. IEEE Computer Society, 2005. Google ScholarDigital Library
- L. Beringer, M. Hofmann, A. Momigliano, and O. Shkaravska. Automatic Certification of Heap Consumption. In Proc. of LPAR'04, LNCS 3452, pages 347--362. Springer, 2004.Google Scholar
- Bruno Blanchet. Escape Analysis for Javatm : Theory and practice. ACM Trans. Program. Lang. Syst., 25(6):713--775, 2003. Google ScholarDigital Library
- Victor Braberman, Diego Garbervetsky, and Sergio Yovine. A static analysis for synthesizing parametric specifications of dynamic memory consumption. Journal of Object Technology, 5(5):31--58, 2006.Google ScholarCross Ref
- F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. Lopez-- Garcia, and G. Puebla (Eds.). The Ciao System. Ref. Manual (v1.13). Technical report, C. S. School (UPM), 2006. Available at http://www.ciaohome.org.Google Scholar
- D. Cachera, D. Pichardie T. Jensen, and G. Schneider. Certified memory usage analysis. In FM'05, number 3582 in LNCS. Springer, 2005. Google ScholarDigital Library
- A. Chander, D. Espinosa, N. Islam, P. Lee, and G. Necula. Enforcing resource bounds via static verification of dynamic checks. In Proc. of ESOP'05, volume 3444 of Lecture Notes in Computer Science, pages 311--325. Springer, 2005. Google ScholarDigital Library
- W. Chin, H. Nguyen, S. Qin, and M. Rinard. Memory Usage Verification for OO Programs. In Proc. of SAS'05, LNCS 3672, pages 70--86. Springer, 2005. Google ScholarDigital Library
- K. Crary and S. Weirich. Resource bound certification. In Proc. of POPL'00, pages 184198. ACM Press, 2000. Google ScholarDigital Library
- Patricia M. Hill and Fausto Spoto. Deriving Escape Analysis by Abstract Interpretation. Higher--Order and Symbolic Computation, (19):415--463, 2006. Google ScholarDigital Library
- M. Hofmann. Certification of Memory Usage. In Theoretical Computer Science, 8th Italian Conference, ICTCS, volume 2841 of Lecture Notes in Computer Science, page 21. Springer, 2003.Google Scholar
- M. Hofmann and S. Jost. Static prediction of heap space usage for first--order functional programs. In 30th ACM Symposium on Principles of Programming Languages (POPL), pages 185--197. ACM Press, 2003. Google ScholarDigital Library
- M. Hofmann and S. Jost. Type--Based Amortised Heap--Space Analysis. In 15th European Symposium on Programming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 22--37. Springer, 2006. Google ScholarDigital Library
- J. Hughes and L. Pareto. Recursion and Dynamic Data--structures in Bounded Space: Towards Embedded ML Programming. In Proc. of ICFP'99, pages 7081. ACM Press, 1999. Google ScholarDigital Library
- T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison--Wesley, 1996. Google ScholarDigital Library
- Patricia M. Hill, Etienne Payet, and Fausto Spoto. Path--length analysis of object--oriented programs. In Proc. EAAI, 2006.Google Scholar
- G. Necula. Proof--Carrying Code. In POPL'97. ACM Press, 1997. Google ScholarDigital Library
- S. Rossignoli and F. Spoto. Detecting Non--Cyclicity by Abstract Compilation into Boolean Functions. In E. A. Emerson and K. S. Namjoshi, editors, Proc. of the 7th workshop on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 95--110, Charleston, SC, USA, January 2006. Springer--Verlag. Google ScholarDigital Library
- L. Unnikrishnan, S. Stoller, and Y. Liu. Optimized Live Heap Bound Analysis. In Proc. of VMCAI'03, Lecture Notes in Computer Science, pages 70--85. Springer, 2003. Google ScholarDigital Library
- P. Vasconcelos and K. Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher--Order Functional Programs. In IFL, volume 3145 of LNCS. Springer, 2003. Google ScholarDigital Library
Index Terms
- Heap space analysis for java bytecode
Recommendations
Heap profiling for space-efficient Java
We present a heap-profiling tool for exploring the potential for space savings in Java programs. The output of the tool is used to direct rewriting of application source code in a way that allows more timely garbage collection (GC) of objects, thus ...
Live heap space analysis for languages with garbage collection
ISMM '09: Proceedings of the 2009 international symposium on Memory managementThe peak heap consumption of a program is the maximum size of the live data on the heap during the execution of the program, i.e., the minimum amount of heap space needed to run the program without exhausting the memory. It is well-known that garbage ...
Parametric inference of memory requirements for garbage collected languages
ISMM '10: Proceedings of the 2010 international symposium on Memory managementThe accurate prediction of program's memory requirements is a critical component in software development. Existing heap space analyses either do not take deallocation into account or adopt specific models of garbage collectors which do not necessarily ...
Comments