src/Pure/ML-Systems/timing.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 31757 c1262feb61c7
child 32935 2218b970325a
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm@31686
     1
(*  Title:      Pure/ML-Systems/timing.ML
wenzelm@31686
     2
    Author:     Makarius
wenzelm@31686
     3
wenzelm@31686
     4
Compiler-independent timing functions.
wenzelm@31686
     5
*)
wenzelm@31686
     6
wenzelm@31686
     7
fun start_timing () =
wenzelm@31686
     8
  let
wenzelm@31686
     9
    val real_timer = Timer.startRealTimer ();
wenzelm@31686
    10
    val real_time = Timer.checkRealTimer real_timer;
wenzelm@31686
    11
    val cpu_timer = Timer.startCPUTimer ();
wenzelm@31686
    12
    val cpu_times = Timer.checkCPUTimes cpu_timer;
wenzelm@31686
    13
  in (real_timer, real_time, cpu_timer, cpu_times) end;
wenzelm@31686
    14
wenzelm@31686
    15
fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
wenzelm@31686
    16
  let
wenzelm@31686
    17
    val real_time2 = Timer.checkRealTimer real_timer;
wenzelm@31686
    18
    val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
wenzelm@31686
    19
    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
wenzelm@31686
    20
      Timer.checkCPUTimes cpu_timer;
wenzelm@31686
    21
wenzelm@31757
    22
    fun checked x y = Real.checkFloat y handle Overflow => x | Div => x;
wenzelm@31757
    23
wenzelm@31686
    24
    open Time;
wenzelm@31686
    25
    val elapsed = real_time2 - real_time;
wenzelm@31686
    26
    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
wenzelm@31686
    27
    val cpu = usr2 - usr + sys2 - sys + gc;
wenzelm@31757
    28
    val gc_percent =
wenzelm@31757
    29
      Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * checked 0.0 (toReal gc / toReal cpu));
wenzelm@31757
    30
    val factor =
wenzelm@31757
    31
      Real.fmt (StringCvt.FIX (SOME 2)) (checked 1.0 (toReal cpu / toReal elapsed));
wenzelm@31686
    32
    val message =
wenzelm@31686
    33
      (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
wenzelm@31693
    34
        gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
wenzelm@31686
    35
  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
wenzelm@31686
    36