| 1 |
Typed memory management via static capabilities
|
|
|
|
In: http://www.cs.cmu.edu/~crary/papers/2000/regions/capabilities.pdf
|
|
Abstract:
Region-based memory management is an alternative to standard tracing garbage collection that makes operations such as memory deallocation explicit but veriably 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 quantication. 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-eects 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.
|
|
Keyword:
Categories and Subject Descriptors; Certied code; D.3.1 [Programming Languages; D.3.4 [Programming Languages; F.3.2 [Logics and Meanings of Programs; F.3.3 [Logics and Meanings of Programs; Formal Denitions and Theory|Semantics; Languages; Processors|Compilers; region-based memory management; Semantics of Programming Languages|Operational Semantics; Studies of Program Constructs|Type Structure General Terms; Syntax; Theory; type- directed compilation; typed intermediate languages; Verication Additional Key Words and Phrases
|
|
URL: http://www.cs.cmu.edu/~crary/papers/2000/regions/capabilities.pdf
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.5862
|
|
BASE
|
|
Hide details
|
|
|
|
|
