A direct approach to control-flow sensitive region-based memory management

ABSTRACT

Region-based memory management can be used to control dynamic memory allocations and deallocations safely and efficiently. Existing (direct-style) region systems that statically guarantee region safety---no dereferencing of dangling pointers---are based on refinements of Tofte and Talpin's seminal work on region inference for managing heap memory in stacks of regions.We present a unified Floyd-Hoare Logic inspired region type system for reasoning about and inferring region-based memory management, using a sublanguage of imperative region commands. Our system expresses and performs control-sensitive region management without requiring a stack discipline for allocating and deallocating regions. Furthermore, it captures storage mode analysis and late allocation/early deallocation analysis in a single, expressive, unified logical framework. Explicit region aliasing in combination with reference-counted regions provides flexible, context-sensitive early memory deallocation and simultaneously dispenses with the need for an integrated region alias analysis.In this paper we present the design of our region type system, illustrate its practical expressiveness, compare it to existing region analyses, demonstrate how this eliminates the need for previously required source code rewritings for good memory performance, and describe automatic inference of region commands that give consistently better (or at least equally good) memory performance as existing inference techniques.

REFERENCES

• 1: Alexander Aiken , Manuel Fähndrich , Raph Levien, Better static memory management: improving region-based analysis of higher-order languages, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.174-185, June 18-21, 1995, La Jolla, California, United States
• 2: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• 3: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 4: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 5: D. R. Hanson, Fast allocation and deallocation of memory based on object lifetimes, Software—Practice & Experience, v.20 n.1, p.5-12, January 1990 [doi>10.1002/spe.4380200104]
• 6: F. Henglein, H. Makholm, and H. Niss. A direct approach to control-flow sensitive region-based memory management. Technical report, 2001. hhttp://www.diku.dk/~hniss/rbmm/ppdp-ext.ps.gzi.
• 7: 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
• 8: Douglas T. Ross, The AED free storage package, Communications of the ACM, v.10 n.8, p.481-492, Aug. 1967 [doi>10.1145/363534.363546]
• 9: J. T. Schwartz. Optimization of very high level languages (parts I and II). Comput. Lang., 1(2 & 3):161--194, 197--218, 1975.
• 10: Miley Semmelroth , Amr Sabry, Monadic encapsulation in ML, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.8-17, September 27-29, 1999, Paris, France
• 11: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 12: J.-P. Talpin and P. Jouvelot. Polymorphic type, region, and effect inference. J. Func. Prog., 2(3):245--271, 1992.
• 13: M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, P. Sestoft, and P. Bertelsen. Programming with regions in the ML Kit (for version 3). Technical Report DIKU-TR-98/25, Department of Computer Science, University of Copenhagen (DIKU), 1998.
• 14: M. Tofte and N. Hallenberg. Region-based memory management in perspective. In F. Henglein, J. Hughes, H. Makholm, and H. Niss, editors, Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE), pages 23--30, 2001.
• 15: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 16: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 17: Philip Wadler, The marriage of effects and monads, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.63-74, September 26-29, 1998, Baltimore, Maryland, United States
• 18: David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

General Terms:
Algorithms, Performance