Duma Rodriguez, Amortised Resource Analysis for Object-Oriented Programs
Amortised Resource Analysis for Object-Oriented Programs
As software systems grow in size and complexity, the need for verifying some of their properties increases. One important property to be verified is the resource usage, where resources include execution time, memory, power, etc. Resource usage analysis is important in many areas, in particular embedded systems and cloud computing.
Resource Aware JAva (RAJA) is a type system for heap-space analysis of object-oriented programs, based on the amortised analysis technique. In this talk 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 like insertion sort and merge sort and also programs that contain different interacting objects that describe real-life scenarios such as a bank account. Some of the programs consist of hundreds of lines of code and they could be analysed within a few seconds.
We also present a type checking algorithm for the RAJA system that is useful for verifying the types discovered by the type inference.