| 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. |