About

Resource Aware ML (RaML) is a tool that automatically and statically computes resource-use bounds for OCaml programs.

In principle, a resource can be any quantity that is of interest to the user. We currently implemented resource metrics for the number of evaluation steps in a high-level abstract machine, allocated heap cells, and user-defined ticks executed.

The system automatically derives upper bounds on the worst-case resource use and lower bounds on the best-case resource use. Furthermore, it can determine if the resource use is constant for inputs of a given size. RaML supports higher-order, polymorphic programs with side effects and user-defined inductive types. The derived bounds are multivariate resource polynomials that are functions of different size parameters that depend on the standard OCaml types. Bound inference is fully automatic and reduced to a linear optimization problem that is passed to an off-the-shelf LP solver.

Since symbolic bound inference is an undecidable problem, RaML cannot automatically derive a bound for every program. Our goal is therefore to find bounds for most programs that appear in practice.

Contributors