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 critical_cyclet::const_iterator e_it=it->begin();
30 for(; e_it!=it->end(); ++e_it)
35 set_of_cycles.erase(*it);
52 std::set<critical_cyclet> &set_of_cycles,
59 std::list<event_idt>* order=
nullptr;
85 for(std::list<event_idt>::const_iterator
119 while(!stack.empty())
125 <<
egraph[current_vertex].get_operation()
126 <<
egraph[current_vertex].variable <<
"@" 127 <<
egraph[current_vertex].thread <<
"~" 128 <<
egraph[current_vertex].local
136 if(current_vertex==vertex)
140 new_cycle.push_front(current_vertex);
142 if(current_vertex==source)
152 std::set<critical_cyclet> &set_of_cycles,
159 bool has_to_be_unsafe,
168 std::stack<event_idt> tmp;
200 <<
egraph[source].id<<
"#"<<source<<
" lw:"<<lwfence_met<<
" unsafe:" 203 bool get_com_only=
false;
204 bool unsafe_met_updated=unsafe_met;
205 bool same_var_pair_updated=same_var_pair;
207 bool not_thin_air=
true;
213 irep_idt avoid_at_the_end=var_to_avoid;
215 if(avoid_at_the_end!=
"" && avoid_at_the_end==this_vertex.
variable)
223 if(!this_vertex.
local)
229 bool has_to_be_unsafe_updated=
false;
258 if(!
egraph[preprevious].unsafe_pair(this_vertex, model) &&
260 egraph[preprevious].operation==
263 egraph[preprevious].operation==
266 egraph[preprevious].operation==
272 has_to_be_unsafe_updated=has_to_be_unsafe;
297 same_var_pair_updated=
true;
311 same_var_pair_updated=
false;
322 if(nb_writes+nb_reads==3)
356 if(unsafe_met_updated &&
359 has_to_be_unsafe_updated=
true;
369 for(wmm_grapht::edgest::const_iterator
375 && (unsafe_met_updated
382 for(critical_cyclet::const_iterator e_it=new_cycle.begin();
383 e_it!=new_cycle.end();
388 not_thin_air && new_cycle.
is_cycle() &&
393 set_of_cycles.insert(new_cycle);
396 set_of_cycles.insert(*reduced);
410 same_var_pair_updated,
412 has_to_be_unsafe_updated,
413 avoid_at_the_end, model);
420 for(wmm_grapht::edgest::const_iterator
428 (unsafe_met_updated ||
435 for(critical_cyclet::const_iterator e_it=new_cycle.begin();
436 e_it!=new_cycle.end();
441 not_thin_air && new_cycle.
is_cycle() &&
446 set_of_cycles.insert(new_cycle);
449 set_of_cycles.insert(*reduced);
507 if(not_thin_air && !get_com_only &&
508 (po_trans > 1 || po_trans==0) &&
522 std::stack<event_idt> tmp;
541 mark[tmp.top()]=
true;
553 avoid_at_the_end=this_vertex.
variable;
567 for(wmm_grapht::edgest::const_iterator w_it=
578 (po_trans==0?0:po_trans-1),
std::list< event_idt > po_order
const std::string & id2string(const irep_idt &d)
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
Tarjan 1972 adapted and modified for events.
std::string print_name(const critical_cyclet &redyced, memory_modelt model) const
std::stack< event_idt > marked_stack
void filter_thin_air(std::set< critical_cyclet > &set_of_cycles)
after the collection, eliminates the executions forbidden by an indirect thin-air ...
std::map< event_idt, bool > mark
bool is_not_thin_air() const
bool is_not_uniproc() const
void remove_com_edge(event_idt a, event_idt b)
std::map< irep_idt, unsigned char > writes_per_variable
void hide_internals(critical_cyclet &reduced) const
static mstreamt & eom(mstreamt &m)
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
const wmm_grapht::edgest & po_out(event_idt n) const
std::map< irep_idt, unsigned char > reads_per_variable
std::map< unsigned, unsigned char > events_per_thread
const wmm_grapht::edgest & com_out(event_idt n) const
bool are_po_ordered(event_idt a, event_idt b)
wmm_grapht::node_indext event_idt
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
std::list< event_idt > poUrfe_order
bool is_unsafe(memory_modelt model, bool fast=false)
checks whether there is at least one pair which is unsafe (takes fences and dependencies into account...
std::set< event_idt > thin_air_events
critical_cyclet extract_cycle(event_idt vertex, event_idt source, unsigned number_of_cycles)
extracts a (whole, unreduced) cycle from the stack.
virtual std::list< event_idt > * order_filtering(std::list< event_idt > *order)
std::map< unsigned, data_dpt > map_data_dp
bool has_user_defined_fence
std::stack< event_idt > point_stack
std::set< event_idt > skip_tracked
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
virtual bool filtering(event_idt u)