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.

翻译：目前存在多种通过分析程序源代码自动推导参数化资源（或成本）边界的技术。这些技术对大多数程序类别和语言特性均能有效工作。然而，异常或效应处理器所需的非局部控制转移始终是一个挑战。本文提出了首个支持异常或效应与其处理器之间非局部控制转移的自动资源边界分析方法。该分析是基于类型的自动摊销资源分析（AARA）的扩展，后者实现了摊销分析的势能方法自动化。本文以包含列表和线性势能函数的简单函数式语言为框架进行阐述，但其核心思想可直接应用于更丰富的语言环境，并已在Standard ML和多项式势能函数中实现。除了针对异常和效应的新型类型系统外，主要贡献在于提出了一种新颖的语法类型可靠性定理，该定理基于栈式抽象机确立了所推导边界的正确性。实验评估表明，新分析方法能够处理现有方法无法分析的复杂程序，且支持异常和效应处理器带来的效率开销较低。