Author:	Angela Yun Zhu	Date:	2007-03-17

Performance measurement on sized lists

Overview

This document is to provide an insight on performance difference between functions implemented in OCaml and in Concoqtion. Timings on a bunch of functions about list operations are examined, including:

• Reading a list vs. Reading a sized list
• Mapping function: OCaml version, OCaml Lib version and Concoqtion version
  • Map an add function
  • Map an square function
• Zip function (five version)
  • OCaml definition
  • OCaml definition using pair
  • Concoqtion definition
  • Concoqtion definition using pair
  • Concoqtion definition without refinement
• Append function: OCaml version, OCaml Lib version and Concoqtion version
• size it function: convert an OCaml list to sized list
• at size function: on list and sized list

Hardware Configuration

• PowerBook^? G4
• Mac OS X 10.4.7

Measuring Methods

To measure the performance on sized list and unsized list and compare them, here are a bunch of suggestions:

• Write the sized version and unsized version of all functions (e.g. zip, map, append) together. It will be convenient for comparation.
• About how many digits you want to keep in your final data: do the experiment several times and throw away those that are varying each time. For example, if you get the time for running function "f" measured as 1.21, 1.23, 1.22. You might want to keep it as 1.2.
• We might be more interested in the time ratio. You can have all your time normalized to either unsized one or sized one.
  • Daniel: What if the ratio is not varying but the actual data varies from time to time. Like you can have the run time for (unsized_f, sized_f) be (1.2, 1.4), (1.3, 1.5), (1.4, 1.7) ....
  • Walid: That could happen, and ...
• We are also more interested in significant speed ratio. If we have one always 10 times faster than the another one, then the varying of individual measurement does not matter much.
• Because of the experiment context, it will also be good to just look at the MINIMUM cycles needed to run the function. In this way, you can get rid of some setup factors like OS processes.
• Be careful and specific on what you are testing for. Like in the function zip, like we wrote the pattern matching in a way that we first pair the l1 and l2, then do the matching. But pairing will cause a lot overhead. We might want to write aother match to avoid doing the pairing.
• Also pay attention to the space cost. Sometimes by using optimization like "memorization" you can get benifit for the speed, i.e. you are trading off space for speed. This is also sensiable and sometime might be thought unfair. You need to be clear about space overhead when necessary.

Source Code

(***********************************************
*     Angela Yun Zhu                           *
*     RAP, CS Dept, Rice Univ.                 *
*     2007, February 2rd                       *
*     Seminar 617 Homework                     *
*     Concoqtion implementation of Sized list  *
************************************************)

type ('n:'(nat), 'a) listl =
  | Nil : ('(0), 'a) listl
  | Cons of let 'm:'(nat) in 'a * ('(m), 'a) listl: ('(1+m), 'a) listl
  ;;

(* map function on unsized list *)
let rec map_u f l =
    match l with 
   | [] -> []
    | x::xs -> (f x)::(map_u f xs)
;;

(* map function on sized list *)
let rec mapl .|n:'(nat)| (f: 'a -> 'b) (l: ('(n), 'a) listl)
    : (('(n), 'b) listl) =
    match l in ('(n), 'b) listl with
   | Nil -> Nil
   | Cons .|m:'(nat)| (x, xs) ->
     Cons .|'(m)| (f x, mapl .|'(m)| f xs) 
;;


exception UNSIZED_EXN;;

(* zip function on unsized list *)
let rec zip_u l1 l2 = match l1 with
   | [] -> (match l2 with | [] -> []
                | y::ys -> raise UNSIZED_EXN)
   | x::xs -> (match l2 with | [] -> raise UNSIZED_EXN
                | y::ys -> (x,y)::(zip_u xs ys))
;;

(* zip function on unsized list using pair *)
let rec zip_pair l1 l2 = match (l1,l2) with
   | ([],[]) -> []
   | (x::xs, y::ys) -> (x,y)::(zip_u xs ys)   
   | _ -> raise UNSIZED_EXN
;;

