more detailed start_timing/end_timing (in timing.ML);
authorwenzelm
Wed Jun 17 17:06:07 2009 +0200 (2009-06-17)
changeset 31686e54ae15335a1
parent 31685 c124445a4b61
child 31687 0d2f700fe5e7
more detailed start_timing/end_timing (in timing.ML);
removed obsolete check_timer;
src/Pure/IsaMakefile
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/timing.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Jun 17 17:06:07 2009 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Wed Jun 17 17:06:07 2009 +0200
     1.3 @@ -29,7 +29,8 @@
     1.4    ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
     1.5    ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
     1.6    ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
     1.7 -  ML-Systems/time_limit.ML ML-Systems/universal.ML
     1.8 +  ML-Systems/timing.ML ML-Systems/time_limit.ML				\
     1.9 +  ML-Systems/universal.ML
    1.10  
    1.11  RAW: $(OUT)/RAW
    1.12  
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Wed Jun 17 17:06:07 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Wed Jun 17 17:06:07 2009 +0200
     2.3 @@ -154,10 +154,6 @@
     2.4      val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
     2.5    in {message = message, user = user, all = all} end;
     2.6  
     2.7 -fun check_timer timer =
     2.8 -  let val {sys, usr, gc} = Timer.checkCPUTimer timer
     2.9 -  in (sys, usr, gc) end;
    2.10 -
    2.11  
    2.12  (* SML basis library fixes *)
    2.13  
     3.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:06:07 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:06:07 2009 +0200
     3.3 @@ -8,6 +8,7 @@
     3.4  use "ML-Systems/exn.ML";
     3.5  use "ML-Systems/multithreading.ML";
     3.6  use "ML-Systems/time_limit.ML";
     3.7 +use "ML-Systems/timing.ML";
     3.8  use "ML-Systems/system_shell.ML";
     3.9  use "ML-Systems/ml_pretty.ML";
    3.10  use "ML-Systems/use_context.ML";
    3.11 @@ -41,30 +42,6 @@
    3.12  val implode = SML90.implode;
    3.13  
    3.14  
    3.15 -(* compiler-independent timing functions *)
    3.16 -
    3.17 -fun start_timing () =
    3.18 -  let
    3.19 -    val timer = Timer.startCPUTimer ();
    3.20 -    val time = Timer.checkCPUTimer timer;
    3.21 -  in (timer, time) end;
    3.22 -
    3.23 -fun end_timing (timer, {sys, usr}) =
    3.24 -  let
    3.25 -    open Time;  (*...for Time.toString, Time.+ and Time.- *)
    3.26 -    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
    3.27 -    val user = usr2 - usr;
    3.28 -    val all = user + sys2 - sys;
    3.29 -    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
    3.30 -  in {message = message, user = user, all = all} end;
    3.31 -
    3.32 -fun check_timer timer =
    3.33 -  let
    3.34 -    val {sys, usr} = Timer.checkCPUTimer timer;
    3.35 -    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    3.36 -  in (sys, usr, gc) end;
    3.37 -
    3.38 -
    3.39  (* prompts *)
    3.40  
    3.41  fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Jun 17 17:06:07 2009 +0200
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jun 17 17:06:07 2009 +0200
     4.3 @@ -12,6 +12,7 @@
     4.4  use "ML-Systems/universal.ML";
     4.5  use "ML-Systems/thread_dummy.ML";
     4.6  use "ML-Systems/multithreading.ML";
     4.7 +use "ML-Systems/timing.ML";
     4.8  use "ML-Systems/system_shell.ML";
     4.9  use "ML-Systems/ml_name_space.ML";
    4.10  use "ML-Systems/ml_pretty.ML";
    4.11 @@ -59,30 +60,6 @@
    4.12  end;
    4.13  
    4.14  
    4.15 -(* compiler-independent timing functions *)
    4.16 -
    4.17 -fun start_timing () =
    4.18 -  let
    4.19 -    val timer = Timer.startCPUTimer ();
    4.20 -    val time = Timer.checkCPUTimer timer;
    4.21 -  in (timer, time) end;
    4.22 -
    4.23 -fun end_timing (timer, {sys, usr}) =
    4.24 -  let
    4.25 -    open Time;  (*...for Time.toString, Time.+ and Time.- *)
    4.26 -    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
    4.27 -    val user = usr2 - usr;
    4.28 -    val all = user + sys2 - sys;
    4.29 -    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
    4.30 -  in {message = message, user = user, all = all} end;
    4.31 -
    4.32 -fun check_timer timer =
    4.33 -  let
    4.34 -    val {sys, usr} = Timer.checkCPUTimer timer;
    4.35 -    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    4.36 -  in (sys, usr, gc) end;
    4.37 -
    4.38 -
    4.39  (*prompts*)
    4.40  fun ml_prompts p1 p2 =
    4.41    (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML-Systems/timing.ML	Wed Jun 17 17:06:07 2009 +0200
     5.3 @@ -0,0 +1,32 @@
     5.4 +(*  Title:      Pure/ML-Systems/timing.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Compiler-independent timing functions.
     5.8 +*)
     5.9 +
    5.10 +fun start_timing () =
    5.11 +  let
    5.12 +    val real_timer = Timer.startRealTimer ();
    5.13 +    val real_time = Timer.checkRealTimer real_timer;
    5.14 +    val cpu_timer = Timer.startCPUTimer ();
    5.15 +    val cpu_times = Timer.checkCPUTimes cpu_timer;
    5.16 +  in (real_timer, real_time, cpu_timer, cpu_times) end;
    5.17 +
    5.18 +fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
    5.19 +  let
    5.20 +    val real_time2 = Timer.checkRealTimer real_timer;
    5.21 +    val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    5.22 +    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
    5.23 +      Timer.checkCPUTimes cpu_timer;
    5.24 +
    5.25 +    open Time;
    5.26 +    val elapsed = real_time2 - real_time;
    5.27 +    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    5.28 +    val cpu = usr2 - usr + sys2 - sys + gc;
    5.29 +    val gc_ratio = Real.fmt (StringCvt.FIX (SOME 2)) (toReal gc / toReal cpu);
    5.30 +    val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
    5.31 +    val message =
    5.32 +      (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
    5.33 +        gc_ratio ^ "% GC time, factor " ^ factor) handle Time => "";
    5.34 +  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
    5.35 +