src/Pure/ML-Systems/timing.ML
author wenzelm
Wed, 17 Jun 2009 17:06:07 +0200
changeset 31686 e54ae15335a1
child 31693 8d1861721887
permissions -rw-r--r--
more detailed start_timing/end_timing (in timing.ML); removed obsolete check_timer;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31686
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/timing.ML
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     3
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     4
Compiler-independent timing functions.
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     5
*)
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     6
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     7
fun start_timing () =
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     8
  let
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     9
    val real_timer = Timer.startRealTimer ();
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    10
    val real_time = Timer.checkRealTimer real_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    11
    val cpu_timer = Timer.startCPUTimer ();
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    12
    val cpu_times = Timer.checkCPUTimes cpu_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    13
  in (real_timer, real_time, cpu_timer, cpu_times) end;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    14
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    15
fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    16
  let
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    17
    val real_time2 = Timer.checkRealTimer real_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    18
    val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    19
    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    20
      Timer.checkCPUTimes cpu_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    21
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    22
    open Time;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    23
    val elapsed = real_time2 - real_time;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    24
    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    25
    val cpu = usr2 - usr + sys2 - sys + gc;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    26
    val gc_ratio = Real.fmt (StringCvt.FIX (SOME 2)) (toReal gc / toReal cpu);
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    27
    val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    28
    val message =
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    29
      (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    30
        gc_ratio ^ "% GC time, factor " ^ factor) handle Time => "";
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    31
  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    32