src/Pure/ML-Systems/timing.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32935 2218b970325a
child 40300 d4487353b3a0
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      Pure/ML-Systems/timing.ML
     2     Author:     Makarius
     3 
     4 Compiler-independent timing functions.
     5 *)
     6 
     7 fun start_timing () =
     8   let
     9     val real_timer = Timer.startRealTimer ();
    10     val real_time = Timer.checkRealTimer real_timer;
    11     val cpu_timer = Timer.startCPUTimer ();
    12     val cpu_times = Timer.checkCPUTimes cpu_timer;
    13   in (real_timer, real_time, cpu_timer, cpu_times) end;
    14 
    15 fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
    16   let
    17     val real_time2 = Timer.checkRealTimer real_timer;
    18     val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    19     val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
    20       Timer.checkCPUTimes cpu_timer;
    21 
    22     open Time;
    23     val elapsed = real_time2 - real_time;
    24     val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    25     val cpu = usr2 - usr + sys2 - sys + gc;
    26 
    27     val message =
    28       (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
    29         toString gc ^ "s GC time") handle Time.Time => "";
    30   in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
    31