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		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]).
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(Start,Msg,Span,WF) :-
40		preference(performance_monitoring_on,true),
41		!,
42		get_preference(performance_monitoring_expansion_limit,Limit),
43		statistics(runtime,[End,_]), TotRuntime is End-Start,
44		(TotRuntime>=Limit
45		-> ajoin([TotRuntime,' ms'],Time),
46		add_message_wf(delay,Msg,Time,Span,WF)
47		; true).
48		observe_runtime_wf(_StartMs,_Msg,_,_).
49
50		:- dynamic recursion_level/1.
51		% TO DO: use counter
52		recursion_level(0).
53		inc_recur(X) :- retract(recursion_level(X)), X1 is X+1,
54		assertz(recursion_level(X1)).
55		dec_recur(X) :- retract(recursion_level(X1)), X is X1-1,
56		assertz(recursion_level(X)).
57		reset_recur(X) :- retract(recursion_level(_)), assertz(recursion_level(X)).
58		:- meta_predicate profile_recursion(0,+,+).
59		profile_recursion(Call,Name,Arg) :-
60		inc_recur(X),
61		statistics(walltime,[Start,_]),
62		indent(X),format('>> ~w,~w,~w ms (ENTER),~w~n',[X1,Name,Start,Arg]),
63		call_cleanup(Call,
64		(statistics(walltime,[End,_]), Tot is End-Start,
65		indent(X),format('<< ~w,~w,~w ms (EXIT)~n',[X1,Name,Tot]),
66		reset_recur(X)
67		)).
68		indent(0) :- !.
69		indent(N) :- N>0,!, N1 is N-1, print(' '), indent(N1).
70
71
72		tcltk_get_profile_info(List) :- tcltk_get_profile_info(_,List).
73		% can be generated from command-line using -csv prob_profile_info FILE
74		tcltk_get_operations_profile_info(List) :-
75		tcltk_get_profile_info(top_level,List).
76
77
78		:- if(environ(prob_profile, false)). %used to be \+ environ(prob_profile, true)).
79		% completely disable profiling
80		reset_runtime_profiler.
81		:- meta_predicate profile_single_call(-,-,0).
82		profile_single_call(_Label,_ID,C) :- call(C).
83		:- meta_predicate profile_single_call(-,0).
84		profile_single_call(_Label,C) :- call(C).
85		register_profiler_runtime(_,_,_,_).
86		profile_failure_driven_loop(_).
87		profile_failure_driven_loop(_,_).
88		print_runtime_profile :-
89		print('No runtime profiling information available'),nl,
90		print('Recompile ProB with -Dprob_profile=true'),nl.
91		tcltk_get_profile_info(_,list([I1,I2])) :-
92		I1='No runtime profiling information available',
93		I2='Recompile ProB with -Dprob_profile=true'.
94		tcltk_get_constants_profile_info(List) :- tcltk_get_profile_info(_,List).
95		runtime_profile_available :- fail.
96
97		start_profile(_,_).
98		stop_profile(_,_,_).
99		opt_stop_profile(_,_,_,_,_).
100		stop_constant_profile(_,_,_,_,_).
101		constants_profiling_on :- fail.
102
103		:- else.
104		runtime_profile_available :- preference(prob_profiling_on,true).
105
106		:- volatile total_runtime/8.
107		:- dynamic total_runtime/8.
108
109		reset_runtime_profiler :- % print('RESET '),nl, print_runtime_profile,
110		retractall(total_runtime(_,_,_,_,_,_,_,_)).
111
112		:- use_module(eventhandling,[register_event_listener/3]).
113		:- register_event_listener(clear_specification,reset_runtime_profiler,
114		'Reset runtime profiler.').
115
116		:- meta_predicate profile_single_call(-,-,0).
117	?	profile_single_call(_,_,Call) :- preference(prob_profiling_on,false), !, call(Call).
118		profile_single_call(Label,ID,C) :-
119		start_profile(Label,StartInfo),
120		if(call(C),stop_profile(Label,ID,StartInfo),(stop_profile(Label,ID,StartInfo),fail)).
121
122		:- meta_predicate profile_single_call(-,0).
123		profile_single_call(Label,C) :- profile_single_call(Label,unknown,C).
124
125
126		% register runtime for a failure driven loop:
127		profile_failure_driven_loop(ActionName) :- profile_failure_driven_loop(ActionName,unknown).
128
129		profile_failure_driven_loop(_,_) :- preference(prob_profiling_on,false), !.
130		profile_failure_driven_loop(ActionName,StateID) :-
131		start_profile(ActionName,Info),
132		%format('Start Action ----> ~w (~w)~n',[ActionName,Info]),
133		register_time(ActionName,StateID,Info).
134		register_time(_,_,_).
135		register_time(AN,StateID,Info) :-
136		stop_profile(AN,StateID,Info),
137		fail.
138
139		start_profile(_,P) :- preference(prob_profiling_on,false), !, P=[0,0].
140		start_profile(_Label,[RT1,WT1]) :-
141		statistics(runtime,[RT1,_Delta]),
142		statistics(walltime,[WT1,_]).
143		% inc_recur(X), indent(X), format('>> ~w, ~w, ~w ms (ENTER)~n',[X,_Label,WT1]).
144		stop_profile(_,_,_) :- preference(prob_profiling_on,false), !.
145		stop_profile(Label,StateID,[RT1,WT1]) :-
146		statistics(runtime,[RT2,_]),
147		statistics(walltime,[WT2,_]),
148		DRT is RT2-RT1, DWT is WT2-WT1,
149		%dec_recur(X),indent(X), format('<< ~w, ~w, ~w ms (EXIT)~n',[X,Label,DWT]),
150		%format('Runtime for ~w : ~w ms (~w wall)~n',[AN,DRT,DWT]),
151		register_profiler_runtime(Label,StateID,DRT,DWT).
152		% now a version with an additional prefix context and only register values with a certain threshold
153		opt_stop_profile(_,_,_,_,_) :- preference(prob_profiling_on,false), !.
154		opt_stop_profile(Category,Label,StateID,[RT1,WT1],Threshold) :-
155		statistics(walltime,[WT2,_]), DWT is WT2-WT1, DWT>=Threshold,
156		!,
157		statistics(runtime,[RT2,_]),
158		DRT is RT2-RT1,
159		register_profiler_runtime(Label,Category,StateID,DRT,DWT).
160		opt_stop_profile(_,_,_,_,_).
161
162		% register_profiler_runtime(Label,StateID,DeltaRunTime,DeltaWallTime)
163		%register_profiler_runtime(_,_,0,0) :- !. % comment out if you want to count all calls
164		register_profiler_runtime(_,_,_,_) :- preference(prob_profiling_on,false), !.
165		register_profiler_runtime(PP,ID,RTime,WTime) :-
166		register_profiler_runtime(PP,top_level,ID,RTime,WTime).
167		register_profiler_runtime(ProgramPoint,Category,StateID,RTime,WTime) :-
168		(var(ProgramPoint) -> PP2='unknown' ; PP2 = ProgramPoint),
169		(retract(total_runtime(PP2,Category,OldR,OldW,Calls,Max,MaxID,Min))
170		-> true
171		; OldR=0,OldW=0,Max=0,MaxID=StateID,Calls=0,Min=inf
172		),
173		((RTime<0 ; WTime <0) -> print(negative_runtime(PP2,StateID,RTime,WTime)),nl ; true),
174		NewR is OldR+RTime, NewW is OldW+WTime, NewCalls is Calls+1,
175		(WTime > Max -> NewMax = WTime, NewMaxID=StateID ; NewMax = Max, NewMaxID=MaxID),
176		(number(Min), Min < WTime -> NewMin = Min ; NewMin = WTime),
177		assertz(total_runtime(PP2,Category,NewR,NewW,NewCalls,NewMax,NewMaxID,NewMin)).
178
179
180
181		constants_profiling_on :- preference(performance_monitoring_on,true). % TODO: maybe use other preference later
182
183		stop_constant_profile(Val,Phase,ID,IDInfo,Timer) :-
184		(get_value_info(Val,ValKind) -> IDInfo2 = [ValKind|IDInfo] ; IDInfo2=IDInfo),
185		opt_stop_profile(constant_computation(Phase,IDInfo2),ID,root,Timer,0).
186
187		get_value_info(Var,ValKind) :- var(Var),!, ValKind=variable.
188		get_value_info(closure(_,_,_),ValKind) :- !, ValKind=symbolic.
189		get_value_info(avl_set(_),ValKind) :- !, ValKind=avl_set.
190		get_value_info(rec(_),ValKind) :- !, ValKind=record.
191		get_value_info(int(_),ValKind) :- !, ValKind=integer.
192		get_value_info(string(_),ValKind) :- !, ValKind=string.
193		get_value_info(fd(_,GS),ValKind) :- !, ValKind=GS.
194		get_value_info(freeval(_ID,_,_),ValKind) :- !, ValKind=freeval.
195		get_value_info(pred_false,ValKind) :- !, ValKind=boolean.
196		get_value_info(pred_true,ValKind) :- !, ValKind=boolean.
197		get_value_info([],ValKind) :- !, ValKind=empty_set.
198		get_value_info(O,other) :- functor(O,F,N), write(other(F,N)),nl,fail.
199
200
201		translate_pp(PP,top_level,PPS) :- !, translate_term_into_atom(PP,PPS).
202		translate_pp(PP,constant_computation(Phase,IDInfo),PPS) :- !,
203		ajoin([PP,'::',Phase,'::',IDInfo],PPS). % TODO: improve rendering of IDInfo
204		translate_pp(PP,Category,PPS) :- ajoin([PP,'::',Category],PPS).
205
206		relevant_total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min) :-
207		total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min),
208		\+ irrelevant_profile_entry(PP,Cat,WT).
209
210		irrelevant_profile_entry(ID,constant_computation(Phase,IDInfo),0) :-
211		Phase = propagate_value, % only show propagations if relevant runtime or instantiates something other than itself
212		(member(instantiates(List),IDInfo) -> List = [ID] ; true).
213
214		:- use_module(library(lists)).
215		print_runtime_profile :-
216		format('---- ProB Runtime Profiler ----~n',[]),
217		format('---- Time spent in B operations and invariant evaluation~n',[]),
218		(get_preference(prob_profiling_on,false) ->
219		format('---- *** set preference PROFILING_INFO to TRUE to obtain more information!~n',[]) ; true),
220		print_runtime_profile(top_level),
221
222		format('---- Time spent evaluating CONSTANTS (defined by equations)~n',[]),
223		print_runtime_profile(constant_computation(_,_)).
224		print_runtime_profile(Cat) :-
225		format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n',['Operation','Total Runtime','Total','Minimum','Maximum','Number of Calls']),
226		findall(profile(RT,WT,Calls,MaxWT,PP,Cat,MaxID,Min),relevant_total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min),List),
227		sort(List,SL),
228		reverse(SL,RSL),
229		maplist(print_runtime_profile_info,RSL),
230		findall(WT2,relevant_total_runtime(_PP1,Cat,_RT1,WT2,_Calls,_MaxWT1,_MaxID1,_),WList),
231		sumlist(WList,TotalWT),
232		findall(Calls2,relevant_total_runtime(_PP2,Cat,_RT2,WT2,Calls2,_MaxWT2,_MaxID2,_),WList2),
233		sumlist(WList2,TotalCalls),
234		format(' Total Walltime: ~w ms for #calls ~w~n',[TotalWT,TotalCalls]).
235
236		print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,Cat,unknown,Min)) :-
237		translate_pp(PP,Cat,PPS),
238		format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n',
239		[PPS,RT,WT,Min,MaxWT,NrCalls]).
240		print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,Cat,MaxID,Min)) :-
241		translate_pp(PP,Cat,PPS),
242		format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime (max for ~w); #calls ~w)~n',
243		[PPS,RT,WT,Min,MaxWT,MaxID,NrCalls]).
244
245		tcltk_get_profile_info(Category,
246		list([list(['Operation/Action','Total Runtime (ms)','Total Walltime (ms)',
247		'# Calls','Max. Walltime (ms)','Max. Witness ID', 'Min. Walltime (ms)'])|L])) :-
248		findall(profile(RT,WT,Calls,MaxWT,AN,Category,MaxWitnessID,Min),
249		relevant_total_runtime(AN,Category,RT,WT,Calls,MaxWT,MaxWitnessID,Min),List),
250		sort(List,SL),
251		reverse(SL,RSL),
252		maplist(get_profile_list,RSL,L).
253
254		:- use_module(probsrc(tools_meta),[translate_term_into_atom/2]).
255		get_profile_list(profile(RT,WT,Calls,MaxWT,AN,Cat,MaxID,Min),list([PPS,RT,WT,Calls,MaxWT,MaxID,Min])) :-
256		translate_pp(AN,Cat,PPS).
257
258		% can be generated from command-line using -csv prob_constants_profile_info FILE
259		tcltk_get_constants_profile_info(
260		list([list(['Constant','Kind','@desc', 'Phase', 'Computation Runtime (ms)',
261		'Computation Walltime (ms)', 'Propagation Walltime (ms)',
262		'# Calls','Other Infos', 'Valued','Det.Value','Instantiates'])|L])) :-
263		findall(ProfileTerm, relevant_cst_profile_entry(ProfileTerm),List),
264		sort(List,SL),
265		reverse(SL,RSL),
266		maplist(get_cprofile_list,RSL,L).
267
268		:- use_module(bmachine, [constant_variable_marked_as_memo/1, constant_variable_marked_as_expand/1]).
269		:- use_module(b_interpreter_components,[get_det_solution_for_constant_value_kind/2]).
270		:- use_module(b_machine_hierarchy,[abstract_constant/2, concrete_constant/2]).
271		:- use_module(translate,[translate_bvalue_kind/2]).
272		:- use_module(state_space,[try_get_unique_constants_state/1]).
273		relevant_cst_profile_entry(cprofile(RT,WT,PropWT,Calls,PP,Kind,Ann,Phase,IDInfo,InstItself,ValInfo,InstList)) :-
274		(try_get_unique_constants_state(CstState) -> true ; CstState=[]),
275		(Category = constant_computation(Phase,IDInfo),
276		relevant_total_runtime(PP,Category,RT,WT,Calls,_MaxWT,_MaxWitnessID,_Min),
277		Phase \= propagate_value,
278		(abstract_constant(PP,_) -> Kind=abstract ; concrete_constant(PP,_) -> Kind=concrete ; Kind=unknown)
279		;
280		(constants_profiling_on -> Phase = no_equation_detected
281		; Phase = '-'), % constants profiling on needed to keep track of all equations (except arith. at the moment)
282		RT=0, WT=0, PropWT=0, Calls=0, IDInfo = [],
283		(abstract_constant(PP,_), Kind=abstract ; concrete_constant(PP,_), Kind=concrete),
284		\+ total_runtime(PP,constant_computation(_,_),_,_,_,_,_,_) % we have no profiling info at all for PP
285		),
286		(get_det_solution_for_constant_value_kind(PP,DetValInfo)
287		-> DetSolFound = true
288		; DetValInfo = '-', DetSolFound = false
289		),
290		( (DetSolFound=false ; DetValInfo='LARGE-VALUE'),
291		member(bind(PP,CstVal),CstState), translate_bvalue_kind(CstVal,ValInfo)
292		-> SolFound=true
293		; ValInfo=DetValInfo, SolFound=DetSolFound
294		),
295		% now check whether there are infos about propagation phase:
296		(total_runtime(PP,constant_computation(propagate_value,PropInfo),_,PropWT,_,_,_,_)
297		-> (member(instantiates(IList),PropInfo) ->
298		(select(PP,IList,InstList)
299		-> InstItself=yes
300		; (DetSolFound=true -> InstItself = 'delayed'
301		; SolFound=true -> InstItself = 'non-det' ; InstItself='NO'),
302		InstList=IList)
303		; % no instantiation list stored; performance monitoring not on
304		(SolFound=true -> InstItself='-' ; InstItself='NO'),
305		InstList = '-'
306		)
307		; PropWT = 0,
308		(DetSolFound=true -> InstItself='-' ; InstItself='NO'),
309		InstList='-'
310		),
311		(constant_variable_marked_as_expand(PP) -> Ann=expand
312		; constant_variable_marked_as_memo(PP) -> Ann=memo
313		; Ann = ''
314		).
315
316		get_cprofile_list(cprofile(RT,WT,PropWT,Calls,PP,Kind,Ann,Phase,IDInfo,InstItself,DetVal,IList),
317		list([PP,Kind,Ann,Phase,RT,WT,PropWT,Calls,IDInfo,InstItself,DetVal,IList])).
318
319
320		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3]).
321		% can be generated from command-line using -dot constants_profile_graph FILE
322		% TODO: improve rendering and then enable in meta_interface
323		tcltk_dot_constants_profile_info(File) :-
324		gen_dot_graph(File,constant_profile_predicate,constant_instantiates).
325
326		constant_profile_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none,
327		Category = constant_computation(Phase,_Infos),
328		total_runtime(NodeID,Category,_RT,WT,_Calls,_MaxWT,_MaxWitnessID,_Min),
329		(abstract_constant(NodeID,_) -> Kind=abstract ; Kind=concrete),
330		Phase \= propagate_value,
331		Shape = box,
332		(total_runtime(NodeID,constant_computation(propagate_value,_),_,WT2,_,_,_,_)
333		-> ajoin([NodeID,'\\n ',Kind,'\\n ',Phase,'\\n',WT, ' ms','\\n + ',WT2, ' ms'],NodeDesc)
334		; ajoin([NodeID,'\\n ',Kind,'\\n ',Phase,'\\n',WT, ' ms'],NodeDesc)
335		),
336		Style='rounded', Color=gray90.
337
338		constant_instantiates(NodeID,Label,SuccID,Color,Style) :-
339		Color=red4, Style=solid, Label = 'inst',
340		Category = constant_computation(Phase,Infos), Phase = propagate_value,
341		total_runtime(NodeID,Category,_RT,_WT,_Calls,_MaxWT,_MaxWitnessID,_Min),
342		member(instantiates(List),Infos),
343		member(SuccID,List), SuccID \= NodeID.
344
345
346		:- endif.