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