Typed memory management via static capabilities

David Walker, Karl Crary, Greg Morrisett

Research output: Contribution to journalArticle

78 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)701-771
Number of pages71
JournalACM Transactions on Programming Languages and Systems
Volume22
Issue number4
DOIs
StatePublished - Jul 2000
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • D.3.1 [Programming Languages]: Formal Definitions and Theory - Semantics, Syntax
  • D.3.4 [Programming Languages]: Processors - Compilers
  • F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages - Operational Semantics

Fingerprint Dive into the research topics of 'Typed memory management via static capabilities'. Together they form a unique fingerprint.

  • Cite this