From 1972639ed4bb0aab7136e3f09d6a46398afec709 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sat, 23 Mar 2013 15:30:28 +0100 Subject: [PATCH] Printout statistics about cache occupation. --- src/auto/ata.ml | 9 ++- src/utils/cache.ml | 162 +++++++++++++++++++++++++++++++------------- src/utils/cache.mli | 8 ++- src/utils/hcons.ml | 4 +- 4 files changed, 132 insertions(+), 51 deletions(-) diff --git a/src/auto/ata.ml b/src/auto/ata.ml index 2710465..6f74455 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -193,7 +193,12 @@ let create s ss = Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2; Cache.N6.iteri (fun _ _ _ _ _ _ _ b -> if b then incr n6) auto.cache6; Format.eprintf "INFO: automaton %i, cache2: %i entries, cache6: %i entries\n%!" - (auto.id :> int) !n2 !n6 + (auto.id :> int) !n2 !n6; + let c2l, c2u = Cache.N2.stats auto.cache2 in + let c6l, c6u = Cache.N6.stats auto.cache6 in + Format.eprintf "INFO: cache2: length: %i, used: %i, occupation: %f\n%!" c2l c2u (float c2u /. float c2l); + Format.eprintf "INFO: cache6: length: %i, used: %i, occupation: %f\n%!" c6l c6u (float c6u /. float c6l) + ); auto diff --git a/src/utils/cache.ml b/src/utils/cache.ml index abd999e..f9b7457 100644 --- a/src/utils/cache.ml +++ b/src/utils/cache.ml @@ -14,37 +14,26 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) -let realloc l old_size new_size dummy = - let l' = Array.create new_size dummy in - for i = 0 to (min old_size new_size) - 1 do - Array.unsafe_set l' i (Array.unsafe_get l i); - done; - l' - module N1 = struct - type 'a t = { mutable line : 'a array; - dummy : 'a; - mutable offset : int; - } - let create a = { + type 'a t = { + mutable line : 'a array; + dummy : 'a; + mutable offset : int; + level : int; + } + type 'a index = int -> 'a + let level a = a.level + let create_with_level level a = { line = Array.create 0 a; dummy = a; offset = ~-1; - + level = level; } - - let print fmt a = - Format.fprintf fmt "{ offset=%i;\n dummy=_;line=%a \n}\n%!" - a.offset - (Pretty.print_array ~sep:", " (fun fmt x -> - if x==a.dummy then - Format.fprintf fmt "%s" "D" - else - Format.fprintf fmt "%s" "E")) a.line + let create a = create_with_level 1 a let add a i v = if a.offset == ~-1 then a.offset <- i; @@ -56,7 +45,7 @@ struct if i < offset then begin (* bottom resize *) let pad = offset - i in let nlen = len + pad in - let narray = Array.create nlen a.dummy in + let narray = Array.create nlen a.dummy in for j = 0 to len - 1 do narray.(j+pad) <- a.line.(j) done; @@ -91,20 +80,28 @@ struct f (i+a.offset) v (v==a.dummy) done - + let stats a = + let d = dummy a in + let len = Array.length a.line in + let used = Array.fold_left (fun acc i -> + if i != d then acc+1 else acc) 0 a.line + in + len, used end module N2 = struct type 'a t = 'a N1.t N1.t - let create a = - let dummy1 = N1.create a in - N1.create dummy1 + let create_with_level level a = + let dummy1 = N1.create_with_level (level+1) a in + N1.create_with_level level dummy1 + + let create a = create_with_level 1 a let add a i j v = let line = N1.find a i in - if line == a.N1.dummy then - let nline = N1.create line.N1.dummy in + if line == N1.dummy a then + let nline = N1.create_with_level (a.N1.level+1) (N1.dummy line) in N1.add a i nline; N1.add nline j v else @@ -126,6 +123,17 @@ struct N1.iteri (f i) line.(i) done + let stats a = + let d = a.N1.dummy in + let len, used = + Array.fold_left (fun ((alen,aused) as acc) i -> + if i != d then + let l, u = N1.stats i in + (alen+l, aused+u) + else + acc) (0, 0) a.N1.line + in + len, used end @@ -133,14 +141,17 @@ module N3 = struct type 'a t = 'a N2.t N1.t - let create a = - let dummy2 = N2.create a in - N1.create dummy2 + let create_with_level level a = + let dummy2 = N2.create_with_level (level+1) a in + N1.create_with_level (level) dummy2 + + let create a = create_with_level 1 a + let add a i j k v = let line = N1.find a i in if line == a.N1.dummy then - let nline = N1.create line.N1.dummy in + let nline = N2.create_with_level (a.N1.level+1) (N2.dummy line) in N1.add a i nline; N2.add nline j k v else @@ -160,20 +171,35 @@ struct N2.iteri (f i) line.(i) done + let stats a = + let d = a.N1.dummy in + let len, used = + Array.fold_left (fun ((alen,aused) as acc) i -> + if i != d then + let l, u = N2.stats i in + (alen+l, aused+u) + else + acc) (0, 0) a.N1.line + in + len, used + end module N4 = struct type 'a t = 'a N3.t N1.t - let create a = - let dummy3 = N3.create a in - N1.create dummy3 + let create_with_level level a = + let dummy3 = N3.create_with_level (level+1) a in + N1.create_with_level (level) dummy3 + + let create a = create_with_level 1 a + let add a i j k l v = let line = N1.find a i in if line == N1.dummy a then - let nline = N3.create (N3.dummy line) in + let nline = N3.create_with_level (a.N1.level+1) (N3.dummy line) in N1.add a i nline; N3.add nline j k l v else @@ -190,20 +216,35 @@ struct N1.iteri (fun i v _ -> N3.iteri (fun j k l v2 b -> f i j k l v2 b) v ) a + let stats a = + let d = a.N1.dummy in + let len, used = + Array.fold_left (fun ((alen,aused) as acc) i -> + if i != d then + let l, u = N3.stats i in + (alen+l, aused+u) + else + acc) (0, 0) a.N1.line + in + len, used + end module N5 = struct type 'a t = 'a N4.t N1.t - let create a = - let dummy4 = N4.create a in - N1.create dummy4 + + let create_with_level level a = + let dummy4 = N4.create_with_level (level+1) a in + N1.create_with_level level dummy4 + + let create a = create_with_level 1 a let add a i j k l m v = let line = N1.find a i in if line == (N1.dummy a) then - let nline = N4.create (N4.dummy line) in + let nline = N4.create_with_level (a.N1.level+1) (N4.dummy line) in N1.add a i nline; N4.add nline j k l m v else @@ -220,20 +261,36 @@ struct N1.iteri (fun i v _ -> N4.iteri (fun j k l m v2 b -> f i j k l m v2 b) v ) a + + + let stats a = + let d = a.N1.dummy in + let len, used = + Array.fold_left (fun ((alen,aused) as acc) i -> + if i != d then + let l, u = N4.stats i in + (alen+l, aused+u) + else + acc) (0, 0) a.N1.line + in + len, used + end module N6 = struct type 'a t = 'a N5.t N1.t - let create a = - let dummy5 = N5.create a in - N1.create dummy5 + let create_with_level level a = + let dummy5 = N5.create_with_level (level+1) a in + N1.create_with_level (level) dummy5 + + let create a = create_with_level 1 a let add a i j k l m n v = let line = N1.find a i in if line == N1.dummy a then - let nline = N5.create (N5.dummy line) in + let nline = N5.create_with_level (a.N1.level+1) (N5.dummy line) in N1.add a i nline; N5.add nline j k l m n v else @@ -250,4 +307,17 @@ struct N1.iteri (fun i v _ -> N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v ) a + + let stats a = + let d = a.N1.dummy in + let len, used = + Array.fold_left (fun ((alen,aused) as acc) i -> + if i != d then + let l, u = N5.stats i in + (alen+l, aused+u) + else + acc) (0, 0) a.N1.line + in + len, used + end diff --git a/src/utils/cache.mli b/src/utils/cache.mli index 1211935..5827f6c 100644 --- a/src/utils/cache.mli +++ b/src/utils/cache.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** N-dimentional caches *) @@ -28,6 +28,7 @@ sig val add : 'a t -> int -> 'a -> unit val dummy : 'a t -> 'a val iteri : (int -> 'a -> bool -> unit) -> 'a t -> unit + val stats : 'a t -> int*int end module N2: @@ -38,6 +39,7 @@ sig val add : 'a t -> int -> int -> 'a -> unit val dummy : 'a t -> 'a val iteri : (int -> int -> 'a -> bool -> unit) -> 'a t -> unit + val stats : 'a t -> int*int end module N3 : @@ -48,6 +50,7 @@ module N3 : val add : 'a t -> int -> int -> int -> 'a -> unit val dummy : 'a t -> 'a val iteri : (int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit + val stats : 'a t -> int*int end module N4 : @@ -58,6 +61,7 @@ module N4 : val add : 'a t -> int -> int -> int -> int -> 'a -> unit val dummy : 'a t -> 'a val iteri : (int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit + val stats : 'a t -> int*int end module N5 : @@ -68,6 +72,7 @@ module N5 : val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit val dummy : 'a t -> 'a val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit + val stats : 'a t -> int*int end module N6 : @@ -78,4 +83,5 @@ module N6 : val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit val dummy : 'a t -> 'a val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit + val stats : 'a t -> int*int end diff --git a/src/utils/hcons.ml b/src/utils/hcons.ml index 3fc3e71..cc7327a 100644 --- a/src/utils/hcons.ml +++ b/src/utils/hcons.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) include Hcons_sig @@ -51,7 +51,7 @@ struct let dummy x = { id = Uid.dummy; hash = H.hash x; node = x } let make x = - let cell = { id = Uid.dummy; hash = H.hash x; node = x } in + let cell = dummy x in try T.find pool cell with -- 2.17.1