Typed memory management in a calculus of capabilities
Typed memory management in a calculus of capabilities
复制标题
能力演算中的类型化内存管理
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
G. Morrisett
中科院分区：
文献类型：
--
作者：
Karl Crary;D. Walker;G. Morrisett
越来越多的系统依赖于编程语言技术来确保低级代码的安全性。不幸的是，这些系统通常依赖一个复杂的，值得信赖的垃圾收集器。基于区域的类型系统通过使内存管理明确但可靠地安全，为垃圾收集提供了替代。但是，尚不清楚如何在低级，类型安全的代码中使用区域。我们提出了一种编译器中间语言，称为“能力微积分”，该语言支持基于区域的内存管理，享有一个可证明的安全类型系统，并且是直接编译到打字的汇编语言。可以使用已知区域推理算法将源语言汇编为我们的语言。此外，区域寿命不必用我们的语言递送词汇，但是可以在没有复杂分析的情况下检查该语言以确保安全。最后，我们的健全性证明相对简单，仅采用标准技术。中心新颖的是使用静态功能来指定各种操作的允许性，例如内存访问和交易。为了确保正确放弃功能，该类型系统使用有限量化的形式跟踪混杂信息。
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.