Typed Memory Management via Static Capabilities
Abstract
Region-based memory management is an alternative to standard tracing
garbage collection that makes operations such as
memory deallocation explicit but verifiably safe. In this article,
we present a new compiler intermediate language, called the
Capability Language (CL), that supports region-based memory management and
enjoys a provably safe type system. Unlike previous region-based type
systems, region lifetimes need not be lexically scoped, and yet the
language may be checked for safety without complex analyses.
Therefore, our type system may be deployed in settings such as
extensible operating systems where both the performance and safety
of untrusted code is important.
The central novelty of the language is the use of static capabilities
to specify the permissibility of various operations, such as memory
access and deallocation. In order to ensure capabilities are
relinquished properly, the type system tracks aliasing information
using a form of bounded quantification. Moreover, unlike previous
work on region-based type systems, the proof of soundness of our type
system is relatively simple, employing only standard syntactic
techniques.
In order to show how our language may be used in practice, we show how
to translate a variant of Tofte and Talpin's high-level
type-and-effects system for region-based memory management into our
language. When combined with known region inference
algorithms, this translation provides a way to compile source-level
languages to CL.
(postscript)