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