# Introduction

In recent years, a considerable amount of research has been carried
out into the prediction and certification of resource usage of
computer programs. The term *resource* refers to some quantity
which can be regarded as a *cost* of the program. Typical
resources include quantities such as time and heap space usage, but
other quantities such as the number of SMS messages sent by a Java
application installed on a mobile phone have also been considered.

In RESA, we are concentrating on static analysis techniques because these enable reliable guarantees to be produced without requiring a program to be executed; thus the resource usage of a program can be evaluated before it is even installed on its target platform.

# Techniques

We are using two main high-level analysis techniques: *amortised
analysis* and *lattice-point enumeration in polytopes*. These
are supported by lower-level abstract interpretation methods.

## Amortised analysis

Amortised resource analysis is based on Tarjan’s observation [1] that the statement and proof of complexity bounds for operations on some data structures can be simplified if we think of the elements of the data structure as being able to store “credits” which are used up by later operations. We have shown how amortisation techniques can be combined with Separation Logic to reason about resource usage associated with complex data structures: see [2] for details.

An analysis technique which predicts resource usage using linear programming in conjunction with the techniques described above has also been developed and implemented.

## Lattice points

Amortisation techniques are useful for dealing with resources associated with data structures, but are less useful for nested loop structures controlled by numerical program variables. We have been exploring the use of geometric techniques to predict the resource usage of such structures.

Consider the following fragment of a Java program:

```
for (i=1; i<=9; i++)
for (j=1; j<=i && j<=7; j++)
System.out.println ("Hello");
```

How many times is the `println` statement executed? (More
generally, we might be allocating memory or sending an SMS message.)
Note that every time `println` is encountered we have the inequalities 1
≤ i ≤ 9, 1 ≤ j ≤ 7, and j ≤ i, which delineate a
trapezoidal region in the (i,j)-plane:

It is easily seen that the number of times that the `println` statement is
executed is
equal to the number of *lattice points* (points with integer
coordinates: move your mouse over the image) within the region. There is a rich mathematical theory
dealing with the problem of counting lattice points within regions
described by linear constraints [3,4] and we are
implementing a resource analysis using these techniques.

Ultimately we hope to combine amortised analysis with lattice-point enumeration in order to obtain a method which will enable automatic resource analysis of a wide range of Java bytecode programs.

# Tools

We intend to develop a static analysis tool for Java bytecode programs. We are implementing a stand-alone command-line based tool in the OCaml functional programming language, and eventually we plan to incorporate this into a plugin for the eclipse Java development environment. Since eclipse is widely used by Java programmers, this will make our tool available to programmers in a straightforward way in a familiar environment. See [5] for more information.

## References

1. Robert E. Tarjan. Amortized computational complexity.

SIAM Journal on Algebraic Discrete Methods, Vol. 6, No. 2. (April 1985), pp. 306-318.

2. Robert Atkey. Amortised Resource Analysis with Separation Logic.

To appear in the proceedings of
ESOP 2010.

Download PDF.

3. Alexander Barvinok, James E. Pommersheim.
An Algorithmic Theory of Lattice Points in Polyhedra.

New Perspectives in Algebraic Combinatorics, MSRI Publications, 38, 1999, 91-147.

Download PS.

4. Matthias Beck, Sinai Robbins. Computing the Continuous Discretely.

Springer-Verlag, 2007.

Link.

5. David Aspinall, Robert Atkey, Kenneth MacKenzie and Don Sannella.
Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode.

To appear in the Proceedings of TGC 2010.

Download PDF.