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