Hoffmann, Jan (2011): Types with potential: polynomial resource bounds via automatic amortized analysis. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics 

PDF
Hoffmann_Jan.pdf 2097Kb 
Abstract
A primary feature of a computer program is its quantitative performance characteristics: the amount of resources such as time, memory, and power the program needs to perform its task. Concrete resource bounds for specific hardware have many important applications in software development but their manual determination is tedious and errorprone. This dissertation studies the problem of automatically determining concrete worstcase bounds on the quantitative resource consumption of functional programs. Traditionally, automatic resource analyses are based on recurrence relations. The difficulty of both extracting and solving recurrence relations has led to the development of typebased resource analyses that are compositional, modular, and formally verifiable. However, existing automatic analyses based on amortization or sized types can only compute bounds that are linear in the sizes of the arguments of a function. This work presents a novel type system that derives polynomial bounds from firstorder functional programs. As pioneered by Hofmann and Jost for linear bounds, it relies on the potential method of amortized analysis. Types are annotated with multivariate resource polynomials, a rich class of functions that generalize nonnegative linear combinations of binomial coefficients. The main theorem states that type derivations establish resource bounds that are sound with respect to the resourceconsumption of programs which is formalized by a bigstep operational semantics. Simple local type rules allow for an efficient inference algorithm for the type annotations which relies on linear constraint solving only. This gives rise to an analysis system that is fully automatic if a maximal degree of the bounding polynomials is given. The analysis is generic in the resource of interest and can derive bounds on time and space usage. The bounds are naturally closed under composition and eventually summarized in closed, easily understood formulas. The practicability of this automatic amortized analysis is verified with a publicly available implementation and a reproducible experimental evaluation. The experiments with a wide range of examples from functional programming show that the inference of the bounds only takes a couple of seconds in most cases. The derived heapspace and evaluationstep bounds are compared with the measured worstcase behavior of the programs. Most bounds are asymptotically tight, and the constant factors are close or even identical to the optimal ones. For the first time we are able to automatically and precisely analyze the resource consumption of involved programs such as quick sort for lists of lists, longest common subsequence via dynamic programming, and multiplication of a list of matrices with different, fitting dimensions.
Item Type:  Thesis (Dissertation, LMU Munich) 

Keywords:  Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis 
Subjects:  000 Computers, Information and General Reference > 004 Data processing computer science 000 Computers, Information and General Reference 
Faculties:  Faculty of Mathematics, Computer Science and Statistics 
Language:  English 
Date Accepted:  14. October 2011 
1. Referee:  Hofmann, Martin 
Persistent Identifier (URN):  urn:nbn:de:bvb:19139552 
MD5 Checksum of the PDFfile:  f7d3517e0e810a40e83b772b33ba9df9 
Signature of the printed copy:  0001/UMC 20055 
ID Code:  13955 
Deposited On:  20. Feb 2012 14:31 
Last Modified:  16. Oct 2012 08:58 