1 | % (c) 2016-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(b_operation_cache, [ %project_in_state/6, | |
6 | %operation_computed/4, | |
7 | compute_operation_on_expanded_store_cache/6, | |
8 | check_invariant_violated_cache/2, | |
9 | print_op_cache_profile/0, | |
10 | get_op_cache_stats/1, | |
11 | reset_b_operation_cache_with_statistics/0, | |
12 | tcltk_op_cache_stats/1 | |
13 | ]). | |
14 | ||
15 | ||
16 | :- use_module(probsrc(module_information)). | |
17 | :- module_info(group,animator). | |
18 | :- module_info(description,'This module caches B operation results on projected states. Used when preference try_operation_reuse different from false'). | |
19 | ||
20 | % TO DO: | |
21 | % provide predecessor ID and operation to know which values are unchanged? -> reuse hash; know which ops are definitely disabled? (cf pge) | |
22 | % Note: operation caching works better with COMPRESSION TRUE, as this way the values are pre-hashed. A simpler hash function is then used. | |
23 | % Note: if we change the MAX_OPERATIONS preference, this will have no effect on already cached operations | |
24 | % TODO: we could invalidate operation cache upon such a change; storing the value for each node is probably overkill | |
25 | ||
26 | :- use_module(probsrc(self_check)). | |
27 | :- use_module(extension('counter/counter')). % op_cache_id,... counter | |
28 | :- use_module(probsrc(succeed_max),[succeed_max_call_id/3, reset_max_reached/1, max_reached/1, assert_max_reached/1]). | |
29 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
30 | :- use_module(probsrc(error_manager)). | |
31 | :- use_module(probsrc(debug),[debug_println/2]). | |
32 | :- use_module(probsrc(performance_messages),[perfmessage/2]). | |
33 | :- use_module(library(ordsets), [ord_subtract/3]). | |
34 | :- use_module(probsrc(tools),[retract_with_statistics/2]). | |
35 | ||
36 | b_operation_cache_startup :- % call once at startup to ensure all counters exist | |
37 | counter_init, | |
38 | new_counter(op_cache_id), | |
39 | new_counter(inv_cache_nr), | |
40 | new_counter(op_cached_failures), | |
41 | new_counter(op_cached_successes), | |
42 | new_counter(inv_cached_successes), | |
43 | new_counter(op_cached_timeouts). | |
44 | ||
45 | ||
46 | :- register_event_listener(startup_prob,b_operation_cache_startup, | |
47 | 'Initialise Statespace Counters.'). | |
48 | :- register_event_listener(reset_specification,reset_b_operation_cache, | |
49 | 'Reset Operation Cache.'). | |
50 | :- register_event_listener(clear_specification,reset_b_operation_cache, % necessary? as reset occurs before? | |
51 | 'Reset Operation Cache.'). | |
52 | :- register_event_listener(change_of_animation_mode,reset_b_operation_cache, | |
53 | 'Reset Operation Cache.'). | |
54 | % TO DO: also reset if maxNrOfEnablingsPerOperation changed ? | |
55 | ||
56 | ||
57 | :- dynamic operation_read_projection_cache/5, operation_read_constants/2, operation_guard_read_info/3. | |
58 | reset_b_operation_cache :- | |
59 | retractall(operation_read_projection_cache(_,_,_,_,_)), | |
60 | retractall(operation_read_constants(_,_)), | |
61 | retractall(operation_guard_read_info(_,_,_)), | |
62 | retractall(operation_computed(_,_,_,_,_)), | |
63 | retractall(operation_cached_results(_,_,_,_)), | |
64 | retractall(operation_cached_max_reached(_,_)), | |
65 | retractall(operation_cached_time_out(_,_)), | |
66 | retractall(op_guard_fails(_,_,_)), | |
67 | reset_counter(op_cache_id), | |
68 | reset_counter(inv_cache_nr), | |
69 | reset_counter(op_cached_failures), | |
70 | reset_counter(op_cached_successes), | |
71 | reset_counter(inv_cached_successes). | |
72 | ||
73 | ||
74 | reset_b_operation_cache_with_statistics :- | |
75 | retract_with_statistics(b_operation_cache, | |
76 | [operation_read_projection_cache(_,_,_,_,_), | |
77 | operation_read_constants(_,_),operation_guard_read_info(_,_,_), | |
78 | operation_computed(_,_,_,_,_), operation_cached_results(_,_,_,_), | |
79 | operation_cached_max_reached(_,_), | |
80 | operation_cached_time_out(_,_), | |
81 | op_guard_fails(_,_,_) | |
82 | ] | |
83 | ), | |
84 | reset_b_operation_cache. | |
85 | ||
86 | ||
87 | % ------------------------------------------------- | |
88 | ||
89 | ||
90 | % project the in-state for an operation onto the relevant variables | |
91 | project_in_state(VarsInState,OpName,ProjectedInState) :- | |
92 | get_opname_key(OpName,OpNameKey), | |
93 | project_in_state_for_opname_key(VarsInState,OpNameKey,ProjectedInState). | |
94 | ||
95 | :- use_module(probsrc(bmachine),[b_is_constant/1]). | |
96 | :- use_module(library(lists),[exclude/3, include/3]). | |
97 | project_in_state_for_opname_key(InState,OpNameKey,ProjectedInState) :- | |
98 | get_operation_read_projection_infos(OpNameKey,_,InState,ProjVars,_,_), | |
99 | (re_project_state(ProjVars,InState,Res) -> ProjectedInState=Res | |
100 | ; add_internal_error('Re-Projection failed: ',re_project_state(ProjVars,InState,_)), | |
101 | ProjectedInState = InState). | |
102 | ||
103 | :- use_module(probsrc(specfile),[csp_with_bz_mode/0]). | |
104 | :- use_module(probsrc(b_read_write_info),[b_get_operation_read_guard_vars/4]). | |
105 | :- use_module(probsrc(bmachine),[b_definition_prefixed/5]). | |
106 | ||
107 | ||
108 | % get infos about cached operations (and compute the first time info requested for an operation) | |
109 | get_operation_read_projection_infos(OpNameKey,OpName,_,ProjVars,IsReadingCsts,AdditionalOutVars) :- | |
110 | operation_read_projection_cache(OpNameKey,OpName,ProjVars,IsReadingCsts,AdditionalOutVars),!, | |
111 | ProjVars \= no_caching. | |
112 | get_operation_read_projection_infos(OpNameKey,OpName,_,_,_,_) :- atom(OpName), | |
113 | b_definition_prefixed(_, 'OPERATION_REUSE_OFF_', OpName, _DefName,_), | |
114 | !, | |
115 | format('Ignoring operation ~w for reuse~n',[OpName]), | |
116 | assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])), | |
117 | fail. | |
118 | get_operation_read_projection_infos(OpNameKey,OpName,InState,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars) :- | |
119 | api_get_operation_read_write_info(OpName,ReadVariables,ReadConstants,WrittenVariables), | |
120 | (ReadConstants=[] -> IsReadingCsts=false ; IsReadingCsts=true), | |
121 | debug_println(19,operation_reads_vars_consts(OpName,ReadVariables,ReadConstants)), | |
122 | (project_state_onto_vars(InState,ReadVariables,ProjVarsInOrder,_RelevantState,0,NrDeleted) | |
123 | -> % TO DO: if we have constants in the state which are deterministic anyway, then they should not count | |
124 | % TO DO: statically pre-compute which operations are worthwhile for this treatment | |
125 | ((NrDeleted>0 % we project away at least one variable and thus hope to cache operation results | |
126 | ; csp_with_bz_mode) % in CSP||B mode, the same operation may be called with different CSP controllers | |
127 | -> ord_subtract(WrittenVariables,ReadVariables,AdditionalOutVars), % vars written but not read | |
128 | assertz(operation_read_projection_cache(OpNameKey,OpName,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars)), | |
129 | assertz(operation_read_constants(OpNameKey,ReadConstants)), | |
130 | % ,print(proj(OpName,ProjVarsInOrder,AdditionalOutVars)),nl, | |
131 | (get_preference(try_operation_reuse,full), | |
132 | b_get_operation_read_guard_vars(OpName,true,ReadVarsInGuard,precise), | |
133 | exclude(member_ord(ReadVarsInGuard),ProjVarsInOrder,IrrelevantVars), | |
134 | % TO DO: analyse if projection really useful | |
135 | IrrelevantVars \= [] | |
136 | -> include(member_ord(ReadVarsInGuard),ProjVarsInOrder,ReadVarsInGuard), | |
137 | debug_println(19,guard_reads_subset_of_vars(OpName,OpNameKey,ReadVarsInGuard,IrrelevantVars)), | |
138 | assertz(operation_guard_read_info(OpNameKey,ReadVarsInGuard,IrrelevantVars)) | |
139 | ; true) | |
140 | ; assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])), | |
141 | perfmessage('Not caching operation for reuse: ',OpName), | |
142 | fail | |
143 | ) | |
144 | ; add_internal_error('Projection failed for: ', project_state_onto_vars(InState,ReadVariables,_,_,0,_)), | |
145 | assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])), | |
146 | fail | |
147 | ). | |
148 | %TODO: also compute precise guard b_get_operation_read_guard_vars(Operation,JustVariables,VarsResult,VarsPrecise) if possible and if read vars in guard << ReadVariables also store this | |
149 | % if operation call fails -> store only precise guard | |
150 | ||
151 | % ------------------------------- | |
152 | ||
153 | % API to abstract operations so that we can use caching also for invariants, maybe later assertions, ... | |
154 | ||
155 | % get atomic key to store operation info | |
156 | get_opname_key(Name,Res) :- var(Name),!, | |
157 | add_internal_error('Variable opname: ',get_opname_key(Name,Res)), Res=Name. | |
158 | get_opname_key(check_invariant_violated(Nr),Key) :- !, Key=Nr. | |
159 | get_opname_key(Name,Name). | |
160 | ||
161 | api_get_operation_read_write_info(OpName,ReadVariables,ReadConstants,WrittenVariables) :- | |
162 | api_get_op_rw_aux(OpName,ReadIds,WrittenVariables), | |
163 | exclude(b_is_constant,ReadIds,ReadVariables), | |
164 | include(b_is_constant,ReadIds,ReadConstants). | |
165 | :- use_module(probsrc(bmachine),[b_nth1_invariant/3,b_get_operation_normalized_read_write_info/3]). | |
166 | api_get_op_rw_aux(check_invariant_violated(Nr),UsedIds,Written) :- !, Written=[], | |
167 | b_nth1_invariant(Nr,_,UsedIds). | |
168 | api_get_op_rw_aux(OpName,ReadVariables,WrittenVariables) :- | |
169 | b_get_operation_normalized_read_write_info(OpName,ReadVariables,WrittenVariables). | |
170 | ||
171 | ||
172 | :- use_module(probsrc(b_interpreter),[b_execute_top_level_operation_update/5]). | |
173 | ||
174 | % we use a trick using a mutable to detect when a time_out or exception has been thrown | |
175 | % during caching; we could have used assert/retract or bb_put/bb_get instead | |
176 | ||
177 | api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall) :- | |
178 | create_mutable(still_computing,Done), | |
179 | call_cleanup( | |
180 | com_op_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,Done), | |
181 | (get_mutable(still_computing,Done) | |
182 | -> format('Timeout, exception or virtual timeout occured during caching for ~w (cache id ~w)~n',[OpName,NewID]), | |
183 | inc_counter(op_cached_timeouts), | |
184 | register_op_cache_time_out(NewID,OpName) | |
185 | ; true | |
186 | )), | |
187 | get_mutable(DVal,Done), DVal \= finished. % fail if we are Done; | |
188 | ||
189 | % we could do this: but we don't know if an exception, timeout or virtual time_out occurred | |
190 | register_op_cache_time_out(ID,OpName) :- | |
191 | inc_counter(op_cached_timeouts), | |
192 | assertz(operation_cached_time_out(ID,OpName)). | |
193 | % as an alternative this removes the cached results: | |
194 | %invalidate_operation_cache(ID,OpName) :- | |
195 | % retractall(operation_cached_results(ID,_Operation,_,_)), | |
196 | % retractall(operation_computed(_,OpName,_,_,ID)). % can be expensive | |
197 | ||
198 | ||
199 | ||
200 | com_op_update_max(_,check_invariant_violated(Nr),Operation,ProjState,NewState,PathInfo,_,Done) :- !, | |
201 | NewState =[], PathInfo=invariant, Operation=Nr, % values not used anyway for invariants | |
202 | %print(check_invariant(Nr)),nl, bmachine:b_nth1_invariant(Nr,Inv,_UsedIds), translate:print_bexpr(Inv),nl, | |
203 | (b_interpreter:check_nth1_invariant(Nr,ProjState ) | |
204 | -> update_mutable(finished,Done) % will lead to failure above; we store only violations | |
205 | ; % invariant violation found | |
206 | update_mutable(last_sol_found,Done) | |
207 | ). | |
208 | com_op_update_max(_,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,_) :- | |
209 | % for CSP||B: clear out any parameters; otherwise we also need to hash the parameters | |
210 | reset_max_reached(OpName), | |
211 | succeed_max_call_id(OpName, | |
212 | b_execute_top_level_operation_update(OpName,Operation,ProjInOutState,NewState,PathInfo), | |
213 | MaxForCall). | |
214 | % TO DO: normalise_store out state values, to avoid re-normalising when storing updates | |
215 | com_op_update_max(NewID,OpName,_,_,_,_,_,Done) :- | |
216 | (NewID \= uncached, | |
217 | max_reached(OpName) | |
218 | -> assertz(operation_cached_max_reached(NewID,OpName)) % store that we reached max. nr of transitions for this node | |
219 | ; true %format('No Timeout or virtual timeout occurred during caching for ~w leading to ~w~n',[OpName,NewID]) | |
220 | ), | |
221 | update_mutable(finished,Done). | |
222 | ||
223 | ||
224 | ||
225 | % entry point to cache invariant checking | |
226 | check_invariant_violated_cache(Nr,State) :- | |
227 | %get_store_and_info(State,FullStore,Infos), | |
228 | compute_operation_on_expanded_store_cache(check_invariant_violated(Nr),_,State,_,_,-1). | |
229 | ||
230 | :- use_module(probsrc(specfile),[expand_const_and_vars_to_full_store/2]). | |
231 | %get_store_and_info(expanded_const_and_vars(_ConstID,_Vars,E,Info),FullStore,Info) :- !, FullStore=E. | |
232 | %get_store_and_info(expanded_vars(E,Info),FullStore,Info) :- !, FullStore=E. | |
233 | %get_store_and_info(Store,FullStore,[]) :- expand_const_and_vars_to_full_store(Store,FullStore). | |
234 | ||
235 | % ------------------------------- | |
236 | ||
237 | ||
238 | % check if caching is worthwhile for this operation | |
239 | %worthwhile_to_cache(OpName) :- | |
240 | % get_read_write_info(OpName,ReadVariables,WrittenVariables), | |
241 | % length(ReadVariables,NrRV), | |
242 | % bmachine:b_machine_statistics(variables,NrVars), | |
243 | % bmachine:b_machine_statistics(constants,NrConstants), | |
244 | % Perc is (NrRV*100) // (NrVars+NrConstants), | |
245 | % length(WrittenVariables,NrWV), | |
246 | % format('Analyzing ~w, ~w %, read: ~w, written: ~w, tot vars: ~w, tot cst: ~w~n (read: ~w)~n',[OpName,Perc,NrRV,NrWV,NrVars,NrConstants,ReadVariables]), | |
247 | % Perc < 95. % maybe provide as preference | |
248 | ||
249 | :- use_module(library(ordsets),[ord_member/2]). | |
250 | %is_read(ReadVariables,bind(Var,_)) :- ord_member(Var,ReadVariables). | |
251 | member_ord(List,X) :- ord_member(X,List). % for maplist, exclude,... | |
252 | ||
253 | % ------------------------------- | |
254 | ||
255 | % a variation of split_list which also returns a list of predicate results | |
256 | % with re_project_state(L,ProjVarsInOrder,A) : we can split another list using the same pattern | |
257 | ||
258 | :- assert_must_succeed((b_operation_cache:project_state_onto_vars([bind(x,1),bind(y,2),bind(b,3)],[b,y], | |
259 | ProjVars,ProjState,0,NrDel), | |
260 | ProjVars == [y,b], ProjState == [bind(y,2),bind(b,3)], NrDel==1)). | |
261 | ||
262 | project_state_onto_vars([],_,[],[],Acc,Acc). | |
263 | project_state_onto_vars([Elem|Rest],ReadVariables,ProjVars,ProjState,NrDelAcc,NrDel) :- | |
264 | Elem = bind(Var,_), | |
265 | (ord_member(Var,ReadVariables) % TO DO: we could improve performance by sorting Elements | |
266 | -> ProjVars=[Var|PT], ProjState=[Elem|AR], ND1=NrDelAcc | |
267 | ; ProjVars=PT, ProjState=AR, ND1 is NrDelAcc+1), | |
268 | project_state_onto_vars(Rest,ReadVariables,PT,AR,ND1,NrDel). | |
269 | ||
270 | ||
271 | % ------------------------------- | |
272 | ||
273 | :- assert_must_succeed((b_operation_cache:re_project_state([y,b],[bind(x,1),bind(y,2),bind(b,3)],Res), | |
274 | Res == [bind(y,2),bind(b,3)])). | |
275 | ||
276 | % project state(VarsInOrder,State,ProjectedState) | |
277 | % faster than project_state_onto_vars | |
278 | re_project_state([],_,[]). | |
279 | re_project_state([VarToProject|PT],[Elem|Rest],A) :- | |
280 | arg(1,Elem,Var), %Elem = bind(Var,_), | |
281 | (VarToProject==Var | |
282 | -> A=[Elem|AR],re_project_state(PT,Rest,AR) | |
283 | ; re_project_state2(VarToProject,PT,Rest,A)). | |
284 | ||
285 | re_project_state2(VarToProject,PT,[Elem|Rest],A) :- | |
286 | arg(1,Elem,Var), %Elem = bind(Var,_), | |
287 | (VarToProject==Var | |
288 | -> A=[Elem|AR],re_project_state(PT,Rest,AR) | |
289 | ; re_project_state2(VarToProject,PT,Rest,A)). | |
290 | ||
291 | % ----------------------------- | |
292 | ||
293 | % Two utilities to optionally generate lemma facts for fast projection | |
294 | % Does not seem to be worth it | |
295 | ||
296 | % abstract away values, can be used to generate pre-compiled facts | |
297 | %abstract_state([],[]). | |
298 | %abstract_state([bind(Var,_)|T],[bind(Var,_)|AT]) :- abstract_state(T,AT). | |
299 | ||
300 | % abstract away unused bindings, can be used to generate pre-compiled facts | |
301 | %clear_unused_bindings([],_,_) :- !. | |
302 | %clear_unused_bindings([VarToProject|PT],[bind(Var,V)|T],[bind(Var,V)|RT]) :- | |
303 | % % we could clear out Variable name Var; but this creates a danger of successfully matching an erroneous state | |
304 | % VarToProject==Var,!, | |
305 | % clear_unused_bindings(PT,T,RT). | |
306 | %clear_unused_bindings(Vars,[_|T],[_|RT]) :- % leave slot in result as fresh var | |
307 | % clear_unused_bindings(Vars,T,RT). | |
308 | ||
309 | % ------------------------------- | |
310 | ||
311 | :- use_module(probsrc(hashing)). | |
312 | :- use_module(probsrc(state_packing)). | |
313 | ||
314 | :- dynamic operation_computed/5, operation_cached_results/4, | |
315 | operation_cached_max_reached/2, operation_cached_time_out/2, | |
316 | op_guard_fails/3. | |
317 | ||
318 | % return Hash and check if operation computed | |
319 | % TO DO: do not hash constants if single value exists ? | |
320 | check_if_operation_was_computed(OpName,ConstID,State,Skel,Infos,PackedValList,IsReadingCsts, | |
321 | HashConstID,Hash,Res) :- | |
322 | (Infos = [packed_state/PS|_] | |
323 | -> get_packed_vars(PS,OpName,PackedState), | |
324 | remove_bind_skeleton(PackedState,Skel,PackedValList) | |
325 | % packing already performed in prepare_state_for_specfile_trans | |
326 | ; write(no_packed_state_info(OpName,ConstID)),nl, % shouldn't happen hopefully | |
327 | project_in_state(State,OpName,ProjectedInState), % State contains just variables | |
328 | pack_bind_list(ProjectedInState,Skel,PackedValList) | |
329 | ), | |
330 | (IsReadingCsts = false -> HashConstID=root ; HashConstID=ConstID), | |
331 | op_hash(OpName,HashConstID,PackedValList,Hash), | |
332 | (operation_computed(Hash,OpName,HashConstID,PackedValList,ID) | |
333 | -> Res = ID | |
334 | ; % operation_guard_read_info(OpKey,GuardVars,_), re_project_state(GuardVars,Skel,PackedValList,GuardPackedVals) | |
335 | % op_hash(OpName,HashConstID,GuardPackedVals,GuardHash), op_guard_fails(GuardHash,OpName,GuardPackedVals,ID) -> true | |
336 | Res= false). | |
337 | ||
338 | % project a state or packed value list onto the variables relevant for the guard (if it is a subset) | |
339 | project_onto_guard(OpName,OpKey,HashConstID,Skel,PackedValList,GuardPackedVals,GuardHash) :- | |
340 | operation_guard_read_info(OpKey,_,IgnoredVars), | |
341 | remove_ignored_vars(IgnoredVars,Skel,PackedValList,GuardPackedVals), | |
342 | op_hash(OpName,HashConstID,GuardPackedVals,GuardHash). | |
343 | ||
344 | ||
345 | % remove_ignored_vars(VarsToIgnore,SkeletonList,ValueList,Result) | |
346 | remove_ignored_vars([],_,PackedVals,Res) :- Res=PackedVals. | |
347 | remove_ignored_vars([ID|T],[ID|ST],[_|PackedVals],GuardPackedVals) :- !, | |
348 | remove_ignored_vars(T,ST,PackedVals,GuardPackedVals). | |
349 | remove_ignored_vars(Ignored,[_|ST],[PV|PackedVals],[PV|GuardPackedVals]) :- | |
350 | remove_ignored_vars(Ignored,ST,PackedVals,GuardPackedVals). | |
351 | ||
352 | get_packed_vars(const_and_vars(_,Vars),OpName,PackedVars) :- !, project_in_state(Vars,OpName,PackedVars). | |
353 | get_packed_vars(PS,OpName,PackedVars) :- !, project_in_state(PS,OpName,PackedVars). | |
354 | :- use_module(library(terms),[term_hash/3]). | |
355 | :- use_module(probsrc(hashing),[my_term_hash/2]). | |
356 | ||
357 | op_hash(OpName,HashConstID,PackedValList,Hash) :- get_preference(use_state_packing,false),!, | |
358 | my_term_hash((OpName,HashConstID,PackedValList),Hash). % will user super_hash | |
359 | op_hash(OpName,HashConstID,PackedValList,Hash) :- | |
360 | % we use state packing and thus replace AVL sets by identifiers, ...: a simpler hash suffices, but we get collisions for Train1_Lukas_POR (which do not seem to matter); we get an improvement for ifm18/Ref5_Switch_mch.eventb | |
361 | term_hash((OpName,HashConstID,PackedValList), | |
362 | [range(smallint),algorithm(sdbm),depth(infinite),if_var(ignore)], % djb2 | |
363 | Hash). | |
364 | ||
365 | ||
366 | % remove bind/2 wrappers and variable name for faster hashing | |
367 | remove_bind_skeleton([],[],R) :- !, R=[]. | |
368 | remove_bind_skeleton([bind(Var,Val)|T],[Var|VT],[Val|RT]) :- !, | |
369 | remove_bind_skeleton(T,VT,RT). | |
370 | remove_bind_skeleton(L,V,R) :- add_internal_error('Illegal store: ',remove_bind_skeleton(L,V,R)), R=L. | |
371 | ||
372 | % we could also peel a few infos not useful for hashing: | |
373 | %peel_val('$stored_avl_packed'(Nr),Nr). | |
374 | %peel_val('$avl_bv'(Nr,_),Nr). % correct because if we use a bit_vector we will never also use stored_avl_packed for the same type | |
375 | ||
376 | ||
377 | get_new_operation_computed_id(OpName,ConstID,PackedValList,Hash,ID) :- | |
378 | inc_counter(op_cache_id,ID), | |
379 | (OpName=check_invariant_violated(_) -> inc_counter(inv_cache_nr,_) ; true), | |
380 | assertz(operation_computed(Hash,OpName,ConstID,PackedValList,ID)). | |
381 | % To reduce memory consumption we could use the following clause: | |
382 | % can be useful if there are many operations with a large number of projected variables | |
383 | % but does lead to noticable slowdown when looking up operations | |
384 | %get_new_operation_computed_id(OpName,ConstID,_PackedValList,Hash,[_,state_id/ReferenceStateID],ID) :- !, | |
385 | % inc_counter(op_cache_id,ID), | |
386 | % assertz(operation_computed(Hash,OpName,ConstID,ReferenceStateID,ID)). % storing reference ID preserves memory | |
387 | % when looking up operation_was_computed we would need to do something like: | |
388 | % state_space:packed_visited_expression(StoredState,PS), | |
389 | % get_packed_b_state_with_uncompressed_lists(PS,PUS), | |
390 | % get_state_infos(PUS,ConstID,PackedList,_,_), | |
391 | % project_in_state(PackedList,OpName,ProjectedStoredState), | |
392 | % remove_bind_skeleton(ProjectedStoredState,Skel,ProjectedValList), | |
393 | % ProjectedValList = PackedValList | |
394 | ||
395 | ||
396 | :- use_module(probsrc(runtime_profiler),[profile_failure_driven_loop/1]). | |
397 | % this is used when get_preference(try_operation_reuse,true/full) | |
398 | % it is only called for operations, not for setup_constants or initalise_machine | |
399 | ||
400 | % treat expanded_const_and_vars(ConstID,Vars,FullStore,Infos) | |
401 | ||
402 | get_state_infos(expanded_const_and_vars(ID,Vars,FullStore,I),ConstID,Vars,FullStore,Infos) :- !,ConstID=ID,Infos=I. | |
403 | get_state_infos(expanded_vars(V,I),ConstID,Vars,FullStore,Infos) :- !, ConstID=root,Vars=V,FullStore=V,Infos=I. | |
404 | get_state_infos(const_and_vars(ConstID,Vars),ConstID,Vars,FullStore,Infos) :- !, | |
405 | add_warning(get_state_infos,'State not prepared for caching: ',const_and_vars(ConstID,Vars)), | |
406 | Infos=[], | |
407 | expand_const_and_vars_to_full_store(const_and_vars(ConstID,Vars),FullStore). | |
408 | get_state_infos(csp_and_b(_,State),ConstID,Vars,FullStore,Infos) :- !, | |
409 | get_state_infos(State,ConstID,Vars,FullStore,Infos). | |
410 | get_state_infos(Vars,unknown,Vars,Vars,[]). | |
411 | ||
412 | % InState is either already an expanded list or expanded_const_and_vars, expanded_vars | |
413 | compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :- | |
414 | get_state_infos(InState,ConstID,Vars,FullStore,Infos), % extract infos from the store | |
415 | % TO DO: check if state_id in Infos and if OpName in equivalence class with same proj. vars | |
416 | get_opname_key(OpName,OpNameKey), | |
417 | get_operation_read_projection_infos(OpNameKey,OpName,Vars,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars), | |
418 | !, | |
419 | % tools_printing:print_term_summary(proj(OpName,ConstID,ProjInState,FullStore)),nl, | |
420 | check_if_operation_was_computed(OpName,ConstID,Vars,ProjVarsInOrder,Infos,PackedValList,IsReadingCsts, | |
421 | HashConstID,Hash,ID), | |
422 | (ID \= false | |
423 | -> % we can reuse the stored operation effect | |
424 | %print('+'), | |
425 | %hit_profiler:add_hit(operation_reused,OpName), | |
426 | (inv_op_name(OpName) -> inc_counter(inv_cached_successes) | |
427 | ; inc_counter(op_cached_successes)), | |
428 | (operation_cached_results(ID,Operation,PackedNewState,PathInfo), | |
429 | unpack_values(PackedNewState,NewState) | |
430 | ; | |
431 | operation_cached_max_reached(ID,OpName), % we did not compute all operations | |
432 | assert_max_reached(OpName), | |
433 | fail | |
434 | ; operation_cached_time_out(ID,OpName), | |
435 | format('Rethrowing cached time_out for ~w and cache id ~w~n',[OpName,ID]), | |
436 | throw(time_out) | |
437 | ) | |
438 | ; % we have not computed solutions for this operation for this projected state | |
439 | (project_onto_guard(OpName,OpNameKey,HashConstID,ProjVarsInOrder,PackedValList,GuardPackedVals,GuardHash) | |
440 | -> true | |
441 | ; GuardPackedVals = none), | |
442 | (nonvar(GuardHash), | |
443 | op_guard_fails(GuardHash,OpName,GuardPackedVals) | |
444 | -> % we did already compute this operation for this projected state and it failed | |
445 | inc_counter(op_cached_failures), | |
446 | fail % the guard is guaranteed to fail | |
447 | ; % we have not yet computed this operation; compute it and store solutions as we go | |
448 | get_new_operation_computed_id(OpName,HashConstID,PackedValList,Hash,NewID), | |
449 | %print('-'), | |
450 | %hit_profiler:add_hit(operation_cache_computation,OpName), | |
451 | (IsReadingCsts=false | |
452 | -> % TO DO: check if this projection is worthwhile | |
453 | project_in_state_for_opname_key(Vars,OpNameKey,ProjInState), | |
454 | % Note: if no packed_state this projection was already performed in check_if_operation_was_computed | |
455 | add_new_vars(AdditionalOutVars,ProjInState,ProjInOutState) | |
456 | ; ProjInOutState = FullStore % use full store with constants | |
457 | ), | |
458 | profile_failure_driven_loop(OpName), | |
459 | if(api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall), | |
460 | (% Normalise here or in update_max | |
461 | pack_values(NewState,PackedNewState), | |
462 | (PathInfo=invariant -> StoredPathInfo=Hash | |
463 | ; filter_transition_path_info(PathInfo,StoredPathInfo)), | |
464 | assertz(operation_cached_results(NewID,Operation,PackedNewState,StoredPathInfo)) | |
465 | ), | |
466 | (nonvar(GuardHash), | |
467 | %print(op_guard_fails(GuardHash,OpName,GuardPackedVals)),nl, | |
468 | assertz(op_guard_fails(GuardHash,OpName,GuardPackedVals)), | |
469 | fail | |
470 | ) | |
471 | ) | |
472 | ) | |
473 | % TO DO: if we have no successors for ID and if the operation reads less IDs in the guard | |
474 | % we can replace remaining identifier values by a variable | |
475 | ). | |
476 | compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :- | |
477 | %hit_profiler:add_hit(operation_not_cached,OpName), | |
478 | % operation is not cached | |
479 | get_state_infos(InState,_,_,FullStore,_), | |
480 | api_compute_operation_update_max(uncached,OpName,Operation,FullStore,NewState,PathInfo,MaxForCall). | |
481 | ||
482 | % add written vars which are not read virtually to state to avoid error messages in store_intermediate_updates: | |
483 | add_new_vars([],S,S). | |
484 | add_new_vars([WrittenVar|T],State,[bind(WrittenVar,term(undefined))|ST]) :- | |
485 | add_new_vars(T,State,ST). | |
486 | ||
487 | :- use_module(probsrc(state_space),[keep_transition_info/1]). | |
488 | filter_transition_path_info([],R) :- !, R=[]. | |
489 | filter_transition_path_info([H|T],Res) :- !, | |
490 | (keep_transition_info(H) -> Res = [H|RT] | |
491 | ; Res=RT), % by default we filter out possibly large path infos (in particular for Event-B) | |
492 | filter_transition_path_info(T,RT). | |
493 | filter_transition_path_info(H,Res) :- | |
494 | (keep_transition_info(H) -> Res = H ; Res=[]). | |
495 | ||
496 | ||
497 | invariant_op_key(OpKey,InvNr) :- operation_read_projection_cache(OpKey,check_invariant_violated(InvNr),_,_,_). | |
498 | ||
499 | :- use_module(probsrc(bmachine),[b_nth1_invariant/3]). | |
500 | print_violated_invariants :- | |
501 | operation_cached_results(ID,Nr,[],Hash),number(Nr), | |
502 | b_nth1_invariant(Nr,Invariant,_UsedIds), | |
503 | format('Invariant ~w violated (op-cache-id ~w)~n ',[Nr,ID]), | |
504 | translate:print_bexpr(Invariant),nl, | |
505 | % now try and recover state where it was violated: | |
506 | operation_computed(Hash,OpName,ConstID,PackedValList,ID), | |
507 | operation_read_projection_cache(_,OpName,Skel,_,_), | |
508 | unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,StateDesc), | |
509 | format(' in state (ConstID ~w) ~w~n',[ConstID,StateDesc]), | |
510 | fail. | |
511 | print_violated_invariants. | |
512 | ||
513 | % small utility code to analyze hash collisions: | |
514 | % b_operation_cache:ahc. | |
515 | :- public ahc/0. | |
516 | ahc :- operation_computed(Hash,OpName,ConstID,State,ID), | |
517 | operation_computed(Hash,OpName2,ConstID2,State2,ID2), | |
518 | (ConstID @> ConstID2 -> true ; ConstID=ConstID2, ID2 > ID), | |
519 | format('Hash collision: ~w~n ~w:~w:~w:~w~n ~w:~w:~w:~w~n~n', | |
520 | [Hash,OpName,ConstID,State,ID,OpName2,ConstID2,State2,ID2]), | |
521 | fail. | |
522 | ahc. | |
523 | ||
524 | :- use_module(probsrc(translate),[translate_bstate_limited/2, translate_event_with_limit/3]). | |
525 | :- use_module(probsrc(debug),[debug_mode/1]). | |
526 | :- use_module(probsrc(preferences),[get_preference/2]). | |
527 | :- use_module(probsrc(specfile),[get_operation_name/2]). | |
528 | get_op_name(Nr,check_invariant_violated(Nr)) :- number(Nr),!. | |
529 | get_op_name(Op,OpName) :- get_operation_name(Op,OpName). | |
530 | get_nr_next_state_calls(OpName,Nr) :- findall(1,operation_computed(_Hash,OpName,_,_,_ID),Ls), length(Ls,Nr). | |
531 | get_nr_cache_results(OpName,RNr) :- | |
532 | findall(1,(operation_cached_results(_ID,Op,_,_),get_op_name(Op,OpName)),Rs), length(Rs,RNr). | |
533 | :- use_module(probsrc(bmachine),[b_get_machine_variables/1]). | |
534 | % b_operation_cache:print_op_cache_profile | |
535 | ||
536 | check_if_op_cache_useful :- | |
537 | b_get_machine_variables(Var),length(Var,VLen), | |
538 | api_get_operation_read_write_info(OpName,ReadVariables,_ReadConstants,_WrittenVariables), | |
539 | length(ReadVariables,ReadLen), | |
540 | ReadLen < VLen, | |
541 | (inv_op_name(OpName) -> get_preference(use_po,false) ; true), | |
542 | format('Operation reuse potentially useful: ~w reads ~w/~w variables~n',[OpName,ReadLen,VLen]), | |
543 | fail. | |
544 | check_if_op_cache_useful. | |
545 | ||
546 | inv_op_name(check_invariant_violated(_)). | |
547 | ||
548 | print_op_cache_profile :- \+ operation_computed(_,_,_,_,_),!, % print nothing | |
549 | (get_preference(try_operation_reuse,false) -> format('OPERATION_REUSE preference not set to TRUE~n',[]) ; true), | |
550 | format('No operation cached~n',[]), | |
551 | check_if_op_cache_useful. | |
552 | print_op_cache_profile :- | |
553 | b_get_machine_variables(Var),length(Var,VLen), | |
554 | operation_read_projection_cache(OpKey,OpName,ProjVars,_,WV), (ProjVars = [] ; ProjVars = [_|_]), | |
555 | length(ProjVars,Len), | |
556 | operation_read_constants(OpKey,ReadConstants), | |
557 | (operation_guard_read_info(OpKey,_,IrrelevantVars) | |
558 | -> format('Operation ~w cached onto ~w/~w variables: ~w (not relevant for guard: ~w, only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,IrrelevantVars,WV,ReadConstants]) | |
559 | ; format('Operation ~w cached onto ~w/~w variables: ~w (only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,WV,ReadConstants]) | |
560 | ),fail. | |
561 | print_op_cache_profile :- findall(OpName,operation_read_projection_cache(_,OpName,no_caching,_,_),Ls), | |
562 | format('Operations not cached: ~w~n',[Ls]),fail. | |
563 | print_op_cache_profile :- operation_read_projection_cache(OpKey,OpName,ProjVars,_,_), ProjVars = [_|_], | |
564 | get_nr_next_state_calls(OpName,Nr), | |
565 | get_nr_cache_results(OpName,RNr), | |
566 | (inv_op_name(OpName) -> Results='violations' ; Results = 'results'), | |
567 | format('Next-state-calls for ~w: ~w (~w ~w)~n',[OpName,Nr,RNr,Results]), | |
568 | operation_guard_read_info(OpKey,RelVars,_), | |
569 | findall(1,op_guard_fails(_,OpName,_),Fails), length(Fails,NrFails), | |
570 | format(' projected-failures (on ~w): ~w~n',[RelVars,NrFails]), | |
571 | fail. | |
572 | print_op_cache_profile :- | |
573 | get_total_number_of_next_state_calls(Nr,InvNr), | |
574 | format('Total Number of Next-state-calls for Operations: ~w~n',[Nr]), | |
575 | get_counter(op_cached_failures,FailCalls), | |
576 | format(' - Reused guard failures: ~w~n',[FailCalls]), | |
577 | get_counter(op_cached_successes,SuccCalls), | |
578 | format(' - Reused successful operation call results: ~w~n',[SuccCalls]), | |
579 | format('Total Number of Invariant-check-calls: ~w~n',[InvNr]), | |
580 | get_counter(inv_cached_successes,SuccInvCalls), | |
581 | format(' - Reused invariant check results: ~w~n',[SuccInvCalls]), | |
582 | fail. | |
583 | print_op_cache_profile :- debug_mode(on), nl, | |
584 | operation_read_projection_cache(_,OpName,Skel,_,_), | |
585 | format('~n** Local Operation Cache Info for ~w ** (projected on ~w):~n',[OpName,Skel]), | |
586 | operation_computed(_Hash,OpName,ConstID,PackedValList,ID), | |
587 | (operation_cached_max_reached(ID,OpName) -> MaxR='(max reached, not all transitions computed)' | |
588 | ; MaxR=''), | |
589 | format('~nNode ID = ~w, Operation = ~w ~w~n',[ID,OpName,MaxR]), | |
590 | unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,NodeDesc), | |
591 | format(' projected state : (ConstID ~w) ~w~n',[ConstID,NodeDesc]), | |
592 | operation_cached_results(ID,Operation,PackedNewState,_PathInfo), | |
593 | translate_event_with_limit(Operation,100,OpStr), | |
594 | unpack_values(PackedNewState,NewState), translate:translate_bstate_limited(NewState,UpdateStr), | |
595 | format(' ~w -upd-> ~w~n',[OpStr,UpdateStr]), | |
596 | fail. | |
597 | print_op_cache_profile :- print_violated_invariants,fail. | |
598 | print_op_cache_profile :- ahc,print('----------'),nl. | |
599 | ||
600 | get_total_number_of_next_state_calls(OpNr,InvNr) :- | |
601 | get_counter(op_cache_id,TotNr), | |
602 | get_counter(inv_cache_nr,InvNr), | |
603 | OpNr is TotNr-InvNr. | |
604 | %findall(0,b_operation_cache:operation_computed(_Hash,_Op,_,_,_ID),Ls), length(Ls,Nr). | |
605 | ||
606 | get_op_cache_stats([next_state_calls-NrN, % actual calls to the B interpreter to compute next state | |
607 | operations_cached-NrC, % number of operations whose calls are cached | |
608 | invariants_cached-NrI, % number of invariants whose evaluation is cached | |
609 | next_state_guard_failures-NrFails, % number of next-state_call failures stored (disabled operation) | |
610 | reused_next_state_calls-SuccCalls, | |
611 | reused_next_state_failures-FailCalls, | |
612 | inv_check_calls-InvNr, % actual calls to check individual invariants in a state | |
613 | reused_inv_check_calls-SuccInvCalls | |
614 | ]) :- | |
615 | findall(OpKey,(operation_read_projection_cache(OpKey,OpName,_,_,_),atomic(OpName)),OK1), | |
616 | length(OK1,NrC), | |
617 | findall(OpKey,invariant_op_key(OpKey,_),OK2), | |
618 | length(OK2,NrI), | |
619 | findall(OpKey,(op_guard_fails(OpKey,_,_)),OK3), | |
620 | length(OK3,NrFails), | |
621 | get_total_number_of_next_state_calls(NrN,InvNr), | |
622 | get_counter(op_cached_failures,FailCalls), | |
623 | get_counter(op_cached_successes,SuccCalls), | |
624 | get_counter(inv_cached_successes,SuccInvCalls). | |
625 | ||
626 | % ---------------------- | |
627 | ||
628 | :- use_module(probsrc(tools_strings),[ajoin/2]). | |
629 | tcltk_op_cache_stats(list([list(['Operation','#Next-State', '#Results', | |
630 | '# Proj.Vars','Proj.Vars', 'ReadCsts', 'OnlyWritten'])|SEntries])) :- | |
631 | %b_get_machine_variables(Var),length(Var,VLen), | |
632 | findall(list([OP,NrCalls,RNr,NrProjVars,ProjVars,ReadConstants,AdditionalOutVars]), | |
633 | (operation_read_projection_cache(OpKey,OpName,ProjVars,_,AdditionalOutVars), | |
634 | (OpName = check_invariant_violated(Nr) -> ajoin(['Invariant',Nr],OP) ; OP=OpName), | |
635 | length(ProjVars,NrProjVars), | |
636 | operation_read_constants(OpKey,ReadConstants), | |
637 | get_nr_next_state_calls(OpName,NrCalls), | |
638 | get_nr_cache_results(OpName,RNr) | |
639 | ), Entries), sort(Entries,SEntries). | |
640 | ||
641 | % ---------------------- | |
642 | % DOT RENDERING (not yet finished) | |
643 | ||
644 | %op_cache_node(ID,OpName,NodeDesc,Shape,Style,Color) :- Shape=box, Style=solid, Color=blue, | |
645 | % operation_computed(_Hash,OpName,_,PackedState,ID), | |
646 | % unpack_values(PackedState,State), translate_bstate_limited(State,NodeDesc). | |
647 | %:- use_module(probsrc(dotsrc(dot_graph_generator)),[gen_dot_graph/3]). | |
648 | % Predicates for creating a dependency graph | |
649 | %tcltk_operation_cache_graph(File) :- gen_dot_graph(File,op_cache_node,cbc_dependence_trans_predicate). | |
650 |