Memory consumption is a particularly interesting case of resource analysis which is challenging due to its non-accumulative nature during run-time: the amount of memory utilized by a program varies during time and does not necessarily increase monotonically. Thus, the problem of automatically inferring memory-usage expressions that approximate memory consumption requires not only computing bounds for memory allocations but it also needs to consider the memory that is reclaimed by a memory manager (e.g., a garbage collector).

JConsume 2.0 implements a new compositional quantitative analysis (following the approach presented in [1,2]) aimed at inferring non-linear uppers bounds on dynamic memory consumption in Java like programs. The analysis is based on the construction of memory consumption summaries for every method under analysis. A memory consumption summary is a parametric specification of the consumption of a method, describing an approximation of the amount of dynamic memory utilized by the method in terms of their parameters. The summaries are built up using the method local information (e.g. their own allocations) and the precomputed summaries of the method they call. Precise method summaries can then inferred automatically or manually using a local reasoning.

The analysis considers the fact that memory is reclaimed by a garbage collector. Summaries could be compartmentalized into groups of objects according to their expected lifetime. For instance, a summary may distinguish temporary or auxiliary objects whose lifetime is confined to that of the method from residual objects, that may live longer. This distinction allows client methods to make a fine-grained analysis of method invocations.

The design of the inference algorithm allows different helper analyses enabling the use of different mechanism for quantifying visits to statements and implementing the lifetime oracle (e.g., escape analyses). The current prototype implements a counting mechanism based on [3] and two different escape analysis: LTO-I based on [4] and LTO-II based on [5]. The symbolic operation support is implemented by using the barvinok symbolic calculator provided by [6].

References

  • [0] D. Garbervetsky, M. Rouaux, S. Yovine, V. Braberman. A compositional analysis of heap memory requirements Technical report, 2011.
  • [1] M. Rouaux. Parametric prediction fo dynamic memory requirements. Modular specification. Master thesis, 2009.
  • [2] M. Grunberg and G. Krasny. A compositional analysis for the inference of memory consumption summaries. Master thesis, 2010.
  • [3] V. Braberman, F. Fernández, D. Garbervetsky, and S. Yovine. Parametric prediction of heap memory requirements. In ISMM ’08, pages 141–150, 2008.
  • [4] G. Salagnac, C. Rippert, and S. Yovine. Semi-automatic region-based memory management for real-time java embedded systems. In RTCSA’07, pages 73–80, 2007.
  • [5] A. Salcianu and M. Rinard. Pointer and escape analysis for multi-threaded programs. In PPoPP 01, volume 36, pages 12–23, 2001.
  • [6] S. Verdoolaege.isl: An integer set library for the polyhedral model. In ICMS 2010, 2010.