Towards Automatic Resource Bound Analysis for OCaml

TL;DR

This paper introduces an automatic resource analysis system for OCaml that derives polynomial bounds on various resources for higher-order, polymorphic, and user-defined inductive type programs, including those with side effects.

Contribution

It presents a novel multivariate automatic amortized resource analysis (AARA) that automatically infers polynomial resource bounds for complex OCaml programs, including higher-order functions and user-defined types.

Findings

Successfully derived resource bounds for 411 functions across multiple libraries.

Outperformed previous linear bound inference systems in handling programs with side effects.

Demonstrated practical applicability with integration into OCaml compiler and case studies.

Abstract

This article presents a resource analysis system for OCaml programs. This system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and can derive bounds for time, memory allocations and energy usage. The derived bounds are multivariate resource polynomials which 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. Technically, the analysis system is based on a novel multivariate automatic amortized resource analysis (AARA). It builds on existing work on linear AARA for higher-order programs with user-defined inductive types and on multivariate AARA for first-order programs with built-in lists and binary trees. For the first time, it is possible to automatically derive polynomial bounds for higher-order functions and polynomial bounds that depend on user-defined inductive types. Moreover, the analysis handles programs with side effects and even outperforms the linear bound inference of previous systems. At the same time, it preserves the expressivity and efficiency of existing AARA techniques. The practicality of the analysis system is demonstrated with an implementation and integration with Inria's OCaml compiler. The implementation is used to automatically derive resource bounds for 411 functions and 6018 lines of code derived from OCaml libraries, the CompCert compiler, and implementations of textbook algorithms. In a case study, the system infers bounds on the number of queries that are sent by OCaml programs to DynamoDB, a commercial NoSQL cloud database service.