David Kahn Liveraging Linearity to Improve Automatic Amortized Resource Analysis Degree Type: Ph.D. in Computer Science Advisor(s): Jan Hoffmann Graduated: July 2024 Abstract: After correctness, the most important properties of programs concern their resource requirements, like how much time they take to run or how much memory they need. It is therefore desirable to automate the derivation of a program's resource requirements. One successful approach to such automatic derivation is the type system known as Automatic Amortized Resource Analysis (AARA). AARA finds polynomial bounds on resource usage by using its types to apply the physicist's method of amortized cost analysis. Type inference in AARA can be reduced to linear programming, thereby automating resource analysis. This balance of expressive bounds and efficient analysis has brought AARA success in analyzing various programs of interest.Unfortunately, deriving a program's resource usage (i.e., costs) can be difficult-in fact it is generally not computable. Thus, despite AARA's success, it is not surprising that there are many natural program patterns that it cannot analyze well. Sometimes AARA finds loose cost bounds, other times it finds bounds slowly, and sometimes it cannot find any bounds at all.This thesis addresses such shortcomings by developing a variety of upgrades to the AARA type system that allow the efficient derivation of tight cost bounds for more programs. The key theme underlying these upgrades is the leveraging of linear reasoning principles. These ideas integrate well with AARA because AARA exists in the intersection of various forms of linearity: the linear flavor of its type system, the linear relations of its cost bound templates, and the linear physicality behind the physicist's method of amortized cost analysis.This work first upgrades the type system's infrastructure with remainder contexts to better reason about reusable resources like memory. Then the class of AARA's bounding functions is enlarged to include, e.g., exponential bounds, which can provide resource bounds for programs with multiple recursive calls. This class of functions is further enlarged to be multivariate, allowing dependence on products of data structure sizes, which is critical for analyzing functions with accumulators. Next, this work provides a more efficient, matrix-based approach to inferring the cost-free AARA types needed for, e.g., non-tail recursion. Finally the physicist's method of amortized cost analysis is refined into the quantum physicist's method, which provides an automatable framework for reasoning about resource reallocation, while also allowing resource bounds to depend on the height of data structures.Each of these upgrades is proven sound with respect to an operational cost semantics, and various implementations are made to empirically evaluate their efficacy. Thesis Committee: Jan Hoffmann (Chair) Stephanie Balzer Frank Pfenning Thomas Reps (University of Wisconsin) Srinivasan Seshan, Head, Computer Science Department Martial Hebert, Dean, School of Computer Science Keywords: Automatic, resource, cost, linear, affine, efficient, remainder, exponential, multivariate, quantum, physicist, potential, amortized, type, functional
