21 std::set<critical_cyclet> &set_of_cycles)
23 for(std::set<critical_cyclet>::const_iterator it=set_of_cycles.begin();
24 it!=set_of_cycles.end(); )
26 std::set<critical_cyclet>::const_iterator next=it;
28 auto e_it=it->begin();
30 for(; e_it!=it->end(); ++e_it)
35 set_of_cycles.erase(*it);
160 std::set<critical_cyclet> &set_of_cycles,
167 bool has_to_be_unsafe,
172 egraph.message.debug() << std::string(80,
'-');
176 std::stack<event_idt> tmp;
207 egraph.message.debug() <<
"bcktck "<<
egraph[vertex].id<<
"#"<<vertex<<
", "
208 <<
egraph[source].id<<
"#"<<source<<
" lw:"<<lwfence_met<<
" unsafe:"
211 bool get_com_only=
false;
212 bool unsafe_met_updated=unsafe_met;
213 bool same_var_pair_updated=same_var_pair;
215 bool not_thin_air=
true;
221 irep_idt avoid_at_the_end=var_to_avoid;
223 if(!avoid_at_the_end.
empty() && avoid_at_the_end == this_vertex.
variable)
231 if(!this_vertex.
local)
237 bool has_to_be_unsafe_updated=
false;
241 if(
egraph.ignore_arrays ||
266 if(!
egraph[preprevious].unsafe_pair(this_vertex, model) &&
268 egraph[preprevious].operation==
271 egraph[preprevious].operation==
274 egraph[preprevious].operation==
280 has_to_be_unsafe_updated=has_to_be_unsafe;
305 same_var_pair_updated=
true;
319 same_var_pair_updated=
false;
330 if(nb_writes+nb_reads==3)
363 egraph.map_data_dp[this_vertex.
thread].dp(prev_vertex, this_vertex));
364 if(unsafe_met_updated &&
367 has_to_be_unsafe_updated=
true;
377 for(wmm_grapht::edgest::const_iterator
378 w_it=
egraph.po_out(vertex).begin();
379 w_it!=
egraph.po_out(vertex).end(); w_it++)
383 && (unsafe_met_updated
391 e_it!=new_cycle.
end();
396 not_thin_air && new_cycle.
is_cycle() &&
401 set_of_cycles.insert(new_cycle);
404 set_of_cycles.insert(*reduced);
418 same_var_pair_updated,
420 has_to_be_unsafe_updated,
421 avoid_at_the_end, model);
428 std::set<event_idt> edges_to_remove;
430 for(wmm_grapht::edgest::const_iterator
431 w_it=
egraph.com_out(vertex).begin();
432 w_it!=
egraph.com_out(vertex).end(); w_it++)
436 edges_to_remove.insert(w);
438 (unsafe_met_updated ||
446 e_it!=new_cycle.
end();
451 not_thin_air && new_cycle.
is_cycle() &&
456 set_of_cycles.insert(new_cycle);
459 set_of_cycles.insert(*reduced);
480 egraph.remove_com_edge(vertex, e);
519 if(not_thin_air && !get_com_only &&
520 (po_trans > 1 || po_trans==0) &&
534 std::stack<event_idt> tmp;
553 mark[tmp.top()]=
true;
563 if(
egraph.ignore_arrays ||
565 avoid_at_the_end=this_vertex.
variable;
579 for(wmm_grapht::edgest::const_iterator w_it=
580 egraph.po_out(vertex).begin();
581 w_it!=
egraph.po_out(vertex).end(); w_it++)
590 (po_trans==0?0:po_trans-1),
bool backtrack(std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwsync_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model)
see event_grapht::collect_cycles
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...