PrevNext

3. Worked Examples of Hume Resource Analysis

In this section we present several worked examples of using the resource analysis, thereby showing various aspects of the analysis.

3.1. Integer Examples

The resource analysis attaches cost information to constructors of data types in the program. For programs iterating over integers this basic design is not sufficient because integers have no constructors. The workaround is to use the flag --ap, which attaches size information to integers in the program and propagates this information. To work properly it must be guaranteed that the integers, over which iterations are performed, are never negative. Section 5.2 discusses safety issues realted to this option.

Another important issue to consider is that the integer variable, over which iteration is performed should always count down so that the analysis can find a bound. This might require some restructuring of the code, as in the following example, where an explicit counter z is introduced for this purpose. 


type num = int 16;

gcd' :: num -> num -> num -> num;
gcd' x y z = if (y==1)
               then x
               else gcd' y (x mod y) (z-1);

gcd :: num -> num -> num;
gcd x y = if (x < y)
            then gcd' y x y
            else gcd' x y x;

For the straightforward gcd computation above we get the heap bound below, after typing phamc-an -H -r gcd12.hume > gcd12.art3 and art3 -H --ap --speak gcd12.art3 


ARTHUR3 typing for HumeHeapBoxed:
0, (int<10> -&-> int<10>) -(8/2)-> int ,0
Worst-case Heap-units required in relation to input:
8 + 10*Z1 + 10*Z2
  where
      Z1 = runtime value of the 1. NTint 
      Z2 = runtime value of the 2. NTint

3.2. List Examples

Consider the following simple list reversal function (available in the examples of the distribution as ra16.hume). 


type num = int 16;

data num_list = Nil | Cons num num_list;

revApp :: num_list -> num_list  -> num_list;
revApp acc Nil = acc;
revApp acc (Cons x xs) = revApp (Cons x acc) xs;

reverse :: num_list  -> num_list;
reverse xs = revApp Nil xs;

expression reverse;

The first step is to generate Schopenhauer code from the Hume code. This is done like this: phamc-an -H -r ra16.hume > ra16.art3

The second step is to run the resource analysis, proper, on the Schopenhauer code, like this: art3 -H --speak ra16.art3

The result of the analysis will be an annotated type, encoding resource information, together with an explanation: 


