LFCS Seminar: 30 March 2021 - Ningning Xie

Title: Garbage Free Reference Counting with Reuse

Abstract: 

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 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.

Joint work with Alex Reinking, Leonardo de Mooura, and Daan Leijen.

Affiliation:

Ningning Xie, University of Hong Kong

https://xnning.github.io/