Modes

RaML has two major modes of operation: analysis and evaluation.

1) Analysis

In analysis mode, RaML performs the automatic resource bound analysis. It outputs the bounds in form of coefficients of resource polynomials and in a simplified form where the bound is described as a polynomial in the inputs.

To analyze a program, the user has to specify a resource metric and a maximal degree of the bounds in the search space.

The standard analysis mode is the main mode. It computes a bound on resource cost of the evaluation of the last expression in the input (main expression). RaML assumes that the main expression has the form

let _ = e or e

RaML provides the option to print the resource-usage information of the functions that have been used in the main expression. RaML prints one resource-annotated function type per function call. In the web interface, RaML prints all annotated types that correspond to function calls up to depth 2 in the syntax tree.

In the module mode, RaML infers a resource bound for every top-level function in the input file. For a function that has higher-order arguments, we assume that the resource cost of calling these functions is zero. The idea is, that the resulting bound describes the cost of the higher-order function itself.

2) Evaluation

In evaluation mode, the last expression in the file (main expression) is evaluated using our resource-accounting operational big-step semantics. Again, RaML assumes that this expression is given in the form

let _ = e or e

RaML prints the result of the evaluation. It also measures and prints the resource cost as defined by the three built-in metrics heap, steps, and ticks.

Analysis modes

RaML has three analysis modes: upper bounds, lower bounds, and constant resource. The upper-bound mode derives an upper bounds on the worst-case resource behavior. The lower-bound mode derives a lower-bound on the best-case resource behavior. Finally, the constant resource mode checks if the resource consumption for a given input size is constant.

Metrics

The resource usage of input programs is defined by resource metrics that assign a constant cost to each step in the big-step operational semantics. The resource bound analysis is parametric in these metrics. Metrics can be selected in the metric drop-down menu in the web interface. There are three built-in metrics:

  • Evaluation steps: number of steps in the big-step semantics
  • Heap space: number of allocated heap cells
  • Ticks: sum of evaluated tick commands

The tick metric allows the user to define a custom resource metric by annotating the code with tick commands, such as Raml.tick(1.3). This expression defines a resource usage of 1.3 resource units whenever the expression is evaluated. The argument of Raml.tick is a floating point number. A negative number expresses that resources are returned. The result type of Raml.tick is unit.

Degree

For an effective analysis we have to limit the search space for the bounds by selecting a maximal degree of the derived polynomials. The degree can be selected in the respective drop-down menu. If the selected degree is n then RaML is only able to find bounds of maximal degree n. However, RaML is still able to, for example, find a quadratic bound, even if the maximal degree is 3.

If the degree is too low then the generated linear program does not have a solution and RaML will report that it was not able to find a bound.

Known Issues

Strings and Integers

Strings and integers are currently not supported. Please use integer lists and natural numbers (see raml_runtime/rnat.ml).

Built-in equality

Built-in equality is only supported for ground types such as integer, bool and float. Therefore is not possible to use equality in a polymorphic function. Fix: Add type annotations or make equality a function parameter.

Exceptions

Exceptions are currently (version 1.3) broken for the constant resource usage and lower bound analysis.