fluet-thesis.double.pdf
fluet-thesis.single.pdf
(PhD thesis;
20060727-Defense.ppt)
Region-based memory management is a scheme for managing dynamically
allocated data. A defining characteristic of region-based memory
management is the bulk deallocation of data, which avoids both the
tedium of malloc/free and the overheads of a garbage
collector. Type systems for region-based memory management enhance
the utility of this scheme by statically determining when a program is
guaranteed to not perform any erroneous region operations.
We describe three type systems for region-based memory management:
- a type-and-effect system (a la the Tofte-Talpin region calculus);
- a novel monadic type system;
- a novel substructural type system.
We demonstrate how to successively encode the type-and-effect system
into the monadic type system and the monadic type system into the
substructural type system. These type systems and encodings support
the argument that the type-and-effect systems that have traditionally
been used to ensure the safety of region-based memory management are
neither the simplest nor the most expressive type systems for this
purpose.
The monadic type system generalizes the state monad of Launchbury and
Peyton Jones and demonstrates that the well-understood parametric
polymorphism of System F provides sufficient encapsulation to ensure
the safety of region-based memory management. The essence of the
first encoding is to translate effects to an indexed monad, trading
the subtleties of a type-and-effect system for the simplicity of a
monadic type system.
However, both the type-and-effect system and the monadic type system
require that regions have nested lifetimes, following the lexical
scope of the program, restricting when data may be effectively
reclaimed. Hence, we introduce a substructural type system that
eliminates the nested-lifetimes requirement. The key idea is to
introduce first-class capabilities that mediate access to a region and
to provide separate primitives for creating and destroying regions.
The essence of the second encoding is to ``break open'' the monad to
reveal its store-passing implementation.
Finally, we show that the substructural type system is expressive
enough to faithfully encode other advanced memory-management features.