Abstract:
Controlling resource usage is important for the reliability, efficiency and security of software systems. Automated analyses for bounding resource usage can be invaluable tools for ensuring these properties.
Hofmann and Jost have developed an automated static analysis for finding linear heap space bounds in terms of the input size for programs in a simple functional programming language. Memory requirements are amortized by representing them as a requirement for an abstract quantity, potential, which is supplied by assigning potential to data structures in proportion to their size. This assignment is represented by annotations on their types. The type system then ensures that all potential requirements can be met from the original input's potential if a set of linear constraints can be solved. Linear programming can optimise this amount of potential subject to the constraints, yielding a upper bound on the memory requirements.
However, obtaining bounds on the heap space requirements does not detect a faulty or malicious program which uses excessive stack space.
In this thesis, we investigate extending Hofmann and Jost's techniques to infer bounds on stack space usage, first by examining two approaches: using the Hofmann-Jost analysis unchanged by applying a CPS transformation to the program being analysed, then showing that this predicts the stack space requirements of the original program; and directly adapting the analysis itself, which we will show is more practical.
We then consider how to deal with the different allocation patterns stack space usage presents. In particular, the temporary nature of stack allocation leads us to a system where we calculate the total potential after evaluating an expression in terms of assignments of potential to the variables appearing in the expression as well as the result. We also show that this analysis subsumes our previous systems, and improves upon them.
We further increase the precision of the bounds inferred by noting the importance of expressing stack memory bounds in terms of the depth of data structures and by taking the maximum of the usage bounds of subexpressions. We develop an analysis which uses richer definitions of the potential calculation to allow depth and maxima to be used, albeit with a more subtle inference process.
An official copy should appear in the Edinburgh Research Archive in due course. A PDF copy is available here and should be identical. I recently presented a paper based on Chapters 4 and 5 at TFP 2008. Some material concerning the type system and inference of Chapters 6 and 7 is available, too.
Brian Campbell. 24th June 2008.