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);
52 std::set<critical_cyclet> &set_of_cycles,
56 for(std::size_t i=0; i<egraph.size(); i++)
59 std::list<event_idt>* order=
nullptr;
66 order=&egraph.po_order;
69 order=&egraph.poUrfe_order;
80 order=order_filtering(order);
85 for(std::list<event_idt>::const_iterator
91 egraph.message.debug() <<
"explore " << egraph[source].id <<
messaget::eom;
92 backtrack(set_of_cycles, source, source,
95 while(!marked_stack.empty())
104 if(egraph.filter_thin_air)
117 std::stack<event_idt>
stack(point_stack);
119 while(!
stack.empty())
124 egraph.message.debug() <<
"extract: " 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)
142 if(current_vertex==source)
152 std::set<critical_cyclet> &set_of_cycles,
159 bool has_to_be_unsafe,
164 egraph.message.debug() << std::string(80,
'-');
166 egraph.
message.
debug() <<
"marked size:" << marked_stack.size()
168 std::stack<event_idt> tmp;
169 while(!point_stack.empty())
172 tmp.push(point_stack.top());
178 point_stack.push(tmp.top());
181 while(!marked_stack.empty())
183 egraph.message.debug() << marked_stack.top() <<
" | ";
184 tmp.push(marked_stack.top());
190 marked_stack.push(tmp.top());
196 if(filtering(vertex))
199 egraph.message.debug() <<
"bcktck "<<egraph[vertex].id<<
"#"<<vertex<<
", " 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;
233 if(egraph.ignore_arrays ||
241 if(events_per_thread[this_vertex.
thread]==4)
244 events_per_thread[this_vertex.
thread]++;
252 if(has_to_be_unsafe && point_stack.size() >= 2)
254 const event_idt previous=point_stack.top();
256 const event_idt preprevious=point_stack.top();
257 point_stack.push(previous);
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;
280 if(!point_stack.empty() &&
281 egraph.are_po_ordered(point_stack.top(), vertex) &&
285 this_vertex.
variable==egraph[point_stack.top()].variable)
289 egraph[point_stack.top()].operation==
292 events_per_thread[this_vertex.
thread]--;
297 same_var_pair_updated=
true;
298 if(events_per_thread[this_vertex.
thread]>=3)
304 if(!point_stack.empty() &&
305 egraph.are_po_ordered(point_stack.top(), vertex) &&
309 this_vertex.
variable!=egraph[point_stack.top()].variable)
311 same_var_pair_updated=
false;
319 const unsigned char nb_writes=writes_per_variable[this_vertex.
variable];
320 const unsigned char nb_reads=reads_per_variable[this_vertex.
variable];
322 if(nb_writes+nb_reads==3)
324 events_per_thread[this_vertex.
thread]--;
331 events_per_thread[this_vertex.
thread]--;
335 writes_per_variable[this_vertex.
variable]++;
341 events_per_thread[this_vertex.
thread]--;
345 reads_per_variable[this_vertex.
variable]++;
349 if(!point_stack.empty())
355 egraph.map_data_dp[this_vertex.
thread].dp(prev_vertex, this_vertex));
356 if(unsafe_met_updated &&
358 egraph.are_po_ordered(point_stack.top(), vertex))
359 has_to_be_unsafe_updated=
true;
362 point_stack.push(vertex);
364 marked_stack.push(vertex);
369 for(wmm_grapht::edgest::const_iterator
370 w_it=egraph.po_out(vertex).begin();
371 w_it!=egraph.po_out(vertex).end(); w_it++)
374 if(w==source && point_stack.size()>=4
375 && (unsafe_met_updated
376 || this_vertex.
unsafe_pair(egraph[source], model)) )
383 e_it!=new_cycle.
end();
385 thin_air_events.insert(*e_it);
388 not_thin_air && new_cycle.
is_cycle() &&
391 egraph.message.debug() << new_cycle.
print_name(model,
false)
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
421 w_it=egraph.com_out(vertex).begin();
422 w_it!=egraph.com_out(vertex).end(); w_it++)
426 egraph.remove_com_edge(vertex, w);
427 else if(w==source && point_stack.size()>=4 &&
428 (unsafe_met_updated ||
436 e_it!=new_cycle.
end();
438 thin_air_events.insert(*e_it);
441 not_thin_air && new_cycle.
is_cycle() &&
444 egraph.message.debug() << new_cycle.
print_name(model,
false)
446 set_of_cycles.insert(new_cycle);
449 set_of_cycles.insert(*reduced);
473 while(!marked_stack.empty() && marked_stack.top()!=vertex)
480 if(!marked_stack.empty())
485 assert(!point_stack.empty());
494 writes_per_variable[this_vertex.
variable]--;
496 reads_per_variable[this_vertex.
variable]--;
498 events_per_thread[this_vertex.
thread]--;
506 if(skip_tracked.find(vertex)==skip_tracked.end())
507 if(not_thin_air && !get_com_only &&
508 (po_trans > 1 || po_trans==0) &&
509 !point_stack.empty() &&
510 egraph.are_po_ordered(point_stack.top(), vertex) &&
513 egraph[point_stack.top()].operation==
517 egraph[point_stack.top()].operation==
520 skip_tracked.insert(vertex);
522 std::stack<event_idt> tmp;
524 while(!marked_stack.empty() && marked_stack.top()!=vertex)
526 tmp.push(marked_stack.top());
527 mark[marked_stack.top()]=
false;
531 if(!marked_stack.empty())
533 assert(marked_stack.top()==vertex);
540 marked_stack.push(tmp.top());
541 mark[tmp.top()]=
true;
545 marked_stack.push(vertex);
548 if(!egraph[point_stack.top()].unsafe_pair(this_vertex, model))
551 if(egraph.ignore_arrays ||
553 avoid_at_the_end=this_vertex.
variable;
560 egraph[point_stack.top()].operation==
564 egraph[point_stack.top()].operation==
567 for(wmm_grapht::edgest::const_iterator w_it=
568 egraph.po_out(vertex).begin();
569 w_it!=egraph.po_out(vertex).end(); w_it++)
578 (po_trans==0?0:po_trans-1),
588 while(!marked_stack.empty() && marked_stack.top()!=vertex)
595 if(!marked_stack.empty())
600 skip_tracked.erase(vertex);
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
void filter_thin_air(std::set< critical_cyclet > &set_of_cycles)
after the collection, eliminates the executions forbidden by an indirect thin-air ...
bool is_not_thin_air() const
bool is_not_uniproc() const
void hide_internals(critical_cyclet &reduced) const
static mstreamt & eom(mstreamt &m)
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
data_typet::const_iterator const_iterator
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
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.
bool has_user_defined_fence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)