Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
cs.PL
Aug 15, 2019 · v2
TL;DR
Describes the reference counting optimizations implemented in the Lean 4 compiler runtime.
Abstract
Most functional languages rely on some form of garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has less bookkeeping overhead at runtime. However, having an exact reference count of each value can enable optimizations such as destructive updates. We explore these optimization opportunities in the context of an eager, purely functional programming language. We propose a new mechanism for efficiently reclaiming memory used by nonshared values, reducing stress on the global memory allocator. We also describe an approach for minimizing the number of reference count updates using borrowed references and a heuristic for automatically inferring borrow annotations. These techniques have been implemented in a new compiler for an eager and purely functional programming language with support for multi-threading. Our preliminary experimental results demonstrate our approach is competitive and often outperforms state-of-the-art compilers.
Problem
Most functional languages use tracing garbage collectors rather than reference counting, missing optimization opportunities such as destructive updates that exact reference counts enable. Minimizing reference counting overhead in purely functional languages remained an open engineering challenge.
Approach
The authors explore reference counting optimizations for an eager, purely functional programming language. They propose a mechanism for efficiently reclaiming memory used by nonshared values (reducing stress on the global allocator), and describe an approach for minimizing reference count updates using borrowed references with a heuristic for automatically inferring borrow annotations. These techniques are implemented in a new compiler for Lean 4, which is an eager purely functional language with multi-threading support.
Results
Preliminary experimental results demonstrate the approach is competitive with and often outperforms state-of-the-art compilers for functional languages, validating that reference counting with borrowing optimizations is viable for purely functional programming.
