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)
151 std::set<critical_cyclet> &set_of_cycles,
158 bool has_to_be_unsafe,
163 egraph.message.debug() << std::string(80,
'-');
165 egraph.message.debug() <<
"marked size:" << marked_stack.size()
167 std::stack<event_idt> tmp;
168 while(!point_stack.empty())
170 egraph.message.debug() << point_stack.top() <<
" | ";
171 tmp.push(point_stack.top());
177 point_stack.push(tmp.top());
180 while(!marked_stack.empty())
182 egraph.message.debug() << marked_stack.top() <<
" | ";
183 tmp.push(marked_stack.top());
189 marked_stack.push(tmp.top());
195 if(filtering(vertex))
198 egraph.message.debug() <<
"bcktck "<<egraph[vertex].id<<
"#"<<vertex<<
", "
199 <<egraph[source].id<<
"#"<<source<<
" lw:"<<lwfence_met<<
" unsafe:"
202 bool get_com_only=
false;
203 bool unsafe_met_updated=unsafe_met;
204 bool same_var_pair_updated=same_var_pair;
206 bool not_thin_air=
true;
212 irep_idt avoid_at_the_end=var_to_avoid;
214 if(avoid_at_the_end!=
"" && avoid_at_the_end==this_vertex.
variable)
222 if(!this_vertex.
local)
228 bool has_to_be_unsafe_updated=
false;
232 if(egraph.ignore_arrays ||
240 if(events_per_thread[this_vertex.
thread]==4)
243 events_per_thread[this_vertex.
thread]++;
251 if(has_to_be_unsafe && point_stack.size() >= 2)
253 const event_idt previous=point_stack.top();
255 const event_idt preprevious=point_stack.top();
256 point_stack.push(previous);
257 if(!egraph[preprevious].unsafe_pair(this_vertex, model) &&
259 egraph[preprevious].operation==
262 egraph[preprevious].operation==
265 egraph[preprevious].operation==
271 has_to_be_unsafe_updated=has_to_be_unsafe;
279 if(!point_stack.empty() &&
280 egraph.are_po_ordered(point_stack.top(), vertex) &&
284 this_vertex.
variable==egraph[point_stack.top()].variable)
288 egraph[point_stack.top()].operation==
291 events_per_thread[this_vertex.
thread]--;
296 same_var_pair_updated=
true;
297 if(events_per_thread[this_vertex.
thread]>=3)
303 if(!point_stack.empty() &&
304 egraph.are_po_ordered(point_stack.top(), vertex) &&
308 this_vertex.
variable!=egraph[point_stack.top()].variable)
310 same_var_pair_updated=
false;
318 const unsigned char nb_writes=writes_per_variable[this_vertex.
variable];
319 const unsigned char nb_reads=reads_per_variable[this_vertex.
variable];
321 if(nb_writes+nb_reads==3)
323 events_per_thread[this_vertex.
thread]--;
330 events_per_thread[this_vertex.
thread]--;
334 writes_per_variable[this_vertex.
variable]++;
340 events_per_thread[this_vertex.
thread]--;
344 reads_per_variable[this_vertex.
variable]++;
348 if(!point_stack.empty())
354 egraph.map_data_dp[this_vertex.
thread].dp(prev_vertex, this_vertex));
355 if(unsafe_met_updated &&
357 egraph.are_po_ordered(point_stack.top(), vertex))
358 has_to_be_unsafe_updated=
true;
361 point_stack.push(vertex);
363 marked_stack.push(vertex);
368 for(wmm_grapht::edgest::const_iterator
369 w_it=egraph.po_out(vertex).begin();
370 w_it!=egraph.po_out(vertex).end(); w_it++)
373 if(w==source && point_stack.size()>=4
374 && (unsafe_met_updated
375 || this_vertex.
unsafe_pair(egraph[source], model)) )
382 e_it!=new_cycle.
end();
384 thin_air_events.insert(*e_it);
387 not_thin_air && new_cycle.
is_cycle() &&
390 egraph.message.debug() << new_cycle.
print_name(model,
false)
392 set_of_cycles.insert(new_cycle);
395 set_of_cycles.insert(*reduced);
409 same_var_pair_updated,
411 has_to_be_unsafe_updated,
412 avoid_at_the_end, model);
419 for(wmm_grapht::edgest::const_iterator
420 w_it=egraph.com_out(vertex).begin();
421 w_it!=egraph.com_out(vertex).end(); w_it++)
425 egraph.remove_com_edge(vertex, w);
426 else if(w==source && point_stack.size()>=4 &&
427 (unsafe_met_updated ||
435 e_it!=new_cycle.
end();
437 thin_air_events.insert(*e_it);
440 not_thin_air && new_cycle.
is_cycle() &&
443 egraph.message.debug() << new_cycle.
print_name(model,
false)
445 set_of_cycles.insert(new_cycle);
448 set_of_cycles.insert(*reduced);
472 while(!marked_stack.empty() && marked_stack.top()!=vertex)
479 if(!marked_stack.empty())
484 assert(!point_stack.empty());
493 writes_per_variable[this_vertex.
variable]--;
495 reads_per_variable[this_vertex.
variable]--;
497 events_per_thread[this_vertex.
thread]--;
505 if(skip_tracked.find(vertex)==skip_tracked.end())
506 if(not_thin_air && !get_com_only &&
507 (po_trans > 1 || po_trans==0) &&
508 !point_stack.empty() &&
509 egraph.are_po_ordered(point_stack.top(), vertex) &&
512 egraph[point_stack.top()].operation==
516 egraph[point_stack.top()].operation==
519 skip_tracked.insert(vertex);
521 std::stack<event_idt> tmp;
523 while(!marked_stack.empty() && marked_stack.top()!=vertex)
525 tmp.push(marked_stack.top());
526 mark[marked_stack.top()]=
false;
530 if(!marked_stack.empty())
532 assert(marked_stack.top()==vertex);
539 marked_stack.push(tmp.top());
540 mark[tmp.top()]=
true;
544 marked_stack.push(vertex);
547 if(!egraph[point_stack.top()].unsafe_pair(this_vertex, model))
550 if(egraph.ignore_arrays ||
552 avoid_at_the_end=this_vertex.
variable;
559 egraph[point_stack.top()].operation==
563 egraph[point_stack.top()].operation==
566 for(wmm_grapht::edgest::const_iterator w_it=
567 egraph.po_out(vertex).begin();
568 w_it!=egraph.po_out(vertex).end(); w_it++)
577 (po_trans==0?0:po_trans-1),
587 while(!marked_stack.empty() && marked_stack.top()!=vertex)
594 if(!marked_stack.empty())
599 skip_tracked.erase(vertex);