| 1 | | % (c) 2014-2025 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, profile_single_call/4, |
| 8 | | register_profiler_runtime/5, % manually register runtimes |
| 9 | | tcltk_get_profile_info/1, tcltk_get_profile_info/2, |
| 10 | | tcltk_get_multiple_profile_infos/2, |
| 11 | | tcltk_get_operations_profile_info/1, tcltk_get_constants_profile_info/1, |
| 12 | | tcltk_dot_constants_profile_info/1, |
| 13 | | runtime_profile_available/0, |
| 14 | | print_runtime_profile/0, % called e.g. by -prob_profile |
| 15 | | |
| 16 | | start_profile/2, opt_stop_profile/5, stop_profile/4, |
| 17 | | stop_constant_profile/5, |
| 18 | | constants_profiling_on/0, |
| 19 | | |
| 20 | | runtime_observe_available/0, |
| 21 | | observe_runtime_wf/4, |
| 22 | | |
| 23 | | profile_recursion/3 |
| 24 | | ]). |
| 25 | | |
| 26 | | % TO DO: optionally load more precise microsecond timer |
| 27 | | |
| 28 | | :- use_module(module_information,[module_info/2]). |
| 29 | | :- module_info(group,profiling). |
| 30 | | :- module_info(description,'This module provides a simple runtime profiler.'). |
| 31 | | |
| 32 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 33 | | |
| 34 | | |
| 35 | | :- use_module(probsrc(kernel_waitflags),[add_message_wf/5, get_waitflags_phase/2, get_call_stack/2]). |
| 36 | | :- use_module(preferences,[preference/2,get_preference/2]). |
| 37 | | :- use_module(probsrc(tools_strings),[ajoin/2]). |
| 38 | | runtime_observe_available :- preference(performance_monitoring_on,true). |
| 39 | | |
| 40 | | observe_runtime_wf(Timer,Msg,Span,WF) :- |
| 41 | | preference(performance_monitoring_on,true), |
| 42 | | Timer = [Start,WStart], |
| 43 | | !, |
| 44 | | get_preference(performance_monitoring_expansion_limit,Limit), |
| 45 | | statistics(runtime,[End,_]), TotRuntime is End-Start, |
| 46 | | statistics(walltime,[WEnd,_]), TotWalltime is WEnd-WStart, |
| 47 | | (TotWalltime>=Limit |
| 48 | | -> ajoin([TotWalltime,' ms'],Time), |
| 49 | | add_message_wf(delay,Msg,Time,Span,WF), |
| 50 | | (get_call_stack(WF,Stack), |
| 51 | | member(id_equality_evaluation(ID,constant,_Pos),Stack), |
| 52 | | write(id(ID)),nl, |
| 53 | | get_waitflags_phase(WF,Phase), |
| 54 | | Cat = constant_computation(Phase,[long_closure_expansion]), |
| 55 | | register_profiler_runtime(ID,Cat,unknown,TotRuntime,TotWalltime), |
| 56 | | fail ; true) |
| 57 | | ; true). |
| 58 | | observe_runtime_wf(_StartMs,_Msg,_,_). |
| 59 | | |
| 60 | | :- dynamic recursion_level/1. |
| 61 | | % TO DO: use counter |
| 62 | | recursion_level(0). |
| 63 | | inc_recur(X) :- retract(recursion_level(X)), X1 is X+1, |
| 64 | | assertz(recursion_level(X1)). |
| 65 | | dec_recur(X) :- retract(recursion_level(X1)), X is X1-1, |
| 66 | | assertz(recursion_level(X)). |
| 67 | | reset_recur(X) :- retract(recursion_level(_)), assertz(recursion_level(X)). |
| 68 | | :- meta_predicate profile_recursion(0,+,+). |
| 69 | | profile_recursion(Call,Name,Arg) :- |
| 70 | | inc_recur(X), |
| 71 | | statistics(walltime,[Start,_]), |
| 72 | | indent(X),format('>> ~w,~w,~w ms (ENTER),~w~n',[X1,Name,Start,Arg]), |
| 73 | | call_cleanup(Call, |
| 74 | | (statistics(walltime,[End,_]), Tot is End-Start, |
| 75 | | indent(X),format('<< ~w,~w,~w ms (EXIT)~n',[X1,Name,Tot]), |
| 76 | | reset_recur(X) |
| 77 | | )). |
| 78 | | indent(0) :- !. |
| 79 | | indent(N) :- N>0,!, N1 is N-1, print(' '), indent(N1). |
| 80 | | |
| 81 | | |
| 82 | | tcltk_get_profile_info(List) :- tcltk_get_profile_info(_,List). |
| 83 | | % can be generated from command-line using -csv prob_profile_info FILE |
| 84 | | tcltk_get_operations_profile_info(List) :- |
| 85 | | tcltk_get_profile_info(top_level,List). |
| 86 | | |
| 87 | | |
| 88 | | :- if(environ(prob_profile, false)). %used to be \+ environ(prob_profile, true)). |
| 89 | | % completely disable profiling |
| 90 | | reset_runtime_profiler. |
| 91 | | :- meta_predicate profile_single_call(-,-,-,0). |
| 92 | | profile_single_call(_Label,_Cat,_ID,C) :- call(C). |
| 93 | | :- meta_predicate profile_single_call(-,-,0). |
| 94 | | profile_single_call(_Label,_ID,C) :- call(C). |
| 95 | | :- meta_predicate profile_single_call(-,0). |
| 96 | | profile_single_call(_Label,C) :- call(C). |
| 97 | | register_profiler_runtime(_,_,_,_,_). |
| 98 | | profile_failure_driven_loop(_). |
| 99 | | profile_failure_driven_loop(_,_). |
| 100 | | print_runtime_profile :- |
| 101 | | print('No runtime profiling information available'),nl, |
| 102 | | print('Recompile ProB with -Dprob_profile=true'),nl. |
| 103 | | tcltk_get_profile_info(_,list([I1,I2])) :- |
| 104 | | I1='No runtime profiling information available', |
| 105 | | I2='Recompile ProB with -Dprob_profile=true'. |
| 106 | | tcltk_get_multiple_profile_infos(_,L) :- tcltk_get_profile_info(_,L). |
| 107 | | tcltk_get_constants_profile_info(List) :- tcltk_get_profile_info(_,List). |
| 108 | | runtime_profile_available :- fail. |
| 109 | | |
| 110 | | start_profile(_,_). |
| 111 | | stop_profile(_,_,_,_). |
| 112 | | opt_stop_profile(_,_,_,_,_). |
| 113 | | stop_constant_profile(_,_,_,_,_). |
| 114 | | constants_profiling_on :- fail. |
| 115 | | |
| 116 | | :- else. |
| 117 | | runtime_profile_available :- preference(prob_profiling_on,true). |
| 118 | | |
| 119 | | :- volatile total_runtime/8. |
| 120 | | :- dynamic total_runtime/8. |
| 121 | | |
| 122 | | reset_runtime_profiler :- % print('RESET '),nl, print_runtime_profile, |
| 123 | | retractall(total_runtime(_,_,_,_,_,_,_,_)). |
| 124 | | |
| 125 | | :- use_module(eventhandling,[register_event_listener/3]). |
| 126 | | :- register_event_listener(clear_specification,reset_runtime_profiler, |
| 127 | | 'Reset runtime profiler.'). |
| 128 | | |
| 129 | | :- meta_predicate profile_single_call(-,-,-,0). |
| 130 | ? | profile_single_call(_,_,_,Call) :- preference(prob_profiling_on,false), !, call(Call). |
| 131 | | profile_single_call(Label,Category,StateID,C) :- |
| 132 | | start_profile(Label,StartInfo), |
| 133 | | if(call(C), |
| 134 | | stop_profile(Label,Category,StateID,StartInfo), |
| 135 | | (stop_profile(Label,Category,StateID,StartInfo),fail)). |
| 136 | | |
| 137 | | :- meta_predicate profile_single_call(-,-,0). |
| 138 | ? | profile_single_call(Label,StateID,C) :- profile_single_call(Label,top_level,StateID,C). |
| 139 | | |
| 140 | | :- meta_predicate profile_single_call(-,0). |
| 141 | | profile_single_call(Label,C) :- profile_single_call(Label,top_level,unknown,C). |
| 142 | | |
| 143 | | |
| 144 | | % register runtime for a failure driven loop: |
| 145 | | profile_failure_driven_loop(ActionName) :- profile_failure_driven_loop(ActionName,unknown). |
| 146 | | |
| 147 | | profile_failure_driven_loop(_,_) :- preference(prob_profiling_on,false), !. |
| 148 | | profile_failure_driven_loop(ActionName,StateID) :- |
| 149 | | start_profile(ActionName,Info), |
| 150 | | %format('Start Action ----> ~w (~w)~n',[ActionName,Info]), |
| 151 | ? | register_time(ActionName,StateID,Info). |
| 152 | | register_time(_,_,_). |
| 153 | | register_time(AN,StateID,Info) :- |
| 154 | | stop_profile(AN,StateID,Info), |
| 155 | | fail. |
| 156 | | |
| 157 | | start_profile(_,P) :- preference(prob_profiling_on,false), !, P=[0,0]. |
| 158 | | start_profile(_Label,[RT1,WT1]) :- |
| 159 | | statistics(runtime,[RT1,_Delta]), |
| 160 | | statistics(walltime,[WT1,_]). |
| 161 | | % inc_recur(X), indent(X), format('>> ~w, ~w, ~w ms (ENTER)~n',[X,_Label,WT1]). |
| 162 | | |
| 163 | | stop_profile(Label,StateID,StartTimes) :- |
| 164 | | stop_profile(Label,top_level,StateID,StartTimes). |
| 165 | | |
| 166 | | stop_profile(_,_,_,_) :- preference(prob_profiling_on,false), !. |
| 167 | | stop_profile(Label,Category,StateID,[RT1,WT1]) :- |
| 168 | | statistics(runtime,[RT2,_]), |
| 169 | | statistics(walltime,[WT2,_]), |
| 170 | | DRT is RT2-RT1, DWT is WT2-WT1, |
| 171 | | %dec_recur(X),indent(X), format('<< ~w, ~w, ~w ms (EXIT)~n',[X,Label,DWT]), |
| 172 | | %format('Runtime for ~w : ~w ms (~w wall)~n',[Label:Category,DRT,DWT]), |
| 173 | | register_profiler_runtime(Label,Category,StateID,DRT,DWT). |
| 174 | | % now a version with an additional prefix context and only register values with a certain threshold |
| 175 | | opt_stop_profile(_,_,_,_,_) :- preference(prob_profiling_on,false), !. |
| 176 | | opt_stop_profile(Category,Label,StateID,[RT1,WT1],Threshold) :- |
| 177 | | statistics(walltime,[WT2,_]), DWT is WT2-WT1, DWT>=Threshold, |
| 178 | | !, |
| 179 | | statistics(runtime,[RT2,_]), |
| 180 | | DRT is RT2-RT1, |
| 181 | | register_profiler_runtime(Label,Category,StateID,DRT,DWT). |
| 182 | | opt_stop_profile(_,_,_,_,_). |
| 183 | | |
| 184 | | % register_profiler_runtime(Label,Category,StateID,DeltaRunTime,DeltaWallTime) |
| 185 | | register_profiler_runtime(_,_,_,_,_) :- preference(prob_profiling_on,false), !. |
| 186 | | %register_profiler_runtime(_,_,_,0,0) :- !. % comment out if you want to count all calls |
| 187 | | register_profiler_runtime(ProgramPoint,Category,StateID,RTime,WTime) :- |
| 188 | | (var(ProgramPoint) -> PP2='unknown' ; PP2 = ProgramPoint), |
| 189 | | (retract(total_runtime(PP2,Category,OldR,OldW,Calls,Max,MaxID,Min)) |
| 190 | | -> true |
| 191 | | ; OldR=0,OldW=0,Max=0,MaxID=StateID,Calls=0,Min=inf |
| 192 | | ), |
| 193 | | ((RTime<0 ; WTime <0) -> write(negative_runtime(PP2,StateID,RTime,WTime)),nl ; true), |
| 194 | | NewR is OldR+RTime, NewW is OldW+WTime, NewCalls is Calls+1, |
| 195 | | (WTime > Max -> NewMax = WTime, NewMaxID=StateID ; NewMax = Max, NewMaxID=MaxID), |
| 196 | | (number(Min), Min < WTime -> NewMin = Min ; NewMin = WTime), |
| 197 | | assertz(total_runtime(PP2,Category,NewR,NewW,NewCalls,NewMax,NewMaxID,NewMin)). |
| 198 | | |
| 199 | | |
| 200 | | |
| 201 | | constants_profiling_on :- preference(performance_monitoring_on,true). % TODO: maybe use other preference later |
| 202 | | |
| 203 | | stop_constant_profile(Val,Phase,ID,IDInfo,Timer) :- |
| 204 | | (get_value_info(Val,ValKind) -> IDInfo2 = [ValKind|IDInfo] ; IDInfo2=IDInfo), |
| 205 | | opt_stop_profile(constant_computation(Phase,IDInfo2),ID,root,Timer,0). |
| 206 | | |
| 207 | | get_value_info(Var,ValKind) :- var(Var),!, ValKind=variable. |
| 208 | | get_value_info(closure(_,_,_),ValKind) :- !, ValKind=symbolic. |
| 209 | | get_value_info(avl_set(_),ValKind) :- !, ValKind=avl_set. |
| 210 | | get_value_info(rec(_),ValKind) :- !, ValKind=record. |
| 211 | | get_value_info(int(_),ValKind) :- !, ValKind=integer. |
| 212 | | get_value_info(string(_),ValKind) :- !, ValKind=string. |
| 213 | | get_value_info(fd(_,GS),ValKind) :- !, ValKind=GS. |
| 214 | | get_value_info(freeval(_ID,_,_),ValKind) :- !, ValKind=freeval. |
| 215 | | get_value_info(pred_false,ValKind) :- !, ValKind=boolean. |
| 216 | | get_value_info(pred_true,ValKind) :- !, ValKind=boolean. |
| 217 | | get_value_info([],ValKind) :- !, ValKind=empty_set. |
| 218 | | get_value_info(O,other) :- functor(O,F,N), write(other(F,N)),nl,fail. |
| 219 | | |
| 220 | | % remove this from the info field, when we have a description about the constant value found (get_det_solution_for_constant_value_kind) |
| 221 | | is_value_info(avl_set). |
| 222 | | is_value_info(boolean). |
| 223 | | is_value_info(empty_set). |
| 224 | | is_value_info(freeval). |
| 225 | | is_value_info(integer). |
| 226 | | is_value_info(record). |
| 227 | | is_value_info(symbolic). |
| 228 | | is_value_info(string). |
| 229 | | |
| 230 | | |
| 231 | | translate_pp(PP,Cat,PPS) :- member(Cat,[top_level,external_functions,well_def_analyser]),!, |
| 232 | | translate_term_into_atom(PP,PPS). |
| 233 | | translate_pp(PP,constant_computation(Phase,IDInfo),PPS) :- !, |
| 234 | | ajoin([PP,'::',Phase,'::',IDInfo],PPS). % TODO: improve rendering of IDInfo |
| 235 | | translate_pp(PP,Category,PPS) :- ajoin([PP,'::',Category],PPS). |
| 236 | | |
| 237 | | |
| 238 | | relevant_total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min) :- |
| 239 | ? | total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min), |
| 240 | | \+ irrelevant_profile_entry(PP,Cat,WT). |
| 241 | | |
| 242 | | irrelevant_profile_entry(ID,constant_computation(Phase,IDInfo),0) :- |
| 243 | | Phase = propagate_value, % only show propagations if relevant runtime or instantiates something other than itself |
| 244 | | (member(instantiates(List),IDInfo) -> List = [ID] ; true). |
| 245 | | |
| 246 | | :- use_module(library(lists)). |
| 247 | | print_runtime_profile :- |
| 248 | | format('---- ProB Runtime Profiler ----~n',[]), |
| 249 | | format('---- Time spent in B operations and invariant evaluation~n',[]), |
| 250 | | (get_preference(prob_profiling_on,false) -> |
| 251 | | format('---- *** set preference PROFILING_INFO to TRUE to obtain more information!~n',[]) ; true), |
| 252 | | print_runtime_profile(top_level), |
| 253 | | |
| 254 | | format('---- Time spent evaluating CONSTANTS (defined by equations)~n',[]), |
| 255 | | (\+ constants_profiling_on -> |
| 256 | | format('---- *** set preference PERFORMANCE_INFO to TRUE to obtain more information!~n',[]) ; true), |
| 257 | | print_runtime_profile(constant_computation(_,_)), |
| 258 | | |
| 259 | ? | (opt_category(Category,_), |
| 260 | | \+ \+ total_runtime(_,Category,_,_,_,_,_,_), |
| 261 | | format('---- Time spent evaluating ~w~n',[Category]), |
| 262 | | print_runtime_profile(Category), |
| 263 | | fail |
| 264 | | ; |
| 265 | | true). |
| 266 | | |
| 267 | | opt_category(ast_cleanup,cleanup). |
| 268 | | opt_category(cache_load_constants,cache). |
| 269 | | opt_category(cache_load_constants_failed,cache). |
| 270 | | opt_category(cache_load_operations_index,cache). |
| 271 | | opt_category(cache_load_operations_index_failed,cache). |
| 272 | | opt_category(cache_hashing_input_values,cache). |
| 273 | | opt_category(cache_load_transitions,cache). |
| 274 | | opt_category(cache_store_transitions,cache). |
| 275 | | opt_category(external_functions,external). |
| 276 | | opt_category(well_def_analyser,wd). |
| 277 | | |
| 278 | | :- use_module(specfile,[get_specification_description/2]). |
| 279 | | get_category_call_name(top_level,N) :- !, |
| 280 | | get_specification_description(operation,N). % also shows invariants though |
| 281 | | get_category_call_name(external_functions,N) :- !, N='Function'. |
| 282 | | get_category_call_name(cache_hashing_input_values,N) :- !, N='Hash_Input'. |
| 283 | | get_category_call_name(cache_load_constants,N) :- !, N='Load_Constants'. |
| 284 | | get_category_call_name(cache_load_constants_failed,N) :- !, N='Load_Constants_KO'. |
| 285 | | get_category_call_name(cache_load_operations_index,N) :- !, N='Load_Operations_Index'. |
| 286 | | get_category_call_name(cache_load_operations_index_failed,N) :- !, N='Load_Operations_Index_KO'. |
| 287 | | get_category_call_name(cache_load_transitions,N) :- !, N='Load_Transition'. |
| 288 | | get_category_call_name(cache_store_transitions,N) :- !, N='Store'. |
| 289 | | get_category_call_name(_,N) :- !, N='Call'. |
| 290 | | |
| 291 | | |
| 292 | | print_runtime_profile(Cat) :- |
| 293 | | get_category_call_name(Cat,Col1Header), |
| 294 | | format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n', |
| 295 | | [Col1Header,'Total Runtime','Total','Minimum','Maximum','Number of Calls']), |
| 296 | | findall(profile(RT,WT,Calls,MaxWT,PP,Cat,MaxID,Min),relevant_total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min),List), |
| 297 | | sort(List,SL), |
| 298 | | reverse(SL,RSL), |
| 299 | | maplist(print_runtime_profile_info,RSL), |
| 300 | | findall(WT2,relevant_total_runtime(_PP1,Cat,_RT1,WT2,_Calls,_MaxWT1,_MaxID1,_),WList), |
| 301 | | sumlist(WList,TotalWT), |
| 302 | | findall(Calls2,relevant_total_runtime(_PP2,Cat,_RT2,WT2,Calls2,_MaxWT2,_MaxID2,_),WList2), |
| 303 | | sumlist(WList2,TotalCalls), |
| 304 | | format(' Total Walltime: ~w ms for #calls ~w~n',[TotalWT,TotalCalls]). |
| 305 | | |
| 306 | | print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,Cat,MaxID,Min)) :- |
| 307 | | translate_pp(PP,Cat,PPS), |
| 308 | | (MaxID=unknown |
| 309 | | -> format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n', |
| 310 | | [PPS,RT,WT,Min,MaxWT,NrCalls]) |
| 311 | | ; format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime (max for ~w); #calls ~w)~n', |
| 312 | | [PPS,RT,WT,Min,MaxWT,MaxID,NrCalls]) |
| 313 | | ). |
| 314 | | |
| 315 | | % get multiple profile info categories for a class like cache |
| 316 | | tcltk_get_multiple_profile_infos(Class,list(Result)) :- |
| 317 | | Sep = list(['-','-','-','-','-','-','-']), |
| 318 | | findall([Sep|L], (opt_category(C,Class), tcltk_get_profile_info(C,list(L))), Ls), |
| 319 | | append(Ls,Result). |
| 320 | | |
| 321 | | tcltk_get_profile_info(Category, |
| 322 | | list([list([Column1,'Total Runtime','Total Walltime', |
| 323 | | '# Calls','Max. Walltime','Max. Witness ID', 'Min. Walltime'])|L])) :- |
| 324 | | get_category_call_name(Category,Column1), |
| 325 | | findall(profile(RT,WT,Calls,MaxWT,AN,Category,MaxWitnessID,Min), |
| 326 | | relevant_total_runtime(AN,Category,RT,WT,Calls,MaxWT,MaxWitnessID,Min),List), |
| 327 | | sort(List,SL), |
| 328 | | reverse(SL,RSL), |
| 329 | | maplist(get_profile_list,RSL,L). |
| 330 | | |
| 331 | | :- use_module(probsrc(tools_meta),[translate_term_into_atom/2]). |
| 332 | | get_profile_list(profile(RT,WT,Calls,MaxWT,AN,Cat,MaxID,Min),list([PPS,RT,WT,Calls,MaxWT,MaxID,Min])) :- |
| 333 | | translate_pp(AN,Cat,PPS). |
| 334 | | |
| 335 | | :- use_module(state_space,[try_get_unique_constants_state/1, |
| 336 | | is_concrete_constants_state_id/1, is_initial_state_id/1]). |
| 337 | | % can be generated from command-line using -csv prob_constants_profile_info FILE |
| 338 | | tcltk_get_constants_profile_info( |
| 339 | | list([list(['Constant','Kind','@desc', |
| 340 | | 'Computation Runtime (ms)', |
| 341 | | 'Computation Walltime (ms)', 'Propagation Walltime (ms)', |
| 342 | | '# Calls','Other Infos', 'Valued','Det.Value','Instantiates'])|ResL])) :- |
| 343 | | (is_concrete_constants_state_id(_) -> |
| 344 | | (constants_profiling_on -> ResL = L ; ResL = [['Set PROFILING_INFO and PERFORMANCE_INFO preference to TRUE for full infos.']|L]) |
| 345 | | ; is_initial_state_id(_) -> ResL = [['The machine has no constants to analyse!']|L] |
| 346 | | ; ResL = [['No constants values computed yet. SETUP_CONSTANTS first!']|L]), |
| 347 | | findall(ProfileTerm, relevant_cst_profile_entry(ProfileTerm),List), |
| 348 | | sort(List,SL), |
| 349 | | reverse(SL,RSL), |
| 350 | | maplist(get_cprofile_list,RSL,L). |
| 351 | | |
| 352 | | % Legend: |
| 353 | | % Computation Runtime & Walltime: time spent computing the constant defined by an equation |
| 354 | | % Propagation Walltime: time spent evaluating predicates and possibly evaluation dependent values |
| 355 | | % #Calls: should probably be 1 here, unless the constants are non-deterministic |
| 356 | | % Other Infos: avl_set, variable, symbolic, marked_as_expand, automatic_expand, marked_as_symbolic |
| 357 | | % long_closure_expansion: this may only count part of the time spent |
| 358 | | % phase1: this computation occured in the second half of the deterministic propagation phase |
| 359 | | % grounding: this computation occured after the determinate propagation phase of ProB |
| 360 | | % automatic_expand: abstract constant detected to be computed automatically |
| 361 | | % marked_as_expand: constant marked with expand pragma |
| 362 | | % Valued: yes: equation determined value straight away, delayed: was computed in phase0 but required more info, non-det was valued but in non-det phase, NO: no value info available |
| 363 | | % Det. Value: value computed in deterministic propagation phase, or unique value found |
| 364 | | % Instantiates: computing that value triggered computation of this list of other constants |
| 365 | | |
| 366 | | :- use_module(bmachine, [constant_variable_marked_as_memo/1, constant_variable_marked_as_expand/1]). |
| 367 | | :- use_module(b_interpreter_components,[get_det_solution_for_constant_value_kind/2]). |
| 368 | | :- use_module(b_machine_hierarchy,[abstract_constant/2, concrete_constant/2]). |
| 369 | | :- use_module(translate,[translate_bvalue_kind/2]). |
| 370 | | relevant_cst_profile_entry(cprofile(RT,WT,PropWT,Calls,PP,Kind,Ann,Phase,IDInfo,InstItself,ValInfo,InstList)) :- |
| 371 | | (try_get_unique_constants_state(CstState) -> true ; CstState=[]), |
| 372 | | (Category = constant_computation(Phase,IDInfo0), |
| 373 | | relevant_total_runtime(PP,Category,RT,WT,Calls,_MaxWT,_MaxWitnessID,_Min), |
| 374 | | Phase \= propagate_value, |
| 375 | | (abstract_constant(PP,_) -> Kind=abstract ; concrete_constant(PP,_) -> Kind=concrete ; Kind=unknown) |
| 376 | | ; |
| 377 | | (constants_profiling_on -> Phase = no_equation_detected |
| 378 | | ; Phase = '-'), % constants profiling on needed to keep track of all equations (except arith. at the moment) |
| 379 | | RT=0, WT=0, PropWT=0, Calls=0, IDInfo0 = [], |
| 380 | | (abstract_constant(PP,_), Kind=abstract ; concrete_constant(PP,_), Kind=concrete), |
| 381 | | \+ total_runtime(PP,constant_computation(_,_),_,_,_,_,_,_) % we have no profiling info at all for PP |
| 382 | | ), |
| 383 | | (get_det_solution_for_constant_value_kind(PP,DetValInfo) |
| 384 | | -> DetSolFound = true, |
| 385 | | exclude(is_value_info,IDInfo0,IDInfo) |
| 386 | | ; DetValInfo = '-', |
| 387 | | DetSolFound = false, IDInfo0=IDInfo |
| 388 | | ), |
| 389 | | ( (DetSolFound=false ; DetValInfo='LARGE-VALUE'), |
| 390 | | member(bind(PP,CstVal),CstState), translate_bvalue_kind(CstVal,ValInfo) |
| 391 | | -> SolFound=true |
| 392 | | ; ValInfo=DetValInfo, SolFound=DetSolFound |
| 393 | | ), |
| 394 | | % now check whether there are infos about propagation phase: |
| 395 | | (total_runtime(PP,constant_computation(propagate_value,PropInfo),_,PropWT,_,_,_,_) |
| 396 | | -> (member(instantiates(IList),PropInfo) -> |
| 397 | | (select(PP,IList,InstList) |
| 398 | | -> InstItself=yes, % Equation determined directly the value |
| 399 | | % check if we have a long closure expansion entry |
| 400 | | % this has already been counted in the regular entry for the constant computation |
| 401 | | (member(long_closure_expansion,IDInfo), Phase=phase0 -> fail ; true) |
| 402 | | ; (DetSolFound=true -> InstItself = 'delayed' |
| 403 | | ; SolFound=true -> InstItself = 'non-det' |
| 404 | | ; InstItself='NO'), |
| 405 | | InstList=IList) |
| 406 | | ; % no instantiation list stored; performance monitoring not on |
| 407 | | (SolFound=true -> InstItself='-' ; InstItself='NO'), |
| 408 | | InstList = '-' |
| 409 | | ) |
| 410 | | ; PropWT = 0, |
| 411 | | (DetSolFound=true -> InstItself='-' ; InstItself='NO'), |
| 412 | | InstList='-' |
| 413 | | ), |
| 414 | | (constant_variable_marked_as_expand(PP) -> Ann=expand |
| 415 | | ; constant_variable_marked_as_memo(PP) -> Ann=memo |
| 416 | | ; Ann = '' |
| 417 | | ). |
| 418 | | |
| 419 | | get_cprofile_list(cprofile(RT,WT,PropWT,Calls,PP,Kind,Ann,Phase,IDInfo0,InstItself,DetVal,IList), |
| 420 | | list([PP,Kind,Ann,RT,WT,PropWT,Calls,IDInfo,InstItself,DetVal,IList])) :- |
| 421 | | (Phase = phase0 -> IDInfo = IDInfo0 ; IDInfo = [Phase|IDInfo0]). |
| 422 | | % phase: phase0, phase1, grounding, enumeration_finished (from get_waitflags_phase) |
| 423 | | |
| 424 | | |
| 425 | | :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3]). |
| 426 | | % can be generated from command-line using -dot constants_profile_graph FILE |
| 427 | | % TODO: improve rendering and then enable in meta_interface |
| 428 | | tcltk_dot_constants_profile_info(File) :- |
| 429 | | gen_dot_graph(File,constant_profile_predicate,constant_instantiates). |
| 430 | | |
| 431 | | constant_profile_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none, |
| 432 | | Category = constant_computation(Phase,_Infos), |
| 433 | | total_runtime(NodeID,Category,_RT,WT,_Calls,_MaxWT,_MaxWitnessID,_Min), |
| 434 | | (abstract_constant(NodeID,_) -> Kind=abstract ; Kind=concrete), |
| 435 | | Phase \= propagate_value, |
| 436 | | Shape = box, |
| 437 | | (total_runtime(NodeID,constant_computation(propagate_value,_),_,WT2,_,_,_,_) |
| 438 | | -> ajoin([NodeID,'\\n ',Kind,'\\n ',Phase,'\\n',WT, ' ms','\\n + ',WT2, ' ms'],NodeDesc) |
| 439 | | ; ajoin([NodeID,'\\n ',Kind,'\\n ',Phase,'\\n',WT, ' ms'],NodeDesc) |
| 440 | | ), |
| 441 | | Style='rounded', Color=gray90. |
| 442 | | |
| 443 | | constant_instantiates(NodeID,Label,SuccID,Color,Style) :- |
| 444 | | Color=red4, Style=solid, Label = 'inst', |
| 445 | | Category = constant_computation(Phase,Infos), Phase = propagate_value, |
| 446 | | total_runtime(NodeID,Category,_RT,_WT,_Calls,_MaxWT,_MaxWitnessID,_Min), |
| 447 | | member(instantiates(List),Infos), |
| 448 | | member(SuccID,List), SuccID \= NodeID. |
| 449 | | |
| 450 | | |
| 451 | | :- endif. |