Thesis Oral Defense - David Kahn

— 4:00pm

Location:
In Person - Mauldin Auditorium, Newell-Simon 1305

Speaker:
DAVID KAHN, Ph.D. Candidate, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~davidkah/

Leveraging Linearity to Improve Automatic Amortized Resource Analysis

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 costs. 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.

Unfortunately, deriving a program’s resource usage 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 resource 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 resource 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 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 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. This class of functions is further enlarged to be multivariate, allowing dependence on products of data structure sizes. 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 data structure height. 

Thesis Committee:

Jan Hoffmann (Chair)
Frank Pfenning
Stephanie Balzer
Thomas Reps (University of Wisconsin)

In Person and Zoom Participation. See announcement.

Event Website:
https://csd.cmu.edu/calendar/thesis-oral-defense-david-kahn

Add event to Google
Add event to iCal