# 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 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 physi?cist’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.

## Funding

### SHF: Medium: Language Support for Sound and Efficient Programmable Inference

Directorate for Computer & Information Science & Engineering

Find out more...### CAREER: Marlin: A Unified Framework for Automatic and Interactive Quantitative Program Analysis

Directorate for Computer & Information Science & Engineering

Find out more...### SaTC: CORE: Medium: Collaborative: Automated Support for Writing High-Assurance Smart Contracts

Directorate for Computer & Information Science & Engineering

Find out more...### SHF: Small: Collaborative Research: Resource-Guided Program Synthesis

Directorate for Computer & Information Science & Engineering

Find out more...### SHF: Small: Automatic Qualitative and Quantitative Verification of CUDA Code

Directorate for Computer & Information Science & Engineering

Find out more...## History

## Date

2024-07-12## Degree Type

- Dissertation

## Department

- Computer Science

## Degree Name

- Doctor of Philosophy (PhD)