Parametric heap usage analysis for functional programs

ABSTRACT

This paper presents an analysis that derives a formula describing the worst-case live heap space usage of programs in a functional language with automated memory management (garbage collection). First, the given program is automatically transformed into bound functions that describe upper bounds on the live heap space usage and other related space metrics in terms of the sizes of function arguments. The bound functions are simplified and rewritten to obtain recurrences, which are then solved to obtain the desired formulas characterizing the worst-case space usage. These recurrences may be difficult to solve due to uses of the maximum operator. We give methods to automatically solve categories of such recurrences. Our analysis determines and exploits monotonicity and monotonicity-like properties of bound functions to derive upper bounds on heap usage, without considering behaviors of the program that cannot lead to maximal space usage.

REFERENCES

• 1: Elvira Albert , Puri Arenas , Samir Genaim , Germán Puebla, Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis, Proceedings of the 15th international symposium on Static Analysis, July 16-18, 2008, Valencia, Spain [doi>10.1007/978-3-540-69166-2_15]
• 2: Elvira Albert , Samir Genaim , Miguel Gomez-Zamalloa, Heap space analysis for java bytecode, Proceedings of the 6th international symposium on Memory management, October 21-22, 2007, Montreal, Quebec, Canada [doi>10.1145/1296907.1296922]
• 3: Elvira Albert , Samir Genaim , Miguel Gómez-Zamalloa Gil, Live heap space analysis for languages with garbage collection, Proceedings of the 2009 international symposium on Memory management, June 19-20, 2009, Dublin, Ireland [doi>10.1145/1542431.1542450]
• 4: D. Aspinall, S. Gilmore, M. Hofmann, D. Sannella, and I. Stark. Mobile resource guarantees for smart devices. In Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), volume 3362 of LNCS, pages 1--26. Springer, 2005.
• 5: David F. Bacon, Realtime Garbage Collection, Queue, v.5 n.1, February 2007 [doi>10.1145/1217256.1217268]
• 6: R. Bagnara, A. Pescetti, A. Zaccagnini, E. Zaffanella, and T. Zolo. PURRS: The Parma University's recurrence relation solver. http: //www.cs.unipr.it/purrs.
• 7: 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]
• 8: Víctor Braberman , Federico Fernández , Diego Garbervetsky , Sergio Yovine, Parametric prediction of heap memory requirements, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA [doi>10.1145/1375634.1375655]
• 9: D. Cachera, T. Jensen, D. Pichardie, and G. Schneider. Certified memory usage analysis. In Formal Methods 05, volume 3582 of LNCS, pages 91--106. Springer-Verlag, 2005.
• 10: Wei-Ngan Chin , Huu Hai Nguyen , Corneliu Popeea , Shengchao Qin, Analysing memory resource bounds for low-level programs, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA [doi>10.1145/1375634.1375656]
• 11: W.-N. Chin, H. H. Nguyen, S. Qin, and M. Rinard. Memory usage verification for oo programs. In SAS 05, pages 70--86. Springer, 2005.
• 12: 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]
• 13: Wei Fu , Carl Hauser, A real-time garbage collection framework for embedded systems, Proceedings of the 2005 workshop on Software and compilers for embedded systems, p.20-26, September 29-October 01, 2005, Dallas, Texas [doi>10.1145/1140389.1140392]
• 14: Somnath Ghosh , Margaret Martonosi , Sharad Malik, Cache miss equations: a compiler framework for analyzing and tuning memory behavior, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.703-746, July 1999 [doi>10.1145/325478.325479]
• 15: Sumit Gulwani , Krishna K. Mehra , Trishul Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 16: 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
• 17: 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
• 18: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 19: Daniel Le Métayer, ACE: an automatic complexity evaluator, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.248-266, April 1988 [doi>10.1145/42190.42347]
• 20: Yanhong A. Liu , Gustavo Gomez, Automatic Accurate Time-Bound Analysis for High-Level Languages, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.31-40, June 01, 1998
• 21: M. B. Monagan, K. O. Geddes, K. M. Heal, G. Labahn, S. M. Vorkoetter, J. McCarron, and P. DeMarco. Maple 10 Programming Guide. Maplesoft, 2005.
• 22: Mads Rosendahl, Automatic complexity analysis, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.144-156, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99381]
• 23: David Sands, Complexity Analysis for a Lazy Higher-Order Language, Proceedings of the 3rd European Symposium on Programming, p.361-376, May 15-18, 1990
• 24: L. Unnikrishnan. Automatic Live Memory Bound Analysis for High-Level Languages. PhD thesis, Stony Brook University, 2008. Available at http://www.cs.sunysb.edu/~leena/thesis.pdf.
• 25: 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
• 26: Ben Wegbreit, Mechanical program analysis, Communications of the ACM, v.18 n.9, p.528-539, Sept. 1975 [doi>10.1145/361002.361016]
• 27: Christian Ferdinand , Reinhard Wilhelm, On Predicting Data Cache Behavior for Real-Time Systems, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.16-30, June 01, 1998

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

General Terms:
Languages, Performance, Verification

Keywords:
functional languages, garbage collection, live heap space analysis, recurrence relations