paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Garbage-Collection Safety for Region-Based Type-Polymorphic Programs

基于 region 的类型多态程序的垃圾回收安全性
PLDI 7(PLDI)2023匹配度 2/10 · 该论文属于传统程序语言理论中的区域推断、类型系统与 GC 安全性,虽包含形式化与实现且是问题驱动,但不涉及 ML/Agent 程序静态分析、LLM 改进静态分析、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 2 inbox
Martin Elsman
crossref: 2026-09-10

AI 速览

一句话:指出区域推断对多态高阶程序的 GC 安全性缺陷,提出带 GC 效应的区域类型系统并修复实现。

区域推断通过在编译期插入分配与释放指令,减少甚至消除引用追踪垃圾回收,并与分代 GC 互补;但当混合使用时,必须保证高阶多态程序在追踪回收期间不出现悬挂指针。本文指出既有理论发展存在可靠性问题,且该问题在基于区域推断的真实实现中表现为实际缺陷。为解决此问题,作者提出一个修改但简单的区域类型系统,能够刻画垃圾回收效应,并覆盖多态高阶代码;文中还概述如何调整区域推断与区域表示分析以适配新类型系统。新系统为函数关联更简单的区域类型方案,支持将基于区域的内存管理与部分无标签的引用追踪(及分代)GC 结合,并修正了依赖此前错误已发表结果的后续工作。

问题
既有区域推断理论在混合引用追踪 GC 时,对高阶多态程序可能无法保证回收期间无悬挂指针,且该可靠性问题已在真实实现中暴露。
方法
提出可刻画 GC 效应的改进区域类型系统,并说明区域推断与区域表示分析如何适配;新系统能为函数给出更简单的区域类型方案。
评估
通过揭示既有理论/实现中的可靠性缺陷并给出修复,论证新类型系统可支持与部分无标签的引用追踪及分代 GC 结合,并修复依赖错误结果的工作。
原文摘要(Abstract)

Region inference offers a mechanism to reduce (and sometimes entirely remove) the need for reference-tracing garbage collection by inferring where to insert allocation and deallocation instructions in a program at compile time. When the mechanism is combined with techniques for reference-tracing garbage collection, which is helpful in general to support programs with very dynamic memory behaviours, it turns out that region-inference is complementary to adding generations to a reference-tracing collector. However, region-inference and the associated region-representation analyses that make such a memory management strategy perform well in practice are complex, both from a theoretical point-of-view and from an implementation point-of-view.In this paper, we demonstrate a soundness problem with existing theoretical developments, which have to do with ensuring that, even for higher-order polymorphic programs, no dangling-pointers appear during a reference-tracing collection. This problem has materialised as a practical soundness problem in a real implementation based on region inference. As a solution, we present a modified, yet simple, region type-system that captures garbage-collection effects, even for polymorphic higher-order code, and outline how region inference and region-representation analyses are adapted to the new type system. The new type system allows for associating simpler region type-schemes with functions, compared to original work, makes it possible to combine region-based memory management with partly tag-free reference-tracing (and generational) garbage-collection, and repairs previously derived work that is based on the erroneous published results.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2004,
  title = {Garbage-Collection Safety for Region-Based Type-Polymorphic Programs},
  author = {Martin Elsman},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591229}
}