Amortised resource analysis for object-oriented programs

Rodriguez, Dulma (2012): Amortised resource analysis for object-oriented programs. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

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.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Object-oriented, resource analysis, amortised analysis, type systems
• Themengebiete: 000 Allgemeines, Informatik, Informationswissenschaft ; 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 5. Oktober 2012
• 1. Bericht­erstatter:in: Hofmann, Martin