Types with potential: polynomial resource bounds via automatic amortized analysis

A primary feature of a computer program is its quantitative
performance characteristics: the amount of resources such as time,
memory, and power the program needs to perform its task. Concrete
resource bounds for specific hardware have many important
applications in software development but their manual determination
is tedious and error-prone. This dissertation studies the problem
of automatically determining concrete worst-case bounds on the
quantitative resource consumption of functional programs.
Traditionally, automatic resource analyses are based on recurrence
relations. The difficulty of both extracting and solving recurrence
relations has led to the development of type-based resource
analyses that are compositional, modular, and formally verifiable.
However, existing automatic analyses based on amortization or sized
types can only compute bounds that are linear in the sizes of the
arguments of a function. This work presents a novel type system
that derives polynomial bounds from first-order functional
programs. As pioneered by Hofmann and Jost for linear bounds, it
relies on the potential method of amortized analysis. Types are
annotated with multivariate resource polynomials, a rich class of
functions that generalize non-negative linear combinations of
binomial coefficients. The main theorem states that type
derivations establish resource bounds that are sound with respect
to the resource-consumption of programs which is formalized by a
big-step operational semantics. Simple local type rules allow for
an efficient inference algorithm for the type annotations which
relies on linear constraint solving only. This gives rise to an
analysis system that is fully automatic if a maximal degree of the
bounding polynomials is given. The analysis is generic in the
resource of interest and can derive bounds on time and space usage.
The bounds are naturally closed under composition and eventually
summarized in closed, easily understood formulas. The
practicability of this automatic amortized analysis is verified
with a publicly available implementation and a reproducible
experimental evaluation. The experiments with a wide range of
examples from functional programming show that the inference of the
bounds only takes a couple of seconds in most cases. The derived
heap-space and evaluation-step bounds are compared with the
measured worst-case behavior of the programs. Most bounds are
asymptotically tight, and the constant factors are close or even
identical to the optimal ones. For the first time we are able to
automatically and precisely analyze the resource consumption of
involved programs such as quick sort for lists of lists, longest
common subsequence via dynamic programming, and multiplication of a
list of matrices with different, fitting dimensions.