1(* Title: Pure/General/timing.ML 2 Author: Makarius 3 4Basic support for time measurement. 5*) 6 7signature BASIC_TIMING = 8sig 9 val cond_timeit: bool -> string -> (unit -> 'a) -> 'a 10 val timeit: (unit -> 'a) -> 'a 11 val timeap: ('a -> 'b) -> 'a -> 'b 12 val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b 13end 14 15signature TIMING = 16sig 17 include BASIC_TIMING 18 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time} 19 type start 20 val start: unit -> start 21 val result: start -> timing 22 val timing: ('a -> 'b) -> 'a -> timing * 'b 23 val is_relevant_time: Time.time -> bool 24 val is_relevant: timing -> bool 25 val message: timing -> string 26 val protocol_message: string -> Position.T -> timing -> unit 27 val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b 28end 29 30structure Timing: TIMING = 31struct 32 33(* type timing *) 34 35type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}; 36 37 38(* timer control *) 39 40abstype start = Start of 41 Timer.real_timer * Time.time * Timer.cpu_timer * 42 {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}} 43with 44 45fun start () = 46 let 47 val real_timer = Timer.startRealTimer (); 48 val real_time = Timer.checkRealTimer real_timer; 49 val cpu_timer = Timer.startCPUTimer (); 50 val cpu_times = Timer.checkCPUTimes cpu_timer; 51 in Start (real_timer, real_time, cpu_timer, cpu_times) end; 52 53fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) = 54 let 55 val real_time2 = Timer.checkRealTimer real_timer; 56 val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; 57 val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = 58 Timer.checkCPUTimes cpu_timer; 59 60 val elapsed = real_time2 - real_time; 61 val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; 62 val cpu = usr2 - usr + sys2 - sys + gc; 63 in {elapsed = elapsed, cpu = cpu, gc = gc} end; 64 65end; 66 67fun timing f x = 68 let 69 val start = start (); 70 val y = f x; 71 in (result start, y) end; 72 73 74(* timing messages *) 75 76val min_time = Time.fromMilliseconds 1; 77 78fun is_relevant_time time = time >= min_time; 79 80fun is_relevant {elapsed, cpu, gc} = 81 is_relevant_time elapsed orelse 82 is_relevant_time cpu orelse 83 is_relevant_time gc; 84 85fun message {elapsed, cpu, gc} = 86 Value.print_time elapsed ^ "s elapsed time, " ^ 87 Value.print_time cpu ^ "s cpu time, " ^ 88 Value.print_time gc ^ "s GC time" handle Time.Time => ""; 89 90fun cond_timeit enabled msg e = 91 if enabled then 92 let 93 val (t, result) = timing (Exn.interruptible_capture e) (); 94 val _ = 95 if is_relevant t then 96 let val end_msg = message t 97 in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end 98 else (); 99 in Exn.release result end 100 else e (); 101 102fun timeit e = cond_timeit true "" e; 103fun timeap f x = timeit (fn () => f x); 104fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); 105 106fun protocol_message name pos t = 107 if is_relevant t then 108 let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos 109 in Output.try_protocol_message (props @ Markup.timing_properties t) [] end 110 else (); 111 112fun protocol name pos f x = 113 let 114 val (t, result) = timing (Exn.interruptible_capture f) x; 115 val _ = protocol_message name pos t; 116 in Exn.release result end; 117 118end; 119 120structure Basic_Timing: BASIC_TIMING = Timing; 121open Basic_Timing; 122