paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Parallelism in a Region Inference Context

区域推断上下文中的并行性
PLDI 7(PLDI)2023匹配度 3/10 · 论文属于类型系统与编译器中的区域推断/静态分析,并结合并行内存管理,具备理论形式化与工程实现,但与用户核心关注的 LLM/Agent 程序静态分析、浮点程序分析、贝叶斯程序分析及其与 LLM 的交叉均无直接关系。引用 2 inbox
Martin Elsman, Troels Henriksen
crossref: 2026-09-10

AI 速览

一句话:为基于区域推断的编译器设计 fork-join 并行构造,并给出类型规则、动态语义、类型可靠性及效应推断算法。

区域推断是一种基于类型的内存管理分析,可将未标注程序转换为显式使用区域栈进行分配与释放的程序;区域内存管理在并行执行中已有优势,但与高阶并行编程的结合尚未研究。本文面向基于区域推断的编译器实现 fork-join 并行构造,给出包含该构造的最小高阶语言的类型规则与动态语义,证明类型可靠性,并提出一种新的基于效应的区域保护推断算法。作者将该方法高效嵌入 MLKit Standard ML 编译器,使用一组并行基准进行评估,结果表明该技术能在高阶函数式环境中有效利用多核架构。

问题
如何将 fork-join 并行构造与区域推断及高阶并行编程结合,同时安全地管理区域内存。
方法
定义一个含并行构造的最小高阶语言,给出类型规则和动态语义,证明类型可靠性,并提出基于效应的区域保护推断算法,实现在 MLKit 编译器中。
评估
在多个并行基准上评估实现,显示其能在高阶函数式设置下有效利用多核架构。
原文摘要(Abstract)

Region inference is a type-based program analysis that takes a non-annotated program as input and constructs a program that explicitly manages memory allocation and deallocation by dividing the heap into a stack of regions, each of which can grow and shrink independently from other regions, using constant-time operations.Whereas region-based memory management has shown useful in the contexts of explicit region-based memory management, and in particular, in combination with parallel execution of code, combining region inference with techniques for higher-order parallel programming has not been investigated.In this paper, we present an implementation of a fork-join parallel construct suitable for a compiler based on region inference. We present a minimal higher-order language incorporating the parallel construct, including typing rules and a dynamic semantics for the language, and demonstrate type soundness. We present a novel effect-based region-protection inference algorithm and discuss benefits and shortcomings of the approach. We also describe an efficient implementation embedded in the MLKit Standard ML compiler. Finally, we evaluate the approach and the implementation based on a number of parallel benchmarks, and thereby demonstrate that the technique effectively utilises multi-core architectures in a higher-order functional setting.

链接与引用

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

BibTeX
@article{paperbot2008,
  title = {Parallelism in a Region Inference Context},
  author = {Martin Elsman and Troels Henriksen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591256}
}