Handling Exceptions and Effects with Automatic Resource Analysis

TL;DR

This paper introduces an automatic resource analysis method that handles non-local control transfer via exceptions and effects, extending type-based amortized analysis to support richer control flow in functional languages.

Contribution

It presents the first type-based resource analysis supporting non-local control transfer for exceptions and effects, with a novel type system and correctness proof.

Findings

Analyzes programs with exceptions and effects that previous methods cannot handle.

Supports implementation in Standard ML with polynomial potential functions.

Experimental results show low overhead and improved analysis capabilities.

Abstract

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.