31 for(std::set<event_grapht::critical_cyclet>::iterator
47 for(std::set<edget>::iterator e_i=C_j->unsafe_pairs.begin();
48 e_i!=C_j->unsafe_pairs.end(); ++e_i)
56 for(wmm_grapht::edgest::const_iterator
57 next_it=egraph.
po_in(e_i->first).begin();
58 next_it!=egraph.
po_in(e_i->first).end();
61 std::list<event_idt> new_path;
62 new_path.push_back(e_i->first);
63 new_path.push_back(next_it->first);
65 next_it->first, new_path);
68 for(wmm_grapht::edgest::const_iterator
69 next_it=egraph.
po_out(e_i->second).begin();
70 next_it!=egraph.
po_out(e_i->second).end();
73 std::list<event_idt> new_path;
74 new_path.push_back(e_i->second);
75 new_path.push_back(next_it->first);
77 next_it->first, new_path);
83 event_grapht::critical_cyclet::const_iterator cur=C_j->begin();
84 assert(cur!=C_j->end());
85 event_grapht::critical_cyclet::const_iterator next=cur;
87 assert(next!=C_j->end());
88 for(; cur!=C_j->end() && next!=C_j->end(); ++cur, ++next)
90 if(egraph[*cur].
is_fence() || egraph[*next].is_fence())
93 const edget e_i(*cur, *next);
100 for(wmm_grapht::edgest::const_iterator
105 std::list<event_idt> new_path;
106 new_path.push_back(e_i.
first);
107 new_path.push_back(next_it->first);
109 next_it->first, e_i.
second, new_path);
115 const edget e_i(*cur, C_j->front());
117 if(!egraph[*cur].
is_fence() && !egraph[C_j->front()].is_fence())
124 for(wmm_grapht::edgest::const_iterator
125 next_it=egraph.
po_out(e_i.first).begin();
126 next_it!=egraph.
po_out(e_i.first).end();
129 std::list<event_idt> new_path;
130 new_path.push_back(e_i.first);
131 new_path.push_back(next_it->first);
133 next_it->first, e_i.second, new_path);
140 for(std::set<edget>::iterator e_i=C_j->unsafe_pairs.begin();
141 e_i!=C_j->unsafe_pairs.end(); ++e_i)
145 std::set<event_grapht::critical_cyclet>::iterator C_k=C_j;
152 event_grapht::critical_cyclet::const_iterator C_j_it=C_j->begin();
153 event_grapht::critical_cyclet::const_iterator C_k_it=C_k->begin();
154 for(; C_j_it!=C_j->end(); ++C_j_it)
157 C_k_it!=C_k->end() &&
164 if(C_k_it!=C_k->end())
168 if(C_j_it==C_j->end())
173 std::map<unsigned, event_grapht::critical_cyclet::const_iterator> m_begin;
174 std::map<unsigned, event_grapht::critical_cyclet::const_iterator> m_end;
175 std::set<event_idt> m_threads;
177 unsigned previous_thread=0;
178 for(event_grapht::critical_cyclet::const_iterator C_j_it=C_j->begin();
179 C_j_it!=C_j->end(); ++C_j_it)
181 const unsigned current_thread=egraph[*C_j_it].thread;
183 if(previous_thread==current_thread && C_j_it!=C_j->begin())
184 m_end[previous_thread]=C_j_it;
187 m_begin[current_thread]=C_j_it;
188 m_end[current_thread]=C_j_it;
189 m_threads.insert(current_thread);
192 previous_thread=current_thread;
196 std::map<unsigned, event_grapht::critical_cyclet::const_iterator> k_begin;
197 std::map<unsigned, event_grapht::critical_cyclet::const_iterator> k_end;
198 std::set<event_idt> k_threads;
201 for(event_grapht::critical_cyclet::const_iterator C_k_it=C_k->begin();
202 C_k_it!=C_k->end(); ++C_k_it)
204 const unsigned current_thread=egraph[*C_k_it].thread;
206 if(previous_thread==current_thread && C_k_it!=C_k->begin())
207 k_end[previous_thread]=C_k_it;
210 k_begin[current_thread]=C_k_it;
211 k_end[current_thread]=C_k_it;
212 k_threads.insert(current_thread);
215 previous_thread=current_thread;
219 for(std::set<event_idt>::const_iterator it=m_threads.begin();
220 it!=m_threads.end(); ++it)
221 if(k_threads.find(*it)!=k_threads.end())
243 throw "no BTWN definition selected!";
251 std::set<event_idt> &edges)
255 for(std::set<edget>::iterator e_i=C_j.
unsafe_pairs.begin();
271 std::set<event_idt> &edges)
275 for(std::set<edget>::iterator e_i=C_j.
unsafe_pairs.begin();
291 std::set<event_idt> &edges)
295 for(std::set<edget>::iterator e_i=C_j.
unsafe_pairs.begin();
311 std::set<event_idt> &edges)
315 for(std::set<edget>::iterator e_i=C_j.
unsafe_pairs.begin();
331 std::set<event_idt> &edges)
335 for(std::set<edget>::const_iterator it=C_j.
unsafe_pairs.begin();
341 && egraph[it->first].thread!=egraph[it->second].thread)
349 std::list<event_idt>::const_iterator e_it=C_j.begin();
350 std::list<event_idt>::const_iterator next_it=e_it;
351 assert(!C_j.empty());
353 for(; next_it!=C_j.end() && e_it!=C_j.end(); ++e_it, ++next_it)
362 if( edges.insert(add_invisible_edge(
edget(*e_it, *next_it))).second )
363 ++constraints_number;
367 assert(e_it!=C_j.end());
377 if( edges.insert(add_invisible_edge(
edget(*e_it, *next_it))).second )
378 ++constraints_number;
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
void poww_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
void powr_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
const wmm_grapht::edgest & po_out(event_idt n) const
unsigned add_invisible_edge(const edget &e)
void po_edges(std::set< event_idt > &edges)
const memory_modelt model
unsigned add_edge(const edget &e)
const wmm_grapht::edgest & po_in(event_idt n) const
virtual bool filter_cycles(unsigned cycle_id) const
bool are_po_ordered(event_idt a, event_idt b)
wmm_grapht::node_indext event_idt
std::set< delayt > unsafe_pairs
void const_graph_explore(event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path)
cycles visitor for computing edges involved for fencing
void porr_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
ILP construction for all cycles and resolution.
void porw_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
instrumentert & instrumenter
fence_insertert & fence_inserter
void const_graph_explore_BC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path)
std::set< event_grapht::critical_cyclet > set_of_cycles
void const_graph_explore_AC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path)
void com_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
std::size_t constraints_number
number of constraints
event_grapht::critical_cyclet::delayt edget