1 | % (c) 2014-2019 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, | |
12 | ||
13 | runtime_observe_available/0, | |
14 | observe_runtime/3 | |
15 | ]). | |
16 | ||
17 | % TO DO: optionally load more precise microsecond timer | |
18 | ||
19 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
20 | ||
21 | ||
22 | :- if(\+ environ(prob_observe_runtime, true)). | |
23 | runtime_observe_available :- fail. | |
24 | observe_runtime(_StartMs,_Msg,_Span). | |
25 | :- else. | |
26 | :- use_module(error_manager,[add_message/4]). | |
27 | runtime_observe_available. | |
28 | observe_limit(100). % TO DO: set limit by SICStus environment variable or preference | |
29 | observe_runtime(Start,Msg,Span) :- | |
30 | statistics(runtime,[End,_]), TotRuntime is End-Start, | |
31 | observe_limit(Limit), | |
32 | (TotRuntime>Limit -> add_message(delay,Msg,TotRuntime,Span) ; true). | |
33 | :- endif. | |
34 | ||
35 | :- if(\+ environ(prob_profile, true)). | |
36 | ||
37 | reset_runtime_profiler. | |
38 | :- meta_predicate profile_single_call(-,-,0). | |
39 | profile_single_call(_Label,_ID,C) :- call(C). | |
40 | :- meta_predicate profile_single_call(-,0). | |
41 | profile_single_call(_Label,C) :- call(C). | |
42 | register_profiler_runtime(_,_,_,_). | |
43 | profile_failure_driven_loop(_). | |
44 | profile_failure_driven_loop(_,_). | |
45 | print_runtime_profile :- | |
46 | print('No profiling information available'),nl, | |
47 | print('Recompile ProB with -Dprob_profile=true'),nl. | |
48 | tcltk_get_profile_info(list([I1,I2])) :- | |
49 | I1='No profiling information available', | |
50 | I2='Recompile ProB with -Dprob_profile=true'. | |
51 | runtime_profile_available :- fail. | |
52 | ||
53 | :- else. | |
54 | runtime_profile_available. | |
55 | ||
56 | :- volatile total_runtime/6. | |
57 | :- dynamic total_runtime/6. | |
58 | ||
59 | reset_runtime_profiler :- % print('RESET '),nl, print_runtime_profile, | |
60 | retractall(total_runtime(_,_,_,_,_,_)). | |
61 | ||
62 | :- use_module(eventhandling,[register_event_listener/3]). | |
63 | :- register_event_listener(clear_specification,reset_runtime_profiler, | |
64 | 'Reset runtime profiler.'). | |
65 | ||
66 | :- meta_predicate profile_single_call(-,-,0). | |
67 | profile_single_call(Label,ID,C) :- | |
68 | start_profile(Label,StartInfo), | |
69 | if(call(C),stop_profile(Label,ID,StartInfo),(stop_profile(Label,ID,StartInfo),fail)). | |
70 | ||
71 | :- meta_predicate profile_single_call(-,0). | |
72 | profile_single_call(Label,C) :- profile_single_call(Label,unknown,C). | |
73 | ||
74 | ||
75 | % register runtime for a failure driven loop: | |
76 | profile_failure_driven_loop(ActionName) :- profile_failure_driven_loop(ActionName,unknown). | |
77 | profile_failure_driven_loop(ActionName,StateID) :- | |
78 | start_profile(ActionName,Info), | |
79 | %format('Start Action ----> ~w (~w)~n',[ActionName,Info]), | |
80 | register_time(ActionName,StateID,Info). | |
81 | register_time(_,_,_). | |
82 | register_time(AN,StateID,Info) :- | |
83 | stop_profile(AN,StateID,Info), | |
84 | fail. | |
85 | ||
86 | start_profile(_Label,[RT1,WT1]) :- | |
87 | statistics(runtime,[RT1,_Delta]), | |
88 | statistics(walltime,[WT1,_]). | |
89 | stop_profile(Label,StateID,[RT1,WT1]) :- | |
90 | statistics(runtime,[RT2,_]), | |
91 | statistics(walltime,[WT2,_]), | |
92 | DRT is RT2-RT1, DWT is WT2-WT1, | |
93 | %format('Runtime for ~w : ~w ms (~w wall)~n',[AN,DRT,DWT]), | |
94 | register_profiler_runtime(Label,StateID,DRT,DWT). | |
95 | ||
96 | % register_profiler_runtime(Label,StateID,DeltaRunTime,DeltaWallTime) | |
97 | register_profiler_runtime(_,_,0,0) :- !. % comment out if you want to count all calls | |
98 | register_profiler_runtime(PP,ID,RTime,WTime) :- | |
99 | (var(PP) -> PP2='unknown' ; PP2 = PP), | |
100 | (retract(total_runtime(PP2,OldR,OldW,Calls,Max,MaxID)) | |
101 | -> true ; OldR=0,OldW=0,Max=0,MaxID=unknown,Calls=0), | |
102 | ((RTime<0 ; WTime <0) -> print(negative_runtime(PP,ID,RTime,WTime)),nl ; true), | |
103 | NewR is OldR+RTime, NewW is OldW+WTime, NewCalls is Calls+1, | |
104 | (WTime > Max -> NewMax = WTime, NewMaxID=ID ; NewMax = Max, NewMaxID=MaxID), | |
105 | assert(total_runtime(PP2,NewR,NewW,NewCalls,NewMax,NewMaxID)). | |
106 | ||
107 | ||
108 | :- use_module(library(lists)). | |
109 | print_runtime_profile :- | |
110 | format('-- ProB Runtime Profiler --~n',[]), | |
111 | findall(profile(RT,WT,Calls,MaxWT,PP,MaxID),total_runtime(PP,RT,WT,Calls,MaxWT,MaxID),List), | |
112 | sort(List,SL), | |
113 | reverse(SL,RSL), | |
114 | maplist(print_runtime_profile_info,RSL), | |
115 | findall(WT2,total_runtime(_PP1,_RT1,WT2,_Calls,_MaxWT1,_MaxID1),WList), | |
116 | sumlist(WList,TotalWT), | |
117 | findall(Calls2,total_runtime(_PP2,_RT2,WT2,Calls2,_MaxWT2,_MaxID2),WList2), | |
118 | sumlist(WList2,TotalCalls), | |
119 | format(' Total Walltime: ~w ms for #calls ~w~n',[TotalWT,TotalCalls]). | |
120 | ||
121 | print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,unknown)) :- | |
122 | format(' ~w : ~w ms (~w ms walltime & ~w ms max. walltime; #calls ~w)~n',[PP,RT,WT,MaxWT,NrCalls]). | |
123 | print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,MaxID)) :- | |
124 | format(' ~w : ~w ms (~w ms walltime & ~w ms max. walltime for ~w; #calls ~w)~n',[PP,RT,WT,MaxWT,MaxID,NrCalls]). | |
125 | ||
126 | tcltk_get_profile_info(list([list(['Operation Name','Total Runtime (ms)','Total Walltime (ms)','# Calls','Max. Walltime (ms)','Max. Witness ID'])|L])) :- | |
127 | findall(profile(RT,WT,Calls,MaxWT,AN,MaxWitnessID),total_runtime(AN,RT,WT,Calls,MaxWT,MaxWitnessID),List), | |
128 | sort(List,SL), | |
129 | reverse(SL,RSL), | |
130 | print(RSL),nl, | |
131 | maplist(get_profile_list,RSL,L). | |
132 | get_profile_list(profile(RT,WT,Calls,MaxWT,AN,MaxID),list([AN,RT,WT,Calls,MaxWT,MaxID])). | |
133 | ||
134 | ||
135 | :- endif. |