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