(* zip function on sized list *)
let rec zipl .|n:'(nat)| (l1: ('(n), 'a) listl) (l2:('(n), 'b) listl)
    : (('(n), ('a * 'b)) listl) =
match l1 in ('(n), 'a * 'b) listl with 
    | Nil -> (match l2 in ('(n), 'a * 'b) listl with
      | Nil -> Nil)
    |  Cons .|i:'(nat)| (x, xs) -> (match l2 in ('(n), 'a * 'b) listl with
      | Cons .|j:'(nat)| (y, ys)  -> Cons .|'(j)| ((x,y), zipl .|'(i)| xs ys))
;;

(* zip function on sized list using pair *)
let rec zipl_pair .|n:'(nat)| (l1: ('(n), 'a) listl) (l2:('(n), 'b) listl)
    : (('(n), ('a * 'b)) listl) =
match (l1, l2) in ('(n), 'a * 'b) listl with 
    | (Nil, Nil) -> Nil
    | Cons .|i:'(nat)| (x, xs), Cons .|j:'(nat)| (y, ys)  -> Cons .|'(j)| ((x,y), zipl .|'(i)| xs ys)
;;


coq
    Require Export Arith.
        Require Omega.
        Lemma pred_eq : forall m n, (S m) = (S n) -> (m=n). intros; omega. Qed.
end

let cast .|m:'(nat),n:'(nat),p:'(m=n)| (x: ('(m), 'a) listl) : ('(n), 'a) listl =
  Obj.magic x
;;

(* zip function on sized list without refinement *)
let rec  zip_comp .|n:'(nat)| (xs:('(n), 'a) listl) (ys:('(n), 'b) listl) : ('(n), 'a * 'b) listl =
  (match xs,ys as ('i:'(nat), 'a) listl * ('j:'(nat), 'b) listl in forall p:'(i=j). unit -> ('(j), ('(a) * '(b))) listl with
        | Nil, Nil -> /\p:'(0=0). fun () -> Nil
        | Cons .|i1:'(nat)| (x,xs), Cons .|j1:'(nat)| (y,ys) ->  /\p:'(i1=j1). fun () ->
                let xs' = cast .|'(i1),'(j1),'(p)| xs in
                let r = zip_comp .|'(j1)| xs' ys in
                Cons .|'(j1)| ((x,y), r)) .|'(refl_equal n)| ()
;;

(* append function on unsized list *)
let rec app_u l1 l2 =
    match l1 with 
   | [] -> l2
   | x::xs -> x::(app_u xs l2)
;;

(* append function on sized list *)
let rec appl .|m:'(nat), n:'(nat)| (l1: ('(m), _) listl) (l2: ('(n), _) listl)
    : ('(m+n), _) listl =
   match l1 as ('i: '(nat), 'a: '(OCamlType)) listl 
     in ('(i+n), '(a)) listl with
   | Nil -> l2
   | Cons .|m2:'(nat)| (x, xs) ->
     Cons .|'(m2+n)| (x, appl .|'(m2), '(n)| xs l2)
;;


type 'a exist_size = EX of let 'n:'(nat) in (('(n), 'a) listl);;

let rec size_it (l: 'a list) : ('a exist_size) =
    match l as ('a list) in ('a exist_size) with
   | [] -> EX .|'(0)| (Nil)
   | x::xs -> let xsl = (size_it xs) in
      (match xsl as 'a exist_size in 'a exist_size 
         with | EX .|m:'(nat)| y -> EX .|'(1+m)| (Cons .|'(m)| (x, y)));;
(***************************************************
 val size_it : 'a list -> 'a exist_size = <fun>
*************************************************)

type 'a option = 
      | None
      | Some of 'a ;;
(***************************************************
type 'a:'(OCamlType) option = None:'a option | Some of   'a : 'a option
*************************************************)

(* take first n elements of an unsized list and return a sized list *)
let rec at_size_u (l:'a list) (n:int) = 
    if n=0 then [] else
    (match l with 
   | [] -> raise UNSIZED_EXN
   | x::xs -> x::(at_size_u xs (n-1)))
;;

(* take first n elements of a sized list and return a sized list *)
let rec at_size (l: 'a list) (n: int) : ('a exist_size) option =
    match (l, n) as ('a list * int) in ('a exist_size) option with
   | (_, 0) -> Some (EX .|'(0)| Nil)
   | ([], m) -> None
   | (x::xs, m) -> let ls = at_size xs (n-1) in
   (match ls as ('a exist_size) option in ('a exist_size) option with
   | None -> None
   | Some (EX .|k:'(nat)| y) -> Some (EX .|'(1+k)| (Cons .|'(k)| (x, y)))
   );;

Experimental Data

let l1 = [0;1;2;3;4;5;6;7;8;9];;

let ll1 = Cons .|'(9)| (0,  Cons .|'(8)| (1,  Cons .|'(7)| (2,  Cons .|'(6)| (3,  Cons .|'(5)| (4,  Cons .|'(4)| (5,  Cons .|'(3)| (6,  Cons .|'(2)| (7,  Cons .|'(1)| (8,  Cons .|'(0)| (9, Nil))))))))));;

let add x = x + x;;
let square x = x * x;;

let id l = l;;

let iter_10_run f = (f;f;f;f;f;f;f;f;f;f);;

let iter_100_run f = ((iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f);(iter_10_run f));;

let iter_1000_run f = ((iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f);(iter_100_run f));;

(* Change here to get different running times *)
let iter_run f = iter_10_run f;;

Trx.init_times ();;
Trx.timenew "list_Normal" (fun () -> iter_run l1);;
Trx.timenew "list_Sized"  (fun () -> iter_run ll1);;
Trx.timenew "map_add_Normal"  (fun () -> iter_run (map_u add l1));;
Trx.timenew "map_add_Normal_lib"  (fun () -> iter_run (List.map add l1));;
Trx.timenew "map_add_Sized"   (fun () -> iter_run (mapl .|'(10)| add ll1));;
Trx.timenew "map_square_Normal"  (fun () -> iter_run (map_u square l1));;
Trx.timenew "map_square_Normal_lib"  (fun () -> iter_run (List.map square l1));;
Trx.timenew "map_square_Sized"   (fun () -> iter_run (mapl .|'(10)| square ll1));;
Trx.timenew "zip_Normal"  (fun () -> iter_run (zip_u l1 l1));;
Trx.timenew "zip_Sized"   (fun () -> iter_run (zipl .|'(10)| ll1 ll1));;
Trx.timenew "zip_Unrefined"   (fun () -> iter_run (zip_comp .|'(10)| ll1 ll1));;
Trx.timenew "zip_usePair"   (fun () -> iter_run (zip_pair .|'(10)| ll1 ll1));;
Trx.timenew "append_Normal"  (fun () -> iter_run (app_u l1 l1));;
Trx.timenew "append_Normal_lib"  (fun () -> iter_run (List.append l1 l1));;
Trx.timenew "append_Sized"   (fun () -> iter_run  (appl .|'(10), '(10)| ll1 ll1));;
Trx.timenew "Size_it"  (fun () -> iter_run  (size_it l1));;
Trx.timenew "at_size_Normal"  (fun () -> iter_run  (at_size_u l1 5));;
(*Trx.timenew "at_size_Normal"  (fun () -> try iter_run  (at_size_u l1 5) with _ -> []);;*)
Trx.timenew "at_size_Sized"   (fun () -> iter_run  (at_size l1 5));;

Trx.print_times ();;

Experimental results

Average on 10*100 iterations

E-08 seconds	UnSized_id	Sized_id	Map_Add_Un	Map_Add_Lib	Map_Add_Size	Map_Square_Un	Map_Square_Lib	Map_Square_Size	Size_it
Time	3.64	3.67	8.93	9.73	9.00	8.90	9.70	8.98	7.81
Nromalized	1	0.99	1	1.09	1.01	1	1.09	1.01	-

E-08 seconds	Zip_Unsized	Zip_U_Pair	Zip_Sized	Zip_S_Pair	Zip_S_unrefine	Append_Unsized	Apeed_Un_Lib	Append_Sized	at_size_Unsize	at_size_Sized
Time	9.31	9.19	9.05	9.22	14.21	7.46	7.98	7.48	6.06	7.25
Nromalized	1	0.98	0.97	0.99	1.53	1	1.07	1.00	1	1.20

Minimum of 10 10,000 iterations

E-08 seconds	UnSized_id	Sized_id	Map_Add_Un	Map_Add_Lib	Map_Add_Size	Map_Square_Un	Map_Square_Lib	Map_Square_Size	Size_it
Time	3.27	3.22	3.25	3.25	3.25	3.26	3.26	3.25	3.26
Nromalized	1	0.98	1	1	1	1	1	0.99	-

E-08 seconds	Zip_Unsized	Zip_U_Pair	Zip_Sized	Zip_S_Pair	Zip_S_unrefine	Append_Unsized	Apeed_Un_Lib	Append_Sized	at_size_Unsize	at_size_Sized
Time	3.25	3.26	3.26	3.26	3.25	3.25	3.25	3.25	3.25	3.25
Nromalized	1	1.00	1.00	1.00	1	1	1	1	1	1

Conclusions and Analysis

• From the above data, it seems that there is no significant performance difference between the sized one and unsized one.
• For the average on 10*100 iterations, most function need more time for sized version except for the id and zip function.
• For the minimum on 10*10,000 iterations, most function use the same time except for the id and at size function.
• The 10*10,000 one need much less time for most functions than the 10*100 one, except for id function.

To get a more clear differentiation between sized list and unsized list w.r.t performance, it seems that experiment need to be conducted in another way.