Reference Counting with Frame Limited Reuse
summary
Defines Perceus garbage-free refcounting that inserts precise increment/drop ops so objects free exactly when unreachable, adds a new drop-guided reuse analysis that converts drops to reuse tokens after Perceus runs, proves reuse is frame-limited via a simplified linear resource calculus, implements it in Koka, and measures large benchmarks (4,200,000-element red‑black tree insert) showing significant speedups and memory boundedness while avoiding the fragility and peak-heap blowups of prior reuse schemes.
AI-written summary · about
chapters (6)
- 0:00Introduction to Koka
- 1:14Understanding Perseus
- 3:32Reuse analysis challenges
- 6:23Drop-guided reuse
- 9:12Formalizing memory bounds
- 13:00Case study and performance
related talks
30mA Mechanised Semantics of Erlang’s References
16mSound Garbage Collection for C using Pointer Provenance
17mAn Effectively Ω(c) Language and Runtime
21mGarbage Collection for Higher Inductive Types
18mThe One Pass (OP) Compactor (an intellectual abstract)
50mAn insight into Go Garbage Collection
28mCERES: Making Equality Saturation Memory-Scalable
28mA Mechanically Verified Garbage Collector for OCaml