RaML has two major modes of operation: analysis and evaluation.
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.
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.
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.
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.
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.
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 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 are currently (version 1.3) broken for the constant resource usage and lower bound analysis.