Typed memory management in a calculus of capabilities

Karl Crary, David Walker, Greg Morrisett

Research output: Contribution to journalConference article

120 Scopus citations

Abstract

An increasing number of systems rely on programming language technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a complex, trusted garbage collector. Region-based type systems provide an alternative to garbage collection by making memory management explicit but verifiably safe. However, it has not been clear how to use regions in low-level, type-safe code. We present a compiler intermediate language, called the Capability Calculus, that supports region-based memory management, enjoys a provably safe type system, and is straightforward to compile to a typed assembly language. Source languages may be compiled to our language using known region inference algorithms. Furthermore, region lifetimes need not be lexically scoped in our language, yet the language may be checked for safety without complex analyses. Finally, our soundness proof is relatively simple, employing only standard techniques. The central novelty 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.

Original languageEnglish (US)
Pages (from-to)262-275
Number of pages14
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
DOIs
StatePublished - 1999
EventProceedings of the 1999 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, POPL'99 - San Antonio, TX, USA
Duration: Jan 20 1999Jan 22 1999

All Science Journal Classification (ASJC) codes

  • Software

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

  • Cite this