Amortised resource analysis for object-oriented programs

As software systems rise in size and complexity, the need for
verifying some of their properties increases. One important
property to be verified is the resource usage, i.e. how many
resources the program will need for its execution, where resources
include execution time, memory, power, etc. Resource usage analysis
is important in many areas, in particular embedded systems and
cloud computing. Thus, resource analysis has been widely researched
and some different approaches to this have been proposed based in
particular on recurrence solving, abstract interpretation and
amortised analysis. In the amortised analysis technique, a
nonnegative number, called potential, is assigned to a data
structure. The amortised cost of operations is then defined by its
actual cost plus the difference in potential of the data structure
before and after performing the operation. Amortised analysis has
been used for automatic resource analysis of functional and
object-oriented programs. The potentials are defined using refined
types and typing rules then ensure that potential and actual
resource usage is accounted for correctly. The automatic inference
of the potential functions can then be achieved by type inference.
In the case of functional programs, the structure of the types is
known. Thus, type inference can be reduced to solving linear
arithmetic constraints. For object-oriented programs, however, the
refined types are more complicated because of the general nature of
objects: they can be used to define any data structure. Thus, the
type inference must discover not only the potential functions for
the data structure but also the data structures themselves. Other
features of object-oriented programs that complicate the analysis
are aliasing and imperative update. Hofmann and Jost presented in
2006 a type system for amortised heap-space analysis of
object-oriented programs, called Resource Aware JAva (RAJA).
However, they left the problem of type inference open. In this
thesis we present a type inference algorithm for the RAJA system.
We were able to reduce the type inference problem to the novel
problem of satisfiability of arithmetic constraints over infinite
trees and we developed a heuristic algorithm for satisfiability of
these constraints. We proved the soundness of the type inference
algorithm and developed an OCaml implementation and experimental
evaluation that shows that we can compute linear upper-bounds to
the heap-space requirements of many programs, including sorting
algorithms for lists such as insertion sort and merge sort and also
programs that contain different interacting objects that describe
real-life scenarios like a bank account. Another contribution of
this thesis is a type checking algorithm for the RAJA system that
is useful for verifying the types discovered by the type inference
by using the \emph{proof carrying code} technology.