Handling Exceptions and Effects with Automatic Resource Analysis

TL;DR

This paper presents the first automatic resource bound analysis that supports non-local control transfer between exceptions or effects and their handlers, and is an extension of type-based automatic amortized resource analysis (AARA), which automates the potential method of amortized analysis.

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.

Figures (11)

• Figure 1: The SML function sqdist computes the square of the Euclidean distance between two $n$-dimensional vectors (lists of reals). The function R.tick is used to specify resource use.
• Figure 2: The functions distances_1 and distances_2 in SML. The exception handler in distances_2 incurs a cost of 1 whenever it is evaluated. The function call List.map f l applies f to each element of l.
• Figure 3: Example implementing a stack store with effect handlers. We assume access to traverse : $L(\mathbb{Z}) \to \mathsf{unit}$.
• Figure 4: Zeroing Resource Annotated Types
• Figure 5: Typing rules for values

Theorems & Definitions (17)

• lemma 1
• lemma 2
• lemma 3
• lemma 4: Substitution
• lemma 5: Stack Append Typing
• theorem 1: Preservation
• theorem 2: Progress
• lemma 6
• lemma 7: Sharing
• lemma 8: Potential Relax