Perceus: garbage free reference counting with reuse
Perceus: garbage free reference counting with reuse
复制标题
Perceus：具有重用性的无垃圾引用计数
DOI：
10.1145/3453483.3454032
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Daan Leijen
中科院分区：
文献类型：
--
作者：
Alex Reinking;Ningning Xie;L. de Moura;Daan Leijen
我们介绍了Perceus算法，它是一种具有可重用性和专门化的精确引用计数算法。从具有显式控制流的函数式核心语言开始，Perceus发出精确的引用计数指令，使得(无周期的)程序是无垃圾的，其中只保留活动引用。这支持进一步的优化，如允许在运行时保证就地更新的重用分析。这反过来又启用了一种新的编程范例，我们称之为_函数但就地_(FBIP)。就像尾部调用优化允许使用常规函数调用编写循环一样，重用分析允许以纯函数方式编写就地变异算法。给出了线性资源演算中引用计数的一种新的形式化形式，并证明了Perceus是健全的和无垃圾的。我们的证据表明，Perceus，如在Koka中实现的，具有良好的性能，并与其他最先进的内存收集器竞争。
We introduce Perceus, an algorithm for precise reference counting with reuse and specialization. Starting from a functional core language with explicit control-flow, Perceus emits precise reference counting instructions such that (cycle-free) programs are _garbage free_, where only live references are retained. This enables further optimizations, like reuse analysis that allows for guaranteed in-place updates at runtime. This in turn enables a novel programming paradigm that we call _functional but in-place_ (FBIP). Much like tail-call optimization enables writing loops with regular function calls, reuse analysis enables writing in-place mutating algorithms in a purely functional way. We give a novel formalization of reference counting in a linear resource calculus, and prove that Perceus is sound and garbage free. We show evidence that Perceus, as implemented in Koka, has good performance and is competitive with other state-of-the-art memory collectors.