A type system for safe memory management and its proof of correctness

ABSTRACT

We present a destruction-aware type system for the functional language Safe, which is a first-order eager language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in constant time.

The language is equipped with several analyses and inference algorithms so that regions, sharing information and types are automatically inferred by the compiler. Here, we concentrate on the correctness of the type system with respect to the operational semantics of the language. In particular, we prove that, in spite of sharing and of the use of implicit and explicit memory deallocation operations, all well-typed programs will be free of dangling pointers at runtime.

The paper ends up with some examples of well-typed programs.

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: David Aspinall , Martin Hofmann, Another Type System for In-Place Update, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.36-52, April 08-12, 2002
• 3: David Aspinall , Martin Hofmann , Michal KoneČnÝ, A type system with usage aspects, Journal of Functional Programming, v.18 n.2, p.141-178, March 2008 [doi>10.1017/S0956796807006399]
• 4: 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]
• 5: M. Fluet, G. Morrisett, and A. J. Ahmed. Linear regions are all you need. In Europeam Symposium On Programming, ESOP'06, pages 7--21, 2006.
• 6: 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
• 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: Naoki Kobayashi, Quasi-linear types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.29-42, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292546]
• 9: S. Lucas and R. Peña. Termination and Complexity Bounds for SAFE Programs. In Proc. 19th Int. Symp. on Implementation and Application of Functional Languages, IFL'07, Freiburg, Sept. 2007, pages 8--23, 2007.
• 10: M. Montenegro, R. Peña, and C. Segura. An Inference Algorithm for Guaranteeing Safe Destruction. In Proc. 8th Symp. on Trends in Functional Programming, TFP'07. New York, April 2007, pages XIV-1--16, 2007.
• 11: M. Montenegro, R. Peña, and C. Segura. A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation, 2008. Submitted to 17th Int'l Workshop on Functional and (Constraint) Logic Programming, Siena, Italy July, 2008.
• 12: M. Montenegro, R. Peña, and C. Segura. A Simple Region Inference Algorithm for a First-Order Functional Language. In Ninth Symposium on Trends in Functional Programming, TFP'08, Nijmegen, The Netherlands, May. 2008, pages XV-1--15, 2008.
• 13: M. Montenegro, R. Peña, and C. Segura. A type system for safe memory management and its proof of correctness. Technical report, Dpto. de Sistemas Informticos y Computación. Universidad Complutense de Madrid, 2008. Technical Report SIC-5-08.
• 14: 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]
• 15: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 16: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 17: Martin Odersky, Observers for linear types, Symposium proceedings on 4th European symposium on programming, p.390-407, January 1992, Rennes, France
• 18: R. Peña, C. Segura, and M. Montenegro. A Sharing Analysis for SAFE. In Selected Papers of the 7th Symp. on Trends in Functional Programming, TFP'06., pages 109--128. Intellect, 2007.
• 19: M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, and P. Sestoft. Programming with regions in the MLKit (revised for version 4.3.0). Technical report, IT University of Copenhagen, Denmark, 2006.
• 20: 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]
• 21: P. Wadler. Linear types can change the world! In IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561--581. North Holland, 1990.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Dynamic storage management
      D.3.4 Processors
          Subjects: Memory management (garbage collection); Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis; Operational semantics

General Terms:
Languages, Security

Keywords:
safe memory deallocation, type systems