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
(************************************************************************)
9
(* $Id: profile.ml 7538 2005-11-08 17:14:52Z herbelin $ *)
13
let word_length = Sys.word_size / 8
14
let int_size = Sys.word_size - 1
16
let float_of_time t = float_of_int t /. 100.
17
let time_of_float f = int_of_float (f *. 100.)
20
let {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
21
time_of_float (ut +. st)
23
(* Since ocaml 3.01, gc statistics are in float *)
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 *)
31
(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *)
32
(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *)
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)
42
let last_alloc = ref 0.0 (* set by init_profile () *)
45
let now = get_alloc () in
46
let before = !last_alloc in
48
now -. before -. get_alloc_overhead
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;
62
let create_record () = {
72
let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw
73
let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw
75
let reset_record (n,e) =
86
let prof_table = ref []
89
let init_alloc = ref 0.0
91
let reset_profile () = List.iter reset_record !prof_table
94
let outside = create_record () in
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
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
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
117
let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
118
let (old_table, old_outside, old_total) =
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
126
with Sys_error msg ->
127
(Printf.printf "Unable to open %s: %s\n" filename msg;
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
138
[Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in
139
output_binary_int c magic;
140
output_value c updated_data;
142
with Sys_error _ -> Printf.printf "Unable to create recording file");
146
(************************************************)
147
(* Compute a rough estimation of time overheads *)
149
(* Time and space are not measured in the same way *)
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 *)
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
163
---------- start profile for f1
165
---------- [1w1] 1st call to get_time for f1
169
---------- start profile for 1st call to f2 inside f1
171
---------- [2w1] 1st call to get_time for 1st f2
173
---------- start 1st f2
175
---------- end 1st f2
177
---------- [2w1] 2nd call to get_time for 1st f2
179
---------- end profile for 1st f2
181
---------- start profile for 2nd call to f2 inside f1
183
---------- [2'w1] 1st call to get_time for 2nd f2
185
---------- start 2nd f2
187
---------- end 2nd f2
189
---------- [2'w2] 2nd call to get_time for 2nd f2
191
---------- end profile for f2
195
---------- [1w1'] 2nd call to get_time for f1
197
---------- end profile for f1
199
When profiling f2, overheadB + overheadC should be subtracted from measure
200
and overheadA + overheadB + overheadC + overheadD should be subtracted from
203
Then the relevant overheads are :
205
"overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and
207
"overheadA + overheadB + overheadC + overheadD" to be subtracted to
208
the measure of f as many time as f calls a profiled function (itself
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
219
let dummy_stack = ref [create_record ()]
224
let time_overhead_A_D () =
225
let e = create_record () in
226
let before = get_time () in
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;
246
(match !dummy_stack with [] -> assert false | _::s -> stack := s);
247
dummy_last_alloc := get_alloc ()
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
256
let time_overhead_B_C () =
258
let before = get_time () in
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
266
with _ -> assert false
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
275
let compute_alloc lo = lo /. (float_of_int word_length)
277
(************************************************)
278
(* End a profiling session and print the result *)
280
let format_profile (table, outside, total) =
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) ->
288
"%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n"
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)
295
Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n"
297
(float_of_time outside.owntime) (float_of_time outside.tottime)
298
(compute_alloc outside.ownalloc)
299
(compute_alloc outside.totalloc)
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);
308
"Time in seconds and allocation in words (1 word = %d bytes)\n"
311
let recording_file = ref ""
312
let set_recording s = recording_file := s
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
319
tottime = e.tottime - int_of_float (abcd_all +. bc_imm);
320
owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
322
let close_profile print =
323
let dw = spent_alloc () in
324
let t = get_time () in
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
346
match !recording_file with
348
| name -> merge_profile !recording_file current_data
350
if print then format_profile updated_data;
353
| _ -> failwith "Inconsistency"
355
let append_profile () = close_profile false
356
let print_profile () = close_profile true
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;
365
(* Default initialisation, may be overriden *)
366
let _ = init_profile ()
368
(******************************)
369
(* Entry points for profiling *)
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
382
last_alloc := get_alloc ();
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;
394
(match !stack with [] -> assert false | _::s -> stack := s);
395
last_alloc := get_alloc ();
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;
408
(match !stack with [] -> assert false | _::s -> stack := s);
409
last_alloc := get_alloc ();
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
424
last_alloc := get_alloc ();
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;
436
(match !stack with [] -> assert false | _::s -> stack := s);
437
last_alloc := get_alloc ();
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;
450
(match !stack with [] -> assert false | _::s -> stack := s);
451
last_alloc := get_alloc ();
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
466
last_alloc := get_alloc ();
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;
478
(match !stack with [] -> assert false | _::s -> stack := s);
479
last_alloc := get_alloc ();
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;
492
(match !stack with [] -> assert false | _::s -> stack := s);
493
last_alloc := get_alloc ();
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
508
last_alloc := get_alloc ();
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;
520
(match !stack with [] -> assert false | _::s -> stack := s);
521
last_alloc := get_alloc ();
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;
534
(match !stack with [] -> assert false | _::s -> stack := s);
535
last_alloc := get_alloc ();
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
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;
562
(match !stack with [] -> assert false | _::s -> stack := s);
563
last_alloc := get_alloc ();
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;
576
(match !stack with [] -> assert false | _::s -> stack := s);
577
last_alloc := get_alloc ();
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
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;
604
(match !stack with [] -> assert false | _::s -> stack := s);
605
last_alloc := get_alloc ();
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;
618
(match !stack with [] -> assert false | _::s -> stack := s);
619
last_alloc := get_alloc ();
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
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;
646
(match !stack with [] -> assert false | _::s -> stack := s);
647
last_alloc := get_alloc ();
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;
660
(match !stack with [] -> assert false | _::s -> stack := s);
661
last_alloc := get_alloc ();
664
(* Some utilities to compute the logical and physical sizes and depth
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)
685
let n = Obj.size t in
686
s := !s + n; b := !b + 1;
687
block_stats (d + 1) (n - 1) t
689
and block_stats d i t =
690
if i >= 0 then (obj_stats d (field t i); block_stats d (i-1) t)
693
c := 0; s:= 0; b:= 0; m:= 0;
694
obj_stats 0 (Obj.repr a);
697
module H = Hashtbl.Make(
701
let hash o = Hashtbl.hash (magic o : int)
704
let tbl = H.create 13
706
let rec obj_shared_size s t =
708
else if H.mem tbl t then s
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
718
block_shared_size (s + n + 1) (n - 1) t
721
and block_shared_size s i t =
723
else block_shared_size (obj_shared_size s (field t i)) (i-1) t
725
let obj_shared_size a =
728
let s = obj_shared_size 0 (Obj.repr a) in
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
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
741
let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }