| 1 | | % (c) 2014-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | |
| 5 | | :- module(runtime_profiler,[reset_runtime_profiler/0, |
| 6 | | profile_failure_driven_loop/1, profile_failure_driven_loop/2, |
| 7 | | profile_single_call/2, profile_single_call/3, |
| 8 | | register_profiler_runtime/4, % manually register runtimes |
| 9 | | tcltk_get_profile_info/1, |
| 10 | | runtime_profile_available/0, |
| 11 | | print_runtime_profile/0, % called e.g. by -prob_profile |
| 12 | | |
| 13 | | runtime_observe_available/0, |
| 14 | | observe_runtime_wf/4, |
| 15 | | |
| 16 | | profile_recursion/3 |
| 17 | | ]). |
| 18 | | |
| 19 | | % TO DO: optionally load more precise microsecond timer |
| 20 | | |
| 21 | | :- use_module(module_information,[module_info/2]). |
| 22 | | :- module_info(group,profiling). |
| 23 | | :- module_info(description,'This module provides a simple runtime profiler.'). |
| 24 | | |
| 25 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 26 | | |
| 27 | | |
| 28 | | :- use_module(probsrc(kernel_waitflags),[add_message_wf/5]). |
| 29 | | :- use_module(preferences,[preference/2,get_preference/2]). |
| 30 | | :- use_module(probsrc(tools_strings),[ajoin/2]). |
| 31 | | runtime_observe_available :- preference(performance_monitoring_on,true). |
| 32 | | |
| 33 | | observe_runtime_wf(Start,Msg,Span,WF) :- |
| 34 | | preference(performance_monitoring_on,true), |
| 35 | | !, |
| 36 | | get_preference(performance_monitoring_expansion_limit,Limit), |
| 37 | | statistics(runtime,[End,_]), TotRuntime is End-Start, |
| 38 | | (TotRuntime>=Limit |
| 39 | | -> ajoin([TotRuntime,' ms'],Time), |
| 40 | | add_message_wf(delay,Msg,Time,Span,WF) |
| 41 | | ; true). |
| 42 | | observe_runtime_wf(_StartMs,_Msg,_,_). |
| 43 | | |
| 44 | | :- dynamic recursion_level/1. |
| 45 | | % TO DO: use counter |
| 46 | | recursion_level(0). |
| 47 | | inc_recur(X) :- retract(recursion_level(X)), X1 is X+1, |
| 48 | | assertz(recursion_level(X1)). |
| 49 | | dec_recur(X) :- retract(recursion_level(X1)), X is X1-1, |
| 50 | | assertz(recursion_level(X)). |
| 51 | | reset_recur(X) :- retract(recursion_level(_)), assertz(recursion_level(X)). |
| 52 | | :- meta_predicate profile_recursion(0,+,+). |
| 53 | | profile_recursion(Call,Name,Arg) :- |
| 54 | | inc_recur(X), |
| 55 | | statistics(walltime,[Start,_]), |
| 56 | | indent(X),format('>> ~w,~w,~w ms (ENTER),~w~n',[X1,Name,Start,Arg]), |
| 57 | | call_cleanup(Call, |
| 58 | | (statistics(walltime,[End,_]), Tot is End-Start, |
| 59 | | indent(X),format('<< ~w,~w,~w ms (EXIT)~n',[X1,Name,Tot]), |
| 60 | | reset_recur(X) |
| 61 | | )). |
| 62 | | indent(0) :- !. |
| 63 | | indent(N) :- N>0,!, N1 is N-1, print(' '), indent(N1). |
| 64 | | |
| 65 | | :- if(\+ environ(prob_profile, true)). |
| 66 | | |
| 67 | | reset_runtime_profiler. |
| 68 | | :- meta_predicate profile_single_call(-,-,0). |
| 69 | ? | profile_single_call(_Label,_ID,C) :- call(C). |
| 70 | | :- meta_predicate profile_single_call(-,0). |
| 71 | | profile_single_call(_Label,C) :- call(C). |
| 72 | | register_profiler_runtime(_,_,_,_). |
| 73 | | profile_failure_driven_loop(_). |
| 74 | | profile_failure_driven_loop(_,_). |
| 75 | | print_runtime_profile :- |
| 76 | | print('No runtime profiling information available'),nl, |
| 77 | | print('Recompile ProB with -Dprob_profile=true'),nl. |
| 78 | | tcltk_get_profile_info(list([I1,I2])) :- |
| 79 | | I1='No runtime profiling information available', |
| 80 | | I2='Recompile ProB with -Dprob_profile=true'. |
| 81 | | runtime_profile_available :- fail. |
| 82 | | |
| 83 | | :- else. |
| 84 | | runtime_profile_available. |
| 85 | | |
| 86 | | :- volatile total_runtime/7. |
| 87 | | :- dynamic total_runtime/7. |
| 88 | | |
| 89 | | reset_runtime_profiler :- % print('RESET '),nl, print_runtime_profile, |
| 90 | | retractall(total_runtime(_,_,_,_,_,_,_)). |
| 91 | | |
| 92 | | :- use_module(eventhandling,[register_event_listener/3]). |
| 93 | | :- register_event_listener(clear_specification,reset_runtime_profiler, |
| 94 | | 'Reset runtime profiler.'). |
| 95 | | |
| 96 | | :- meta_predicate profile_single_call(-,-,0). |
| 97 | | profile_single_call(Label,ID,C) :- |
| 98 | | start_profile(Label,StartInfo), |
| 99 | | if(call(C),stop_profile(Label,ID,StartInfo),(stop_profile(Label,ID,StartInfo),fail)). |
| 100 | | |
| 101 | | :- meta_predicate profile_single_call(-,0). |
| 102 | | profile_single_call(Label,C) :- profile_single_call(Label,unknown,C). |
| 103 | | |
| 104 | | |
| 105 | | % register runtime for a failure driven loop: |
| 106 | | profile_failure_driven_loop(ActionName) :- profile_failure_driven_loop(ActionName,unknown). |
| 107 | | profile_failure_driven_loop(ActionName,StateID) :- |
| 108 | | start_profile(ActionName,Info), |
| 109 | | %format('Start Action ----> ~w (~w)~n',[ActionName,Info]), |
| 110 | | register_time(ActionName,StateID,Info). |
| 111 | | register_time(_,_,_). |
| 112 | | register_time(AN,StateID,Info) :- |
| 113 | | stop_profile(AN,StateID,Info), |
| 114 | | fail. |
| 115 | | |
| 116 | | start_profile(_Label,[RT1,WT1]) :- |
| 117 | | statistics(runtime,[RT1,_Delta]), |
| 118 | | statistics(walltime,[WT1,_]). |
| 119 | | % inc_recur(X), indent(X), format('>> ~w, ~w, ~w ms (ENTER)~n',[X,_Label,WT1]). |
| 120 | | stop_profile(Label,StateID,[RT1,WT1]) :- |
| 121 | | statistics(runtime,[RT2,_]), |
| 122 | | statistics(walltime,[WT2,_]), |
| 123 | | DRT is RT2-RT1, DWT is WT2-WT1, |
| 124 | | %dec_recur(X),indent(X), format('<< ~w, ~w, ~w ms (EXIT)~n',[X,Label,DWT]), |
| 125 | | %format('Runtime for ~w : ~w ms (~w wall)~n',[AN,DRT,DWT]), |
| 126 | | register_profiler_runtime(Label,StateID,DRT,DWT). |
| 127 | | |
| 128 | | % register_profiler_runtime(Label,StateID,DeltaRunTime,DeltaWallTime) |
| 129 | | %register_profiler_runtime(_,_,0,0) :- !. % comment out if you want to count all calls |
| 130 | | register_profiler_runtime(PP,ID,RTime,WTime) :- |
| 131 | | (var(PP) -> PP2='unknown' ; PP2 = PP), |
| 132 | | (retract(total_runtime(PP2,OldR,OldW,Calls,Max,MaxID,Min)) |
| 133 | | -> true ; OldR=0,OldW=0,Max=0,MaxID=unknown,Calls=0,Min=inf), |
| 134 | | ((RTime<0 ; WTime <0) -> print(negative_runtime(PP,ID,RTime,WTime)),nl ; true), |
| 135 | | NewR is OldR+RTime, NewW is OldW+WTime, NewCalls is Calls+1, |
| 136 | | (WTime > Max -> NewMax = WTime, NewMaxID=ID ; NewMax = Max, NewMaxID=MaxID), |
| 137 | | (number(Min), Min < WTime -> NewMin = Min ; NewMin = WTime), |
| 138 | | assertz(total_runtime(PP2,NewR,NewW,NewCalls,NewMax,NewMaxID,NewMin)). |
| 139 | | |
| 140 | | |
| 141 | | :- use_module(library(lists)). |
| 142 | | print_runtime_profile :- |
| 143 | | format('---- ProB Runtime Profiler ----~n',[]), |
| 144 | | format('---- Tracks time spent in B operations and invariant evaluation~n',[]), |
| 145 | | format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n',['Operation','Total Runtime','Total','Minimum','Maximum','Number of Calls']), |
| 146 | | findall(profile(RT,WT,Calls,MaxWT,PP,MaxID,Min),total_runtime(PP,RT,WT,Calls,MaxWT,MaxID,Min),List), |
| 147 | | sort(List,SL), |
| 148 | | reverse(SL,RSL), |
| 149 | | maplist(print_runtime_profile_info,RSL), |
| 150 | | findall(WT2,total_runtime(_PP1,_RT1,WT2,_Calls,_MaxWT1,_MaxID1,_),WList), |
| 151 | | sumlist(WList,TotalWT), |
| 152 | | findall(Calls2,total_runtime(_PP2,_RT2,WT2,Calls2,_MaxWT2,_MaxID2,_),WList2), |
| 153 | | sumlist(WList2,TotalCalls), |
| 154 | | format(' Total Walltime: ~w ms for #calls ~w~n',[TotalWT,TotalCalls]). |
| 155 | | |
| 156 | | print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,unknown,Min)) :- |
| 157 | | format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n',[PP,RT,WT,Min,MaxWT,NrCalls]). |
| 158 | | print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,MaxID,Min)) :- |
| 159 | | format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime (max for ~w); #calls ~w)~n',[PP,RT,WT,Min,MaxWT,MaxID,NrCalls]). |
| 160 | | |
| 161 | | tcltk_get_profile_info(list([list(['Operation Name','Total Runtime (ms)','Total Walltime (ms)','# Calls','Max. Walltime (ms)','Max. Witness ID', 'Min. Walltime (ms)'])|L])) :- |
| 162 | | findall(profile(RT,WT,Calls,MaxWT,AN,MaxWitnessID,Min),total_runtime(AN,RT,WT,Calls,MaxWT,MaxWitnessID,Min),List), |
| 163 | | sort(List,SL), |
| 164 | | reverse(SL,RSL), |
| 165 | | print(RSL),nl, |
| 166 | | maplist(get_profile_list,RSL,L). |
| 167 | | |
| 168 | | :- use_module(probsrc(tools_meta),[translate_term_into_atom/2]). |
| 169 | | get_profile_list(profile(RT,WT,Calls,MaxWT,AN,MaxID,Min),list([OpName,RT,WT,Calls,MaxWT,MaxID,Min])) :- |
| 170 | | translate_term_into_atom(AN,OpName). |
| 171 | | |
| 172 | | |
| 173 | | :- endif. |