A type theory for memory allocation and data layout

ABSTRACT

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We show that a language based on ordered types can use this property to give an exact account of the layout of data in memory. The fuse constructor from ordered logic describes adjacency of values in memory, and the mobility modal describes pointers into the heap. We choose a particular allocation model based on a common implementation scheme for copying garbage collection and show how this permits us to separate out the allocation and initialization of memory locations in such a way as to account for optimizations such as the coalescing of multiple calls to the allocator.

REFERENCES

• 1: Jawahar Chirimar, Carl A. Gunter, and Jon G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2):195--244, 1996.
• 2: Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.95-107, June 18-21, 2000, Vancouver, British Columbia, Canada
• 3: Karl Crary , J. Gregory Morrisett, Type Structure for Low-Level Programming Languages, Proceedings of the 26th International Colloquium on Automata, Languages and Programming, p.40-54, July 11-15, 1999
• 4: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• 5: A. Igarashi and N. Kobayashi. Garbage collection based on a linear type system, 2000.
• 6: T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of c, June 2002.
• 7: 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]
• 8: Yasuhiko Minamide, A functional representation of data structures with a hole, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.75-84, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268953]
• 9: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support for System Software, pages 25--35, Atlanta, Georgia, May 1999.
• 10: G. Morrisett , R. Harper, Semantics of memory management for polymorphic languages, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 11: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 12: 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
• 13: Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning. A type theory for memory allocation and data layout. Technical Report CMU-CS-02-171, Department of Computer Science, Carnegie Mellon University, December 2002.
• 14: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 15: Jeff Polakow , Frank Pfenning, Ordered linear logic and applications, 2001
• 16: Jeff Polakow , Frank Pfenning, Natural Deduction for Intuitionistic Non-communicative Linear Logic, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, p.295-309, April 07-09, 1999
• 17: Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20.
• 18: Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In J.Despeyroux, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), Santa Barbara, California, June 2000.
• 19: Zhong Shao. An overview of the FLINT/ML compiler. In 1997 Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Department Technical Report BCCS-97-03.
• 20: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 21: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 22: David N. Turner , Philip Wadler, Operational interpretations of linear logic, Theoretical Computer Science, v.227 n.1-2, p.231-248, Oct. 1, 1999 [doi>10.1016/S0304-3975(99)00054-7]
• 23: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

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

General Terms:
Languages, Theory

Keywords:
data representation, memory management, ordered logic, type theory