Computer Science Thesis Proposal
— 2:00pm
Location:
In Person and Virtual - ET
-
Reddy Conference Room, Gates Hillman 4405 and Zoom
Speaker:
DAVID KAHN
,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~davidkah/
Leveraging Linearity to Improve Automatic Amortized Resource Analysis
To reason about more complex resource usage, existing tools for the verification of a program’s cost bounds often require a (dis)proportional amount of additional user-guidance. Ideally, cost bounds could be provided in the same lightweight, automatic manner as a program’s type information, at least for “natural” programs that do not run afoul of decidability. Automatic Amortized Resource Analysis (AARA) aims to provide exactly such cost information by automatically and efficiently measuring polynomial resource usage through the type system itself, using types to apply the physicist’s method of amortized cost analysis. While this approach has enjoyed some success so far, it is not hard to find natural program patterns that confound its practical and theoretical capabilities.
This thesis presents a variety of modifications to the AARA type system that allow it to overcome such stumbling blocks while still maintaining a high degree of automatability, and does so by leveraging the intrinsic linearity of both the approach and the problem. To start, we upgrade the type system’s infrastructure with the new feature of remainder contexts to allow the typing rules to better track resource reuse. We then enlarge the class of bounding functions AARA can reason about to include any functions with a basis given by linear recurrence; in particular we introduce exponential functions, which allow for bounding the resource usage of programs with more than one recursive call.
Finally we describe a refinement of the physicist’s method of amortized cost analysis called the quantum physicist’s method, which significantly improves reasoning about resource allocation and reuse, while also allowing for cost bounds to depend on the depth of trees. For future work, we propose the following: 1) Extending the work on exponential bounds to the multivariate setting. This extension would allow exponential bounds to coexist with the multivariate bounds currently inferred by AARA’s state-of-the-art typechecker RaML. We could also show that exponential potential is sound for trees. 2) Investigating the use of linear maps to generalize AARA types. These maps would replace the feature of cost-free types, which are critical for supporting various language features, including parallel execution, logarithmic and multivariate cost bounds, and the typing of non-tail-recursive functions.
Thesis Committee:
Jan Hoffmann (Chair)
Frank Pfenning
Stephanize Balzer
Tom Reps (University of Wisconsin)
In Person and Zoom Participation. See announcement.