paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Zero-Overhead Lexical Effect Handlers

零开销的词法作用域效应处理器
OOPSLA 9(OOPSLA2)2025匹配度 2/10 · 该论文属于程序语言与编译器方向的效应处理器实现,虽兼具形式化与工程实现,但与用户核心关注的 PL 与 LLM/Agent 交叉、静态分析、浮点程序分析、贝叶斯程序分析均无直接关系。引用 2 inbox
Cong Ma, Zhaoyi Ge, Max Jung, Yizhou Zhang
crossref: 2026-09-10

AI 速览

一句话:提出类型制导翻译,使词法作用域效应处理器在无效应时不增加主代码运行时开销,并形式化证明其正确性。

异常处理器及更一般的效应处理器用于结构化非局部控制流。词法作用域处理器解决了动态作用域的模块化问题,但已有实现仅因词法上下文存在处理器就让程序付出开销。本文提出一种异常效应的词法作用域处理器实现:用类型制导翻译生成处理器进入词法上下文的信息,指导运行时栈遍历定位正确处理器;无需具体化处理器词法标识符,主代码也不因处理器存在而变慢。作者形式化核心编译方案并证明正确性,并集成到 Lexa,可按效应预期调用频率定制编译策略。实验表明,新编译器在低效应/无效应场景降低运行时开销,在效应密集负载中保持有竞争力。

问题
词法作用域效应处理器虽解决动态作用域的模块化问题,但已有实现使程序仅因词法上下文中存在处理器就承担运行时开销。
方法
提出类型制导翻译,生成处理器进入词法上下文的信息以指导运行时栈遍历,无需具体化词法标识符;形式化并证明该编译方案正确,并集成到 Lexa 支持按效应调用频率定制。
评估
通过集成 Lexa 编译器并进行经验评估,显示低/无效应场景下运行时开销降低,效应密集负载中性能保持竞争力。
原文摘要(Abstract)

Exception handlers—and effect handlers more generally—are language mechanisms for structured nonlocal control flow. A recent trend in language-design research has introduced lexically scoped handlers, which address a modularity problem with dynamic scoping. While dynamically scoped handlers allow zero-overhead implementations when no effects are raised, existing implementations of lexically scoped handlers require programs to pay a cost just for having handlers in the lexical context. In this paper, we present a novel approach to implementing lexically scoped handlers of exceptional effects. It satisfies the zero-overhead principle—a property otherwise met by most modern compilers supporting dynamically scoped exception handlers. The key idea is a type-directed translation that emits information indicating how handlers come into the lexical context. This information guides the runtime in walking the stack to locate the right handler. Crucially, no reified lexical identifiers of handlers are needed, and mainline code is not slowed down by the presence of handlers in the program text. We formalize the essential aspects of this compilation scheme and prove it correct. We integrate our approach into the Lexa language, allowing the compilation strategy to be customized for each declared effect based on its expected invocation rate. Empirical results suggest that the new Lexa compiler reduces run-time overhead in low-effect or no-effect scenarios while preserving competitive performance for effect-heavy workloads.

链接与引用

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

BibTeX
@article{paperbot2975,
  title = {Zero-Overhead Lexical Effect Handlers},
  author = {Cong Ma and Zhaoyi Ge and Max Jung and Yizhou Zhang},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763177}
}