Heap space analysis for java bytecode

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.

REFERENCES

• 1: E. Albert, P. Arenas, S. Genaim, and G. Puebla. Automatic Inference of Upper Bounds for Cost Equation Systems. Submitted, 2007.
• 2: 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.
• 3: E. Albert , P. Arenas , S. Genaim , G. Puebla , D. Zanardini, Experiments in Cost Analysis of Java Bytecode, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.1, p.67-83, July, 2007 [doi>10.1016/j.entcs.2007.02.061]
• 4: 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.
• 5: 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.
• 6: Gilles Barthe , Mariela Pavlova , Gerardo Schneider, Precise Analysis of Memory Consumption using Program Logics, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.86-95, September 07-09, 2005 [doi>10.1109/SEFM.2005.34]
• 7: 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.
• 8: Bruno Blanchet, Escape analysis for Java^TM: Theory and practice, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.6, p.713-775, November 2003 [doi>10.1145/945885.945886]
• 9: 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.
• 10: 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.
• 11: D. Cachera, D. Pichardie T. Jensen, and G. Schneider. Certified memory usage analysis. In FM'05, number 3582 in LNCS. Springer, 2005.
• 12: 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.
• 13: 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.
• 14: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 15: Patricia M. Hill , Fausto Spoto, Deriving escape analysis by abstract interpretation, Higher-Order and Symbolic Computation, v.19 n.4, p.415-463, December 2006 [doi>10.1007/s10990-006-0481-5]
• 16: 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.
• 17: Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.185-197, January 15-17, 2003, New Orleans, Louisiana, USA
• 18: 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.
• 19: John Hughes , Lars Pareto, Recursion and dynamic data-structures in bounded space: towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.70-81, September 27-29, 1999, Paris, France
• 20: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 21: Patricia M. Hill, Etienne Payet, and Fausto Spoto. Path--length analysis of object--oriented programs. In Proc. EAAI, 2006.
• 22: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 23: 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.
• 24: Leena Unnikrishnan , Scott D. Stoller , Yanhong A. Liu, Optimized Live Heap Bound Analysis, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.70-85, January 09-11, 2002
• 25: P. Vasconcelos and K. Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher--Order Functional Programs. In IFL, volume 3145 of LNCS. Springer, 2003.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.0 General

General Terms:
Languages, Reliability, Theory

Keywords:
Java bytecode, heap consumption, heap space analysis, low-level languages