ARTHUR3 typing for HumeHeapBoxed:
 0, (num_list[Nil|Cons<4>:int,#]) -(2/0)-> num_list[Nil|Cons:int,#] ,0

Worst-case Heap-units required in relation to input:
2 + 4*X1
  where
      X1 = number of "Cons" nodes at 1. position

In this example the heap consumption is linear in the input list: if the input list has n elements, heap consumption will be 2 + 4*n.

3.3. Operations on Trees

3.3.1. Insertion into a Red-Black Tree

The resource bounds inferred by our analysis are in general data-dependent and we demonstrate this strength on a standard textbook example of insertion into a red-black tree. The following code is taken from Okasaki's textbook. 


program -- RedBlack

type num = int 16;
data colour = Red | Black;
data tree = Empty | Node colour tree num tree;

balance :: colour -> tree -> num -> tree -> tree;
balance Black (Node Red (Node Red a x b) y c) z d = Node Red (Node Black a x b) y (Node Black c z d);
balance Black (Node Red a x (Node Red b y c)) z d = Node Red (Node Black a x b) y (Node Black c z d);
balance Black a x (Node Red (Node Red b y c) z d) = Node Red (Node Black a x b) y (Node Black c z d);
balance Black a x (Node Red b y (Node Red c z d)) = Node Red (Node Black a x b) y (Node Black c z d);
balance c a x b = Node c a x b;

ins :: num -> tree -> tree;
ins x Empty = Node Red Empty x Empty;
ins x (Node col a y b) = if (x < y) 
                           then balance col (ins x a) y b
                         else if (x>y)
                           then balance col a y (ins x b)
                         else (Node col a y b);

insert :: num -> tree -> tree;
insert x t = case ins x t of
                (Node _ a y b) -> Node Black a y b;


expression insert;

A red-black tree is a binary search tree, in which nodes are coloured red or black. With the help of these colours, invariants can be formulated that guarantee that a tree is roughly balanced. The invariants are that on each path no red node is followed by another red node, and that the number of black nodes is the same on all paths. These invariants guarantee that the lengths of any two paths in the tree differs by at most a factor of two. This loose balancing constraint has the benefit that all balancing operations in the tree can be done locally. The balance function only has to look at the local pattern and restructure the tree if a red-red violation is found. The insert function in the above code performs the usual binary tree search, finally inserting the node as a red node in the tree, if it does not already exist in the tree, and balancing all trees in the path down to the inserted node.

In a first step we translate the Hume program into a Schopenhauer program, using the command phamc-an -H -r redblack11.hume > redblack11.art3. The program in redblack11.art3 is the one we analyse in the following steps.

To infer the heap bound for the insert function we use the command art3 -H --noapisolve --oldarity redblack11.art3. The important option is -H for "heap bound". The following 2 options make the output slightly easier to read but can be omitted in general: --noapisolve in this case avoids floating point numbers in the annotated type, and --oldarity does not distinguish between two forms of function arrows. All available options are discussed in the art3 manual. The result of the heap analysis is:


ARTHUR3 typing for HumeHeapBoxed:
  0, (int,tree[Empty<20>|Node<18>:colour[Red|Black<10>],#,int,#]) -(0/0)-> tree[Empty|Node:colour[Red|Black],#,int,#] ,0

This bound expresses that the total heap consumption of the function is 10 n + 18 b + 20, where the n is the number of nodes in the tree, and b is the number of black nodes in the tree. The latter demonstrates how our analysis is able to produce data-dependent bounds by attaching annotations to constructors of the input structure. This gives a more precise formula compared to one that only refers to the size of the input structure. In this example the 18 b part of the formula reflects the costs of applying the balance function, which restructures a sub-tree with a black root in the case of a red-red violation. The analysis assumes a worst-case, where every black node is affected by a balancing operation. Note that, due to the above invariants, this cannot occur for a well-formed red-black tree: any insertion into the tree will trigger at most 2 balancing operations (see Chapter 13 of Cormen, Leiserson, Rivest, Stein's textbook). As expected, capturing these (semantic) constraints is beyond the power of our type system.

In Section Section 4.1.1 we will revisit this example and show how to get even better analysis results for its heap consumption.

The stack bound for the insert function, inferred by our analysis is (using the command art3 -S --noapisolve --oldarity redblack11.art3): 


ARTHUR3 typing for HumeStackBoxed:
 7, (int,tree[Empty<8>|Node<13>:colour[Red|Black],#,int,#]) -(14/18)-> tree[Empty|Node<2>:colour[Red|Black],#,int,#] ,6

Similarly the time bound for the insert function associates costs to the black nodes in the input tree (using the command art3 -T --noapisolve --oldarity redblack11.art3): 


ARTHUR3 typing for HumeTimeM32:
 298, (int,tree[Empty<2288>|Node<3010>:colour[Red|Black<1830>],#,int,#]) -(474/0)-> tree[Empty|Node:colour[Red|Black],#,int,#] ,0

Finally, the call count analysis for insert, using the command art3 --RK CC --noapisolve -- oldarity redblack11.art3, yields: 


ARTHUR3 typing for CallCount:
 0, (int,tree[Empty|Node<2>:colour[Red|Black],#,int,#]) -(1/0)-> tree[Empty|Node:colour[Red|Black],#,int,#] ,0

This type encodes a bound of 2 n +1, where n is the number of nodes. By attaching costs to the constructors of the input it is possible to distinguish between nodes and leaves. However, it is currently not possible to express the fact that in the tree traversal the number of nodes visited on each path is at most log n. In the extension of the amortised cost based analysis, developed by Campbell in his PhD Thesis, such information on the depth of data structures is available, and his system is able to infer logarithmic bounds on space consumption for such examples.

3.4. Box-level examples

Resource analysis of box-leve code proceeds in the same way as analysis of expression-level code. In particular, resources are encoded as numeric annotations attached to the input wires of a box. One important difference to the expression level is that on box level an input may not be available at all. This is reflected in the elaboration of the inferred type.

3.4.1. Multiplication by recursion

The following example realises a box calculating the product of two integer numbers. The first version performs the entire calculation on expression level, using a recursive function mult that multiplies two numbers using an accumulating parameter as first argument. 


program -- recmult

-- stream stdin  from "std_in";
stream stdout to "std_out";

type integer = int 64;

mult :: integer -> integer -> integer -> integer;
mult r x 0 = r;
mult r x y = mult (r+x) x (y-1);

box mult_box
in  (i :: integer)
out (i' :: integer, o :: integer)
match
 (x) -> (x+1, mult 0 x x);

wire mult_box (mult_box.i' initially 0) (mult_box.i, stdout);

We analyse the time consumption of this program by first converting the code into Schopenhauer code, using phamc-an -H -r recmult.hume > recmult.art3, and then calling the analysis like this art3 -T --ap --shrtcon --speak recmult.art3. The output of the analysis is: 


ARTHUR3 typing for HumeTimeM32:
  
@BOX mult_box:
    mult_box.i: wire[W<1308>:int<828>|NOVAL]
  ---137/0---> 
    mult_box.i':
                wire[W:int|NOVAL]
    mult_box.o: wire[W:int|NOVAL]
Worst-case Time-units required to compute box mult_box once in relation to its input:
  137 + 1308*X1 + 828*Z2
    where
        X1 = one if 1. wire is live, zero if the wire is void
        Z2 = runtime value of the 1. NTint

First of all, with the help of the --ap option, it is possible to infer a bound on the overall time consumption. The bound delieverd has three components: a fixed cost of 137, an optional cost of 1308, which is incurred only if an input is available on the first argument, representing the accumulating parameter, and finally a linear component (828) in terms of the value of the second component, over which the recursion is performed.

We can check the concrete time consumption of the mult, without the overhead on box level, by using the additional option --jfun to the analysis (art3 -T --ap --shrtcon --speak --jfun recmult.art3). This will deliever resource bounds for all functions in the code: 


ARTHUR3 typing for HumeTimeM32:
mult_LIFTED: (int -&-> int -&-> int<854>) -(544/0)-> wire[W:int|NOVAL]
 
Worst-case Time-units required to call mult_LIFTED in relation to its input:
  544 + 854*Z1
    where
        Z1 = runtime value of the 3. NTint

3.4.2. Multiplication by iteration

As a second version we examine the resource consumption of box-level implementation of multiplication. In this version, we use 2 boxes: the mult_box sets up the computation, by initialising the three input wires of the itermult box; the latter performs only one iteration of multiplication, using its fourth input and its first output wire for accumulating the result. First we call phamc-an -H -r itermult.hume > itermult.art3. 


program -- itermult

type integer = int 64;

stream output to "std_out";

-- controls input stream (x) feeding input vals (0,x,x) to itermult box
-- sending result (r) to output, once it's returned from itermult
box mult2
in  (i::integer,  iter'::integer)
out (i'::integer, iter1 ::integer, iter2 ::integer, iter3 ::integer, r::integer)
match
(x,r) -> (x+1,0,x,x,r);

-- computing (*,x,y,*,*,*,*) -> x*y, 
-- using the last 3 inputs and first 3 outputs as state via feedback wires
box itermult
in  (i1::integer, i2::integer, i3::integer, iter1::integer, iter2::integer, iter3::integer)
out (iter1'::integer, iter2'::integer, iter3'::integer, r::integer)
match
 (r,x,y,*,*,*) -> (r,x,y,*) |
 (*,*,*,r,x,0) -> (*,*,*,r) |
 (*,*,*,r,x,y) -> (r+x, x, y-1, *);

wire mult2 
 (mult2.i' initially 0,itermult.r)
 (mult2.i,itermult.i1,itermult.i2,itermult.i3,output);

wire itermult 
 (mult2.iter1,mult2.iter2,mult2.iter3,itermult.iter1',itermult.iter2',itermult.iter3') 
 (itermult.iter1,itermult.iter2,itermult.iter3,mult2.iter');

We analyse the time consumption of this code by calling art3 -T --ap --shrtcon --speak itermult.art3 . 


ARTHUR3 typing for HumeTimeM32:
  
@BOX mult2:
    mult2.i:    wire[W<1034>:int|NOVAL]
    mult2.iter':
                wire[W:int|NOVAL]
  ---211/0---> 
    mult2.i':   wire[W:int|NOVAL]
    mult2.iter1:
                wire[W:int<ANY>|NOVAL]
    mult2.iter2:
                wire[W:int|NOVAL]
    mult2.iter3:
                wire[W:int|NOVAL]
    mult2.r:    wire[W:int|NOVAL]
Worst-case Time-units required to compute box mult2 once in relation to its input:
  211 + 1034*X1
    where
        X1 = one if 1. wire is live, zero if the wire is void
   

ARTHUR3 typing for HumeTimeM32:
  
@BOX itermult:
    itermult.i1:
                wire[W:int|NOVAL]
    itermult.i2:
                wire[W:int|NOVAL]
    itermult.i3:
                wire[W:int|NOVAL]
    itermult.iter1:
                wire[W<859>:int|NOVAL]
    itermult.iter2:
                wire[W:int|NOVAL]
    itermult.iter3:
                wire[W:int|NOVAL]
  ---1322/0---> 
    itermult.iter1':
                wire[W:int|NOVAL]
    itermult.iter2':
                wire[W:int|NOVAL]
    itermult.iter3':
                wire[W:int|NOVAL]
    itermult.r: wire[W<687>:int|NOVAL]
Worst-case Time-units required to compute box itermult once in relation to its input:
  1322 + 859*X1
    where
        X1 = one if 4. wire is live, zero if the wire is void

As expected, the time bound for the itermult box is now fixed, not depending on an input value but only on the availability of data along the fourth input wire, which holds the accumulated result.

3.4.3. Vending machine


type cash = int 8;

type _smallint = int 16;
type _int = int 32;

data coins =  Nickel | Dime;
data drinks = Coffee | Tea;
data buttons = BCoffee | BTea | BCancel;

showdrink :: drinks -> char;
showdrink Coffee = 'C';
showdrink Tea = 'T';

vend :: drinks -> cash -> cash -> (drinks, cash, cash);
vend drink cost v = 
   if v >= cost then
        ( drink, v-cost, * ) 
   else ( *,     v,      * );

-- input handling box

box inp
in ( c :: char )
out ( coin :: coins, button :: buttons )
match
    'N' -> ( Nickel, * )
  | 'D' -> ( Dime,   * )
  | 'C' -> ( *,      BCoffee )
  | 'T' -> ( *,      BTea )
  | 'X' -> ( *,      BCancel )
  | _   -> ( *,      * )
  ;

-- vending machine control box
box control
in  ( coin :: coins, button :: buttons, value :: cash )
out ( drink :: drinks, value' :: cash,  return :: cash )
match
    ( Nickel, *,  v )  ->  ( *, v + 5, * )
  | ( Dime,   *,  v )  ->  ( *, v + 10, * )
  | ( *, BCoffee, v )  ->  vend Coffee 10 v
  | ( *, BTea,    v )  ->  vend Tea 5 v
  | ( *, BCancel, v )  ->  ( *, 0, v )
  ;

box outp
in ( drink :: drinks, return :: cash )
out (d :: char, r :: cash) -- s :: string 15)
match
  ( d, * ) -> (showdrink d, *) -- "Vending " ++ showdrink d ++ "\n"
| ( *, r ) -> (* , r)          -- "Returning " ++ r as string ++ "\n"
;

stream stdout to "std_out";
stream stderr to "std_err";
stream stdin  from "std_in";

wire inp    ( stdin )                          ( control.coin, control.button );
wire control ( inp.coin, inp.button, control.value' initially 0 )( outp.drink,  control.value, outp.return );
wire outp   ( control.drink, control.return )  ( stdout, stderr );

We will now illustrate Hume with a simple, but more realistic, example from the reactive systems literature, suggested to us at CEFP 2005 by Pieter Koopman: the control logic for a simple vending machine. A system diagram is shown in the figure above. We will show Hume code only for the most important part of the system: the control box. This box responds to inputs from the keypad box and the cash holder box representing presses of a button (for tea, coffee, or a refund) or coins (nickels/dimes) being loaded into the cash box. In a real system, these boxes would probably be implemented as hardware components. If a drinks button (tea/coffee) is pressed, then the controller determines whether a sufficient value of coins has been deposited for the requested drink using the vend function. If so, the vending unit is instructed to produce the requested drink. Otherwise, the button press is ignored. If the cancel button is pressed, then the cash box is instructed to refund the value of the input coins to the consumer.

First we define some basic types representing the value of coins held in the machine (Cash), the different types of coins (Coins), the drinks that can be dispensed (Drinks) and the buttons that can be pressed (Buttons).

Now we can define the control box itself. This box uses asychronous constructs to react to each of the two input possibilities: either an inserted coin or a button-press. As with the inc box, state is maintained explicity through a feedback wire: the value' output will be wired directly to the value input. For simplicity, the box uses unfair matching, which will prioritise coin inputs over simultaneous button presses. If the cancel button (BCancel) is pressed, no drink will be dispensed (shown by *), but the internal cash value will be reset to zero and the cash holder instructed to refund the current value of coins held (value) through the return wire. A timeout has the same effect as explicitly pressing the cancel button.

The control box logic makes use of two auxiliary functions: vend calculates whether sufficient coins have been deposited and instructs the outp box accordingly; and showdrink displays the chosen drink as a single character. Note the use of * as a return value in the vend function: this is permitted only in positions which correspond to top-level outputs. Note also that the box corresponds to the FSM-Hume level: it uses first-order non-recursive functions as part of its definition.

Finally, we wire the control box to the other boxes shown in the system diagram.

We convert the Hume program to a Schopenhauer program: phamc-an -H -r vending.hume > vending.art3. Then we perform an analysis of the heap consumption of the program: art3 -H --shrtcon --speak vending.art3. 


ARTHUR3 typing for HumeHeapBoxed:
  
@BOX inp:
    inp.c:      wire[W<2>:char|NOVAL]
  ---0/0---> 
    inp.coin:   wire[W:coins[Nickel|Dime]|NOVAL]
    inp.button: wire[W:buttons[BCoffee|BTea|BCancel]|NOVAL]
Worst-case Heap-units required to compute box inp once in relation to its input:
  2*X1
    where
        X1 = one if 1. wire is live, zero if the wire is void
   

ARTHUR3 typing for HumeHeapBoxed:
  
@BOX control:
    control.coin:
                wire[W:coins[Nickel|Dime]|NOVAL]
    control.button:
                wire[W<4>:buttons[BCoffee|BTea|BCancel]|NOVAL]
    control.value:
                wire[W<4>:int|NOVAL]
  ---0/0---> 
    control.drink:
                wire[W:drinks[Coffee|Tea]|NOVAL]
    control.value':
                wire[W:int|NOVAL]
    control.return:
                wire[W<6>:int|NOVAL]
Worst-case Heap-units required to compute box control once in relation to its input:
  4*X1 + 4*X2
    where
        X1 = one if 2. wire is live, zero if the wire is void
        X2 = one if 3. wire is live, zero if the wire is void
   

ARTHUR3 typing for HumeHeapBoxed:
  
@BOX outp:
    outp.drink: wire[W:drinks[Coffee<2>|Tea<2>]|NOVAL]
    outp.return:
                wire[W:int|NOVAL]
  ---0/0---> 
    outp.d:     wire[W:char|NOVAL]
    outp.r:     wire[W:int|NOVAL]
Worst-case Heap-units required to compute box outp once in relation to its input:
  2*X1 + 2*X2
    where
        X1 = number of "Coffee" nodes at 1. position
        X2 = number of "Tea" nodes at 1. position

We notice that for these simple boxes the heap consumption is in all case fixed, depending only on the availability but not on the size of the input. For the outp we know that only one value, either Coffee or Tea, can be supplied, since they are 0-ary constructors of the same type. Therefore, the maximal heap consumption of the outp box is 2. Note that in the control box a value of 6 is attached to the output wire return. This indicates, that in the case of producing an output along this wire, 6 heap cells, of the maximal bound of 8, are not used, reducing the bound in this case to only 2.

PrevHomeNext
A Quick Introduction to Using the Resource Analysis for Hume Advanced Features of the Resource Analysis