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.