CMU-CS-23-140
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-23-140

The Theory and Implementation of Resource Aware ML 2

Ethan Chu

M.S. Thesis

December 2023

CMU-CS-23-140.pdf


Keywords: Amortized Analysis, Resource Analysis, Type System, Linear Programming

Resource Aware ML (RaML) is a tool that can compute the resource use of programs in the ML family (SML, OCaml, etc) through a type-based technique known as automatic amortized resource analysis (AARA). Existing implementations of RaML have numerous shortcomings, such as lacking support for regular recursive types and being difficult to maintain.

This thesis presents the theory and implementation of a new and improved version of RaML, Resource Aware ML 2. Using work by Grosen et al, RaML 2 can analyze programs with regular recursive types, non-monotone resource analysis, and more. Furthermore, it presents the univariate AARA theory that the implementation is based on; univariate AARA's expressive power is a subset of Grosen et al's multivariate AARA, but it is still a unique variant.

Additionally, this thesis presents supporting features for a full RaML implementation. This includes a new Intermediate Representation (IR) that the resource analysis operates on; this IR is implemented efficiently with an infrastructure known as Abstract Binding Trees. Other contributions include an SML frontend implementation that can translate arbitrary SML code to the RaML IR, as well as a linear programming solver backend.

71 pages

Thesis Committee:
Jan Hoffmann (Chair)
Frank Pfenning

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science


Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu