一句话:首个支持异常与效应处理器间非局部控制转移的自动资源界分析,扩展了基于类型的 AARA。
自动推导参数化资源(代价)界的技术已能处理大量语言特性,但异常与效应处理器所需的非局部控制转移一直是难点。本文提出首个支持异常/效应与其处理器之间非局部控制转移的自动资源界分析。该方法扩展了基于类型的自动摊销资源分析(AARA),为带列表和线性 potential 函数的简单函数式语言设计了新的类型系统,并给出一种新颖的语法式类型可靠性定理,相对于基于栈的抽象机器证明所推导界的正确性;其思想可直接推广,并在 Standard ML 与多项式 potential 函数上实现。实验表明,该分析能处理现有方法无法分析的程序,且支持异常与效应处理器的效率开销较低。
There exist many techniques for automatically deriving parametric resource (or cost) bounds by analyzing the source code of a program. These techniques work effectively for a large class of programs and language features. However, non-local transfer of control as needed for exception or effect handlers has remained a challenge. This paper presents the first automatic resource bound analysis that supports non-local control transfer between exceptions or effects and their handlers. The analysis is an extension of type-based automatic amortized resource analysis (AARA), which automates the potential method of amortized analysis. It is presented for a simple functional language with lists and linear potential functions. However, the ideas are directly applicable to richer settings and implemented for Standard ML and polynomial potential functions. Apart from the new type system for exceptions and effects, a main contribution is a novel syntactic type-soundness theorem that establishes the correctness of the derived bounds with respect to a stack-based abstract machine. An experimental evaluation shows that the new analysis is capable of analyzing programs that cannot be analyzed by existing methods and that the efficiency overhead of supporting exception and effect handlers is low.
@article{paperbot3780,
title = {Handling Exceptions and Effects with Automatic Resource Analysis},
author = {Ethan Chu and Yiyang Guo and Jan Hoffmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798207}
}