Rodriguez, Dulma (2012): Amortised resource analysis for objectoriented programs. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics 

PDF
Rodriguez_Dulma.pdf 1MB 
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 objectoriented 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 objectoriented 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 objectoriented programs that complicate the analysis are aliasing and imperative update. Hofmann and Jost presented in 2006 a type system for amortised heapspace analysis of objectoriented 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 upperbounds to the heapspace 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 reallife 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.
Item Type:  Thesis (Dissertation, LMU Munich) 

Keywords:  Objectoriented, resource analysis, amortised analysis, type systems 
Subjects:  000 Computers, Information and General Reference 000 Computers, Information and General Reference > 004 Data processing computer science 
Faculties:  Faculty of Mathematics, Computer Science and Statistics 
Language:  English 
Date of oral examination:  5. October 2012 
1. Referee:  Hofmann, Martin 
MD5 Checksum of the PDFfile:  b0dcc784e8cf46e69396332b985ef48b 
Signature of the printed copy:  0001/UMC 20820 
ID Code:  14983 
Deposited On:  13. Dec 2012 14:47 
Last Modified:  20. Jul 2016 10:31 