~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to lib/profile.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: profile.ml 7538 2005-11-08 17:14:52Z herbelin $ *)
 
10
 
 
11
open Gc
 
12
 
 
13
let word_length = Sys.word_size / 8
 
14
let int_size = Sys.word_size - 1
 
15
 
 
16
let float_of_time t = float_of_int t /. 100.
 
17
let time_of_float f = int_of_float (f *. 100.)
 
18
 
 
19
let get_time () =
 
20
  let  {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
 
21
  time_of_float (ut +. st)
 
22
 
 
23
(* Since ocaml 3.01, gc statistics are in float *)
 
24
let get_alloc () =
 
25
  (* If you are unlucky, a minor collection can occur between the *)
 
26
  (* measurements and produces allocation; we trigger a minor *)
 
27
  (* collection in advance to be sure the measure is not corrupted *)
 
28
  Gc.minor ();
 
29
  Gc.allocated_bytes ()
 
30
 
 
31
(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *)
 
32
(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *)
 
33
 
 
34
let get_alloc_overhead =
 
35
  let mark1 = get_alloc () in
 
36
  let mark2 = get_alloc () in
 
37
  let mark3 = get_alloc () in
 
38
  (* If you are unlucky, a major collection can occur between the *)
 
39
  (* measurements; with two measures the risk decreases *)
 
40
  min (mark2 -. mark1) (mark3 -. mark2)
 
41
 
 
42
let last_alloc = ref 0.0 (* set by init_profile () *)
 
43
 
 
44
let spent_alloc () =
 
45
  let now = get_alloc () in
 
46
  let before = !last_alloc in
 
47
  last_alloc := now;
 
48
  now -. before -. get_alloc_overhead
 
49
 
 
50
(* Profile records *)
 
51
 
 
52
type profile_key = {
 
53
  mutable owntime : int;
 
54
  mutable tottime : int;
 
55
  mutable ownalloc : float;
 
56
  mutable totalloc : float;
 
57
  mutable owncount : int;
 
58
  mutable intcount : int;
 
59
  mutable immcount : int;
 
60
}
 
61
 
 
62
let create_record () = {
 
63
  owntime=0;
 
64
  tottime=0;
 
65
  ownalloc=0.0;
 
66
  totalloc=0.0;
 
67
  owncount=0;
 
68
  intcount=0;
 
69
  immcount=0
 
70
}
 
71
 
 
72
let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw
 
73
let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw
 
74
 
 
75
let reset_record (n,e) =
 
76
  e.owntime <- 0;
 
77
  e.tottime <- 0;
 
78
  e.ownalloc <- 0.0;
 
79
  e.totalloc <- 0.0;
 
80
  e.owncount <- 0;
 
81
  e.intcount <- 0;
 
82
  e.immcount <- 0
 
83
 
 
84
(* Profile tables *)
 
85
 
 
86
let prof_table = ref []
 
87
let stack = ref []
 
88
let init_time = ref 0
 
89
let init_alloc = ref 0.0
 
90
 
 
91
let reset_profile () = List.iter reset_record !prof_table
 
92
 
 
93
let init_profile () =
 
94
  let outside = create_record () in
 
95
  stack := [outside];
 
96
  last_alloc := get_alloc ();
 
97
  init_alloc := !last_alloc;
 
98
  init_time := get_time ();
 
99
  outside.tottime <- - !init_time;
 
100
  outside.owntime <- - !init_time
 
101
 
 
102
let ajoute n o =
 
103
  o.owntime <- o.owntime + n.owntime;
 
104
  o.tottime <- o.tottime + n.tottime;
 
105
  ajoute_ownalloc o n.ownalloc;
 
106
  ajoute_totalloc o n.totalloc;
 
107
  o.owncount <- o.owncount + n.owncount;
 
108
  o.intcount <- o.intcount + n.intcount;
 
109
  o.immcount <- o.immcount + n.immcount
 
110
 
 
111
let ajoute_to_list ((name,n) as e) l =
 
112
  try ajoute n (List.assoc name l); l
 
113
  with Not_found -> e::l
 
114
 
 
115
let magic = 1249
 
116
  
 
117
let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
 
118
  let (old_table, old_outside, old_total) =
 
119
    try 
 
120
      let c = open_in filename in
 
121
      if input_binary_int c <> magic 
 
122
      then Printf.printf "Incompatible recording file: %s\n" filename;
 
123
      let old_data = input_value c in
 
124
      close_in c;
 
125
      old_data
 
126
    with Sys_error msg ->
 
127
      (Printf.printf "Unable to open %s: %s\n" filename msg;
 
128
       new_data) in
 
129
  let updated_data =
 
130
    let updated_table = List.fold_right ajoute_to_list curr_table old_table in
 
131
    ajoute curr_outside old_outside;
 
132
    ajoute curr_total old_total;
 
133
    (updated_table, old_outside, old_total) in
 
134
  begin
 
135
    (try
 
136
       let c =
 
137
         open_out_gen 
 
138
           [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in
 
139
       output_binary_int c magic;
 
140
       output_value c updated_data;
 
141
       close_out c
 
142
     with Sys_error _ -> Printf.printf "Unable to create recording file");
 
143
    updated_data
 
144
  end
 
145
 
 
146
(************************************************)
 
147
(* Compute a rough estimation of time overheads *)
 
148
 
 
149
(* Time and space are not measured in the same way *)
 
150
 
 
151
(* Byte allocation is an exact number and for long runs, the total
 
152
   number of allocated bytes may exceed the maximum integer capacity
 
153
   (2^31 on 32-bits architectures);  therefore, allocation is measured
 
154
   by small steps, total allocations are computed by adding elementary
 
155
   measures and carries are controled from step to step *)
 
156
 
 
157
(* Unix measure of time is approximative and shoitt delays are often
 
158
   unperceivable; therefore, total times are measured in one (big)
 
159
   step to avoid rounding errors and to get the best possible
 
160
   approximation *)
 
161
 
 
162
(*
 
163
----------        start profile for f1
 
164
overheadA|        ...
 
165
  ---------- [1w1]  1st call to get_time for f1
 
166
  overheadB|        ...
 
167
  ----------        start f1
 
168
   real 1  |        ...
 
169
  ----------        start profile for 1st call to f2 inside f1
 
170
  overheadA|        ...
 
171
    ---------- [2w1]  1st call to get_time for 1st f2
 
172
    overheadB|        ...
 
173
    ----------        start 1st f2
 
174
     real 2  |        ...
 
175
    ----------        end 1st f2
 
176
    overheadC|        ...
 
177
    ---------- [2w1]  2nd call to get_time for 1st f2
 
178
  overheadD|        ...
 
179
  ----------        end profile for 1st f2
 
180
   real 1  |        ...
 
181
  ----------        start profile for 2nd call to f2 inside f1
 
182
  overheadA|        ...
 
183
    ---------- [2'w1] 1st call to get_time for 2nd f2
 
184
    overheadB|        ...
 
185
    ----------        start 2nd f2
 
186
     real 2' |        ...
 
187
    ----------        end 2nd f2
 
188
    overheadC|        ...
 
189
    ---------- [2'w2]  2nd call to get_time for 2nd f2 
 
190
  overheadD|        ...
 
191
  ----------        end profile for f2
 
192
   real 1  |        ...
 
193
  ----------        end f1
 
194
  overheadC|        ...
 
195
---------- [1w1'] 2nd call to get_time for f1
 
196
overheadD|        ...
 
197
----------        end profile for f1
 
198
 
 
199
When profiling f2, overheadB + overheadC should be subtracted from measure
 
200
and overheadA + overheadB + overheadC + overheadD should be subtracted from
 
201
the amount for f1
 
202
 
 
203
Then the relevant overheads are :
 
204
 
 
205
  "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and
 
206
 
 
207
  "overheadA + overheadB + overheadC + overheadD" to be subtracted to
 
208
  the measure of f as many time as f calls a profiled function (itself
 
209
  included)
 
210
*)
 
211
 
 
212
let dummy_last_alloc = ref 0.0
 
213
let dummy_spent_alloc () =
 
214
  let now = get_alloc () in
 
215
  let before = !last_alloc in
 
216
  last_alloc := now;
 
217
  now -. before
 
218
let dummy_f x = x
 
219
let dummy_stack = ref [create_record ()]
 
220
let dummy_ov = 0
 
221
 
 
222
let loops = 10000
 
223
 
 
224
let time_overhead_A_D () =
 
225
  let e = create_record () in
 
226
  let before = get_time () in
 
227
  for i=1 to loops do
 
228
    (* This is a copy of profile1 for overhead estimation *)
 
229
    let dw = dummy_spent_alloc () in
 
230
    match !dummy_stack with [] -> assert false | p::_ ->
 
231
      ajoute_ownalloc p dw;
 
232
      ajoute_totalloc p dw;
 
233
      e.owncount <- e.owncount + 1;
 
234
      if not (p==e) then stack := e::!stack;
 
235
      let totalloc0 = e.totalloc in
 
236
      let intcount0 = e.intcount in
 
237
      let dt = get_time () - 1 in
 
238
      e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime;
 
239
      ajoute_ownalloc p dw;
 
240
      ajoute_totalloc p dw;
 
241
      p.owntime <- p.owntime - e.tottime;
 
242
      ajoute_totalloc p (e.totalloc-.totalloc0);
 
243
      p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
244
      p.immcount <- p.immcount + 1;
 
245
      if not (p==e) then 
 
246
        (match !dummy_stack with [] -> assert false | _::s -> stack := s);
 
247
      dummy_last_alloc := get_alloc ()
 
248
  done;
 
249
  let after = get_time () in
 
250
  let beforeloop =  get_time () in
 
251
  for i=1 to loops do () done;
 
252
  let afterloop = get_time () in
 
253
  float_of_int ((after - before) - (afterloop - beforeloop))
 
254
  /. float_of_int loops
 
255
 
 
256
let time_overhead_B_C () =
 
257
  let dummy_x = 0 in
 
258
  let before = get_time () in
 
259
  for i=1 to loops do
 
260
    try
 
261
      dummy_last_alloc := get_alloc ();
 
262
      let _r = dummy_f dummy_x in
 
263
      let _dw = dummy_spent_alloc () in
 
264
      let _dt = get_time () in
 
265
      ()
 
266
    with _ -> assert false
 
267
  done;
 
268
  let after = get_time () in
 
269
  let beforeloop =  get_time () in
 
270
  for i=1 to loops do () done;
 
271
  let afterloop = get_time () in
 
272
  float_of_int ((after - before) - (afterloop - beforeloop))
 
273
  /. float_of_int loops
 
274
 
 
275
let compute_alloc lo = lo /. (float_of_int word_length)
 
276
 
 
277
(************************************************)
 
278
(* End a profiling session and print the result *)
 
279
 
 
280
let format_profile (table, outside, total) =
 
281
  print_newline ();
 
282
  Printf.printf 
 
283
    "%-23s  %9s %9s %10s %10s %10s\n"
 
284
    "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls ";
 
285
  let l = Sort.list (fun (_,{tottime=p}) (_,{tottime=p'}) -> p > p') table in
 
286
  List.iter (fun (name,e) ->
 
287
    Printf.printf
 
288
      "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n"
 
289
      name
 
290
      (float_of_time e.owntime) (float_of_time e.tottime)
 
291
      (compute_alloc e.ownalloc)
 
292
      (compute_alloc e.totalloc)
 
293
      e.owncount e.intcount)
 
294
    l;
 
295
  Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f        %6d\n"
 
296
    "others" 
 
297
    (float_of_time outside.owntime) (float_of_time outside.tottime)
 
298
    (compute_alloc outside.ownalloc)
 
299
    (compute_alloc outside.totalloc)
 
300
    outside.intcount;
 
301
  (* Here, own contains overhead time/alloc *)
 
302
  Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n"
 
303
    "Est. overhead/total"
 
304
    (float_of_time total.owntime) (float_of_time total.tottime)
 
305
    (compute_alloc total.ownalloc)
 
306
    (compute_alloc total.totalloc);
 
307
  Printf.printf
 
308
    "Time in seconds and allocation in words (1 word = %d bytes)\n" 
 
309
    word_length
 
310
 
 
311
let recording_file = ref ""
 
312
let set_recording s = recording_file := s
 
313
 
 
314
let adjust_time ov_bc ov_ad e =
 
315
  let bc_imm = float_of_int e.owncount *. ov_bc in
 
316
  let ad_imm = float_of_int e.immcount *. ov_ad in
 
317
  let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in
 
318
  {e with
 
319
     tottime = e.tottime - int_of_float (abcd_all +. bc_imm);
 
320
     owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
 
321
 
 
322
let close_profile print = 
 
323
  let dw = spent_alloc () in
 
324
  let t = get_time () in
 
325
  match !stack with
 
326
    | [outside] ->
 
327
        outside.tottime <- outside.tottime + t;
 
328
        outside.owntime <- outside.owntime + t;
 
329
        ajoute_ownalloc outside dw;
 
330
        ajoute_totalloc outside dw;
 
331
        if !prof_table <> [] then begin
 
332
          let ov_bc = time_overhead_B_C () (* B+C overhead *) in
 
333
          let ov_ad = time_overhead_A_D () (* A+D overhead *) in
 
334
          let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
 
335
          let adjtable = List.map adjust !prof_table in
 
336
          let adjoutside = adjust_time ov_bc ov_ad outside in
 
337
          let totalloc = !last_alloc -. !init_alloc in
 
338
          let total = create_record () in
 
339
          total.tottime <- outside.tottime;
 
340
          total.totalloc <- totalloc;
 
341
          (* We compute estimations of overhead, put into "own" fields *)
 
342
          total.owntime <- outside.tottime - adjoutside.tottime;
 
343
          total.ownalloc <- totalloc -. outside.totalloc;
 
344
          let current_data = (adjtable, adjoutside, total) in
 
345
          let updated_data =
 
346
            match !recording_file with
 
347
              | "" -> current_data
 
348
              | name -> merge_profile !recording_file current_data
 
349
          in
 
350
          if print then format_profile updated_data;
 
351
          init_profile ()
 
352
        end
 
353
    | _ -> failwith "Inconsistency"
 
354
 
 
355
let append_profile () = close_profile false
 
356
let print_profile () = close_profile true
 
357
 
 
358
let declare_profile name =
 
359
  if name = "___outside___" or name = "___total___" then
 
360
    failwith ("Error: "^name^" is a reserved keyword");
 
361
  let e = create_record () in
 
362
  prof_table := (name,e)::!prof_table;
 
363
  e
 
364
 
 
365
(* Default initialisation, may be overriden *)
 
366
let _ = init_profile ()
 
367
 
 
368
(******************************)
 
369
(* Entry points for profiling *)
 
370
let profile1 e f a =
 
371
  let dw = spent_alloc () in
 
372
  match !stack with [] -> assert false | p::_ ->
 
373
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
374
  ajoute_ownalloc p dw;
 
375
  ajoute_totalloc p dw;
 
376
  e.owncount <- e.owncount + 1;
 
377
  if not (p==e) then stack := e::!stack;
 
378
  let totalloc0 = e.totalloc in
 
379
  let intcount0 = e.intcount in
 
380
  let t = get_time () in
 
381
  try
 
382
    last_alloc := get_alloc ();
 
383
    let r = f a in
 
384
    let dw = spent_alloc () in
 
385
    let dt = get_time () - t in
 
386
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
387
    ajoute_ownalloc e dw;
 
388
    ajoute_totalloc e dw;
 
389
    p.owntime <- p.owntime - dt;
 
390
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
391
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
392
    p.immcount <- p.immcount + 1;
 
393
    if not (p==e) then 
 
394
      (match !stack with [] -> assert false | _::s -> stack := s);
 
395
    last_alloc := get_alloc ();
 
396
    r
 
397
  with exn ->
 
398
    let dw = spent_alloc () in
 
399
    let dt = get_time () - t in
 
400
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
401
    ajoute_ownalloc e dw;
 
402
    ajoute_totalloc e dw;
 
403
    p.owntime <- p.owntime - dt;
 
404
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
405
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
406
    p.immcount <- p.immcount + 1;
 
407
    if not (p==e) then 
 
408
      (match !stack with [] -> assert false | _::s -> stack := s);
 
409
    last_alloc := get_alloc ();
 
410
    raise exn
 
411
 
 
412
let profile2 e f a b =
 
413
  let dw = spent_alloc () in
 
414
  match !stack with [] -> assert false | p::_ ->
 
415
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
416
  ajoute_ownalloc p dw;
 
417
  ajoute_totalloc p dw;
 
418
  e.owncount <- e.owncount + 1;
 
419
  if not (p==e) then stack := e::!stack;
 
420
  let totalloc0 = e.totalloc in
 
421
  let intcount0 = e.intcount in
 
422
  let t = get_time () in
 
423
  try
 
424
    last_alloc := get_alloc ();
 
425
    let r = f a b in
 
426
    let dw = spent_alloc () in
 
427
    let dt = get_time () - t in
 
428
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
429
    ajoute_ownalloc e dw;
 
430
    ajoute_totalloc e dw;
 
431
    p.owntime <- p.owntime - dt;
 
432
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
433
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
434
    p.immcount <- p.immcount + 1;
 
435
    if not (p==e) then 
 
436
      (match !stack with [] -> assert false | _::s -> stack := s);
 
437
    last_alloc := get_alloc ();
 
438
    r
 
439
  with exn ->
 
440
    let dw = spent_alloc () in
 
441
    let dt = get_time () - t in
 
442
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
443
    ajoute_ownalloc e dw;
 
444
    ajoute_totalloc e dw;
 
445
    p.owntime <- p.owntime - dt;
 
446
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
447
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
448
    p.immcount <- p.immcount + 1;
 
449
    if not (p==e) then 
 
450
      (match !stack with [] -> assert false | _::s -> stack := s);
 
451
    last_alloc := get_alloc ();
 
452
    raise exn
 
453
 
 
454
let profile3 e f a b c =
 
455
  let dw = spent_alloc () in
 
456
  match !stack with [] -> assert false | p::_ ->
 
457
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
458
  ajoute_ownalloc p dw;
 
459
  ajoute_totalloc p dw;
 
460
  e.owncount <- e.owncount + 1;
 
461
  if not (p==e) then stack := e::!stack;
 
462
  let totalloc0 = e.totalloc in
 
463
  let intcount0 = e.intcount in
 
464
  let t = get_time () in
 
465
  try
 
466
    last_alloc := get_alloc ();
 
467
    let r = f a b c in
 
468
    let dw = spent_alloc () in
 
469
    let dt = get_time () - t in
 
470
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
471
    ajoute_ownalloc e dw;
 
472
    ajoute_totalloc e dw;
 
473
    p.owntime <- p.owntime - dt;
 
474
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
475
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
476
    p.immcount <- p.immcount + 1;
 
477
    if not (p==e) then 
 
478
      (match !stack with [] -> assert false | _::s -> stack := s);
 
479
    last_alloc := get_alloc ();
 
480
    r
 
481
  with exn ->
 
482
    let dw = spent_alloc () in
 
483
    let dt = get_time () - t in
 
484
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
485
    ajoute_ownalloc e dw;
 
486
    ajoute_totalloc e dw;
 
487
    p.owntime <- p.owntime - dt;
 
488
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
489
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
490
    p.immcount <- p.immcount + 1;
 
491
    if not (p==e) then 
 
492
      (match !stack with [] -> assert false | _::s -> stack := s);
 
493
    last_alloc := get_alloc ();
 
494
    raise exn
 
495
 
 
496
let profile4 e f a b c d =
 
497
  let dw = spent_alloc () in
 
498
  match !stack with [] -> assert false | p::_ ->
 
499
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
500
  ajoute_ownalloc p dw;
 
501
  ajoute_totalloc p dw;
 
502
  e.owncount <- e.owncount + 1;
 
503
  if not (p==e) then stack := e::!stack;
 
504
  let totalloc0 = e.totalloc in
 
505
  let intcount0 = e.intcount in
 
506
  let t = get_time () in
 
507
  try
 
508
    last_alloc := get_alloc ();
 
509
    let r = f a b c d in
 
510
    let dw = spent_alloc () in
 
511
    let dt = get_time () - t in
 
512
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
513
    ajoute_ownalloc e dw;
 
514
    ajoute_totalloc e dw;
 
515
    p.owntime <- p.owntime - dt;
 
516
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
517
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
518
    p.immcount <- p.immcount + 1;
 
519
    if not (p==e) then 
 
520
      (match !stack with [] -> assert false | _::s -> stack := s);
 
521
    last_alloc := get_alloc ();
 
522
    r
 
523
  with exn ->
 
524
    let dw = spent_alloc () in
 
525
    let dt = get_time () - t in
 
526
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
527
    ajoute_ownalloc e dw;
 
528
    ajoute_totalloc e dw;
 
529
    p.owntime <- p.owntime - dt;
 
530
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
531
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
532
    p.immcount <- p.immcount + 1;
 
533
    if not (p==e) then 
 
534
      (match !stack with [] -> assert false | _::s -> stack := s);
 
535
    last_alloc := get_alloc ();
 
536
    raise exn
 
537
 
 
538
let profile5 e f a b c d g =
 
539
  let dw = spent_alloc () in
 
540
  match !stack with [] -> assert false | p::_ ->
 
541
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
542
  ajoute_ownalloc p dw;
 
543
  ajoute_totalloc p dw;
 
544
  e.owncount <- e.owncount + 1;
 
545
  if not (p==e) then stack := e::!stack;
 
546
  let totalloc0 = e.totalloc in
 
547
  let intcount0 = e.intcount in
 
548
  let t = get_time () in
 
549
  try
 
550
    last_alloc := get_alloc ();
 
551
    let r = f a b c d g in
 
552
    let dw = spent_alloc () in
 
553
    let dt = get_time () - t in
 
554
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
555
    ajoute_ownalloc e dw;
 
556
    ajoute_totalloc e dw;
 
557
    p.owntime <- p.owntime - dt;
 
558
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
559
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
560
    p.immcount <- p.immcount + 1;
 
561
    if not (p==e) then 
 
562
      (match !stack with [] -> assert false | _::s -> stack := s);
 
563
    last_alloc := get_alloc ();
 
564
    r
 
565
  with exn ->
 
566
    let dw = spent_alloc () in
 
567
    let dt = get_time () - t in
 
568
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
569
    ajoute_ownalloc e dw;
 
570
    ajoute_totalloc e dw;
 
571
    p.owntime <- p.owntime - dt;
 
572
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
573
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
574
    p.immcount <- p.immcount + 1;
 
575
    if not (p==e) then 
 
576
      (match !stack with [] -> assert false | _::s -> stack := s);
 
577
    last_alloc := get_alloc ();
 
578
    raise exn
 
579
 
 
580
let profile6 e f a b c d g h =
 
581
  let dw = spent_alloc () in
 
582
  match !stack with [] -> assert false | p::_ ->
 
583
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
584
  ajoute_ownalloc p dw;
 
585
  ajoute_totalloc p dw;
 
586
  e.owncount <- e.owncount + 1;
 
587
  if not (p==e) then stack := e::!stack;
 
588
  let totalloc0 = e.totalloc in
 
589
  let intcount0 = e.intcount in
 
590
  let t = get_time () in
 
591
  try
 
592
    last_alloc := get_alloc ();
 
593
    let r = f a b c d g h in
 
594
    let dw = spent_alloc () in
 
595
    let dt = get_time () - t in
 
596
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
597
    ajoute_ownalloc e dw;
 
598
    ajoute_totalloc e dw;
 
599
    p.owntime <- p.owntime - dt;
 
600
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
601
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
602
    p.immcount <- p.immcount + 1;
 
603
    if not (p==e) then 
 
604
      (match !stack with [] -> assert false | _::s -> stack := s);
 
605
    last_alloc := get_alloc ();
 
606
    r
 
607
  with exn ->
 
608
    let dw = spent_alloc () in
 
609
    let dt = get_time () - t in
 
610
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
611
    ajoute_ownalloc e dw;
 
612
    ajoute_totalloc e dw;
 
613
    p.owntime <- p.owntime - dt;
 
614
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
615
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
616
    p.immcount <- p.immcount + 1;
 
617
    if not (p==e) then 
 
618
      (match !stack with [] -> assert false | _::s -> stack := s);
 
619
    last_alloc := get_alloc ();
 
620
    raise exn
 
621
 
 
622
let profile7 e f a b c d g h i =
 
623
  let dw = spent_alloc () in
 
624
  match !stack with [] -> assert false | p::_ ->
 
625
  (* We add spent alloc since last measure to current caller own/total alloc *)
 
626
  ajoute_ownalloc p dw;
 
627
  ajoute_totalloc p dw;
 
628
  e.owncount <- e.owncount + 1;
 
629
  if not (p==e) then stack := e::!stack;
 
630
  let totalloc0 = e.totalloc in
 
631
  let intcount0 = e.intcount in
 
632
  let t = get_time () in
 
633
  try
 
634
    last_alloc := get_alloc ();
 
635
    let r = f a b c d g h i in
 
636
    let dw = spent_alloc () in
 
637
    let dt = get_time () - t in
 
638
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
639
    ajoute_ownalloc e dw;
 
640
    ajoute_totalloc e dw;
 
641
    p.owntime <- p.owntime - dt;
 
642
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
643
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
644
    p.immcount <- p.immcount + 1;
 
645
    if not (p==e) then 
 
646
      (match !stack with [] -> assert false | _::s -> stack := s);
 
647
    last_alloc := get_alloc ();
 
648
    r
 
649
  with exn ->
 
650
    let dw = spent_alloc () in
 
651
    let dt = get_time () - t in
 
652
    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
 
653
    ajoute_ownalloc e dw;
 
654
    ajoute_totalloc e dw;
 
655
    p.owntime <- p.owntime - dt;
 
656
    ajoute_totalloc p (e.totalloc -. totalloc0);
 
657
    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
 
658
    p.immcount <- p.immcount + 1;
 
659
    if not (p==e) then 
 
660
      (match !stack with [] -> assert false | _::s -> stack := s);
 
661
    last_alloc := get_alloc ();
 
662
    raise exn
 
663
 
 
664
(* Some utilities to compute the logical and physical sizes and depth
 
665
   of ML objects *)
 
666
 
 
667
open Obj
 
668
 
 
669
let c = ref 0
 
670
let s = ref 0
 
671
let b = ref 0
 
672
let m = ref 0
 
673
 
 
674
let rec obj_stats d t =
 
675
  if is_int t then m := max d !m
 
676
  else if tag t >= no_scan_tag then
 
677
    if tag t = string_tag then
 
678
      (c := !c + size t; b := !b + 1; m := max d !m)
 
679
    else if tag t = double_tag then
 
680
      (s := !s + 2; b := !b + 1; m := max d !m)
 
681
    else if tag t = double_array_tag then
 
682
      (s := !s + 2 * size t; b := !b + 1; m := max d !m)
 
683
    else (b := !b + 1; m := max d !m)
 
684
  else
 
685
    let n = Obj.size t in
 
686
    s := !s + n; b := !b + 1;
 
687
    block_stats (d + 1) (n - 1) t
 
688
 
 
689
and block_stats d i t =
 
690
  if i >= 0 then (obj_stats d (field t i); block_stats d (i-1) t)
 
691
 
 
692
let obj_stats a =
 
693
  c := 0; s:= 0; b:= 0; m:= 0;
 
694
  obj_stats 0 (Obj.repr a);
 
695
  (!c, !s + !b, !m)
 
696
 
 
697
module H = Hashtbl.Make(
 
698
  struct 
 
699
    type t = Obj.t 
 
700
    let equal = (==) 
 
701
    let hash o = Hashtbl.hash (magic o : int)
 
702
  end)
 
703
 
 
704
let tbl = H.create 13
 
705
 
 
706
let rec obj_shared_size s t =
 
707
  if is_int t then s
 
708
  else if H.mem tbl t then s
 
709
  else begin
 
710
    H.add tbl t ();
 
711
    let n = Obj.size t in
 
712
    if tag t >= no_scan_tag then
 
713
      if tag t = string_tag then (c := !c + n; s + 1)
 
714
      else if tag t = double_tag then s + 3
 
715
      else if tag t = double_array_tag then s + 2 * n + 1
 
716
      else s + 1
 
717
    else
 
718
      block_shared_size (s + n + 1) (n - 1) t
 
719
  end
 
720
 
 
721
and block_shared_size s i t =
 
722
  if i < 0 then s
 
723
  else block_shared_size (obj_shared_size s (field t i)) (i-1) t
 
724
 
 
725
let obj_shared_size a =
 
726
  H.clear tbl;
 
727
  c := 0;
 
728
  let s = obj_shared_size 0 (Obj.repr a) in
 
729
  (!c, s)
 
730
 
 
731
let print_logical_stats a =
 
732
  let (c, s, d) = obj_stats a in
 
733
  Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d
 
734
 
 
735
let print_stats a =
 
736
  let (c1, s, d) = obj_stats a in
 
737
  let (c2, o) = obj_shared_size a in
 
738
  Printf.printf "Size: %8d (str: %8d) (exp: %10d)  Depth: %6d\n"
 
739
    (o + c2) c2 (s + c1) d
 
740
(*
 
741
let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }
 
742
*)