High-level type-safe languages such as Java and ML are equipped with tracing garbage collectors to take care of recycling memory resources. For most programming tasks, this situation is ideal; the programmer does not have to worry about the tedious and error-prone task of explicitly managing memory. However, for some applications, alternative memory management strategies can result in significant performance improvements. Moreover, compilers often implement memory management optimizations to improve upon the performance of tracing garbage collectors. Normally, such optimizations are implemented in untyped languages, but there are numerous benefits to designing advanced type systems for checking the safety of optimized code. For example, such a type system can be used in a certifying compiler that produces optimized proof-carrying code.
In this talk, I will discuss some recent work on a type system for low-level languages with explicit operations for allocating, deallocating, and reusing memory to store objects of different types. The type system is derived from linear type systems, but is considerably more powerful as it admits a degree of aliasing. Using the "alias types" that I will define, it is possible to track many sources of aliasing that are introduced naturally during compilation. It is also possible to construct conventional linear data structures such as linear lists and trees as well as more complex data structures such as cyclic lists and queues.
We have proven a core language sound and have implemented (a portion of) the type system in Cornell's Typed Assembly Language, where aliasing is ubiquitous. Among other things, our certifying compiler uses alias types to certify that data structures are initialized properly and that code generated at run-time is manipulated safely.
This is joint work with Fred Smith and Greg Morrisett.