cprover
cycles_visitor.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: cycles visitor for computing edges involved for fencing
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #include "cycles_visitor.h"
13 
14 #include <list>
15 #include <map>
16 
17 #include "fence_inserter.h"
18 
19 class instrumentert;
20 
21 /* implemented: BTWN1, BTWN4 */
22 #define BTWN1
23 
24 /* po^+ /\ U{C_1, ..., C_n} \/ delays */
25 void cycles_visitort::po_edges(std::set<event_idt> &edges)
26 {
28 
29  event_grapht &egraph=instrumenter.egraph;
30 
31  for(std::set<event_grapht::critical_cyclet>::iterator
32  C_j=instrumenter.set_of_cycles.begin();
33  C_j!=instrumenter.set_of_cycles.end();
34  ++C_j)
35  {
36  /* filters */
37  if(fence_inserter.filter_cycles(C_j->id))
38  continue;
39 
40 #ifdef BTWN1
41  /* btwn1: variables are all the pos involved in cycles, plus the delays
42  for dp when analysing Power or ARM */
44  {
45  /* for Power/ARM, add also delays as variables for dp (other fences
46  are superfluous if the edge is not in pos; yet it's not harmful) */
47  for(std::set<edget>::iterator e_i=C_j->unsafe_pairs.begin();
48  e_i!=C_j->unsafe_pairs.end(); ++e_i)
49  {
50  if(e_i->is_po)
51  edges.insert(fence_inserter.add_edge(*e_i));
52  else
53  {
54  /* also add pos of non-delaying pos+ of cycles, as they could AC or
55  BC */
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();
59  ++next_it)
60  {
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);
66  }
67 
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();
71  ++next_it)
72  {
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);
78  }
79  }
80  }
81  }
82 
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;
86  ++next;
87  assert(next!=C_j->end());
88  for(; cur!=C_j->end() && next!=C_j->end(); ++cur, ++next)
89  {
90  if(egraph[*cur].is_fence() || egraph[*next].is_fence())
91  continue;
92 
93  const edget e_i(*cur, *next);
94 
95  if(e_i.is_po)
96  edges.insert(fence_inserter.add_edge(e_i));
97  else
98  {
99  /* adds basic pos from this pos^+ */
100  for(wmm_grapht::edgest::const_iterator
101  next_it=egraph.po_out(e_i.first).begin();
102  next_it!=egraph.po_out(e_i.first).end();
103  ++next_it)
104  {
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);
110  }
111  }
112  }
113  /* last case */
114  {
115  const edget e_i(*cur, C_j->front());
116 
117  if(!egraph[*cur].is_fence() && !egraph[C_j->front()].is_fence())
118  {
119  if(e_i.is_po)
120  edges.insert(fence_inserter.add_edge(e_i));
121  else
122  {
123  /* adds basic pos from this pos^+ */
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();
127  ++next_it)
128  {
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);
134  }
135  }
136  }
137  }
138 #elif defined BTWN4
139  /* add delays as var */
140  for(std::set<edget>::iterator e_i=C_j->unsafe_pairs.begin();
141  e_i!=C_j->unsafe_pairs.end(); ++e_i)
142  edges.insert(fence_inserter.add_edge(*e_i));
143 
144  /* maximum pos+ at the intersection of two cycles */
145  std::set<event_grapht::critical_cyclet>::iterator C_k=C_j;
146  ++C_k;
147  for(; C_k!=instrumenter.set_of_cycles.end(); ++C_k)
148  {
149  /* not necessary; might improve the construction time however */
150 #if 0
151  /* first, let us check if these cycles are entangled */
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)
155  {
156  for( ;
157  C_k_it!=C_k->end() &&
158  !egraph.are_po_ordered(*C_j_it, *C_k_it) &&
159  !egraph.are_po_ordered(*C_k_it, *C_j_it);
160  ++C_k_it)
161  {
162  }
163 
164  if(C_k_it!=C_k->end())
165  break;
166  }
167 
168  if(C_j_it==C_j->end())
169  continue;
170 #endif
171 
172  /* computes the largest pos+ in C_j */
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;
176 
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)
180  {
181  const unsigned current_thread=egraph[*C_j_it].thread;
182 
183  if(previous_thread==current_thread && C_j_it!=C_j->begin())
184  m_end[previous_thread]=C_j_it;
185  else
186  {
187  m_begin[current_thread]=C_j_it;
188  m_end[current_thread]=C_j_it;
189  m_threads.insert(current_thread);
190  }
191 
192  previous_thread=current_thread;
193  }
194 
195  /* computes the largest pos+ in C_k */
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;
199 
200  previous_thread=0;
201  for(event_grapht::critical_cyclet::const_iterator C_k_it=C_k->begin();
202  C_k_it!=C_k->end(); ++C_k_it)
203  {
204  const unsigned current_thread=egraph[*C_k_it].thread;
205 
206  if(previous_thread==current_thread && C_k_it!=C_k->begin())
207  k_end[previous_thread]=C_k_it;
208  else
209  {
210  k_begin[current_thread]=C_k_it;
211  k_end[current_thread]=C_k_it;
212  k_threads.insert(current_thread);
213  }
214 
215  previous_thread=current_thread;
216  }
217 
218  /* if there are some commun threads, take the intersection if relevant */
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())
222  {
223  const event_idt a=*m_begin[*it];
224  const event_idt b=*m_end[*it];
225  const event_idt c=*k_begin[*it];
226  const event_idt d=*k_end[*it];
227 
228  if(egraph.are_po_ordered(b, c))
229  continue;
230  else if(egraph.are_po_ordered(d, a))
231  continue;
232  else if(egraph.are_po_ordered(a, c) && egraph.are_po_ordered(b, d))
234  else if(egraph.are_po_ordered(a, c) && egraph.are_po_ordered(d, b))
236  else if(egraph.are_po_ordered(c, a) && egraph.are_po_ordered(b, d))
238  else if(egraph.are_po_ordered(c, a) && egraph.are_po_ordered(d, b))
240  }
241  }
242 #else
243  throw "no BTWN definition selected!";
244 #endif
245  }
246 }
247 
248 /* C_j /\ po^+ /\ poWR */
251  std::set<event_idt> &edges)
252 {
254 
255  for(std::set<edget>::iterator e_i=C_j.unsafe_pairs.begin();
256  e_i!=C_j.unsafe_pairs.end(); ++e_i)
257  {
258  if(e_i->is_po &&
259  (graph[e_i->first].operation==abstract_eventt::operationt::Write &&
260  graph[e_i->second].operation==abstract_eventt::operationt::Read))
261  {
262  if( edges.insert(fence_inserter.add_edge(*e_i)).second )
264  }
265  }
266 }
267 
268 /* C_j /\ po^+ /\ poWW */
271  std::set<event_idt> &edges)
272 {
274 
275  for(std::set<edget>::iterator e_i=C_j.unsafe_pairs.begin();
276  e_i!=C_j.unsafe_pairs.end(); ++e_i)
277  {
278  if(e_i->is_po &&
279  (graph[e_i->first].operation==abstract_eventt::operationt::Write &&
280  graph[e_i->second].operation==abstract_eventt::operationt::Write))
281  {
282  if( edges.insert(fence_inserter.add_edge(*e_i)).second )
284  }
285  }
286 }
287 
288 /* C_j /\ po^+ /\ poRW */
291  std::set<event_idt> &edges)
292 {
294 
295  for(std::set<edget>::iterator e_i=C_j.unsafe_pairs.begin();
296  e_i!=C_j.unsafe_pairs.end(); ++e_i)
297  {
298  if(e_i->is_po &&
299  (graph[e_i->first].operation==abstract_eventt::operationt::Read &&
300  graph[e_i->second].operation==abstract_eventt::operationt::Write))
301  {
302  if( edges.insert(fence_inserter.add_edge(*e_i)).second )
304  }
305  }
306 }
307 
308 /* C_j /\ po^+ /\ poRR */
311  std::set<event_idt> &edges)
312 {
314 
315  for(std::set<edget>::iterator e_i=C_j.unsafe_pairs.begin();
316  e_i!=C_j.unsafe_pairs.end(); ++e_i)
317  {
318  if(e_i->is_po &&
319  (graph[e_i->first].operation==abstract_eventt::operationt::Read &&
320  graph[e_i->second].operation==abstract_eventt::operationt::Read))
321  {
322  if( edges.insert(fence_inserter.add_edge(*e_i)).second )
324  }
325  }
326 }
327 
328 /* C_j /\ comWR */
331  std::set<event_idt> &edges)
332 {
334 
335  for(std::set<edget>::const_iterator it=C_j.unsafe_pairs.begin();
336  it!=C_j.unsafe_pairs.end();
337  ++it)
338  {
339  if(egraph[it->first].operation==abstract_eventt::operationt::Write
340  && egraph[it->second].operation==abstract_eventt::operationt::Read
341  && egraph[it->first].thread!=egraph[it->second].thread)
342  if( edges.insert(fence_inserter.add_invisible_edge(*it)).second )
344  }
345 
346 #if 0
347  event_grapht &egraph=instrumenter.egraph;
348 
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());
352  ++next_it;
353  for(; next_it!=C_j.end() && e_it!=C_j.end(); ++e_it, ++next_it)
354  {
355  const abstract_eventt &e1=egraph[*e_it];
356  const abstract_eventt &e2=egraph[*next_it];
357 
358  if(e1.operation==abstract_eventt::Write
359  && e2.operation==abstract_eventt::Read
360  && e1.thread!=e2.thread)
361  {
362  if( edges.insert(add_invisible_edge(edget(*e_it, *next_it))).second )
363  ++constraints_number;
364  }
365  }
366  /* last case */
367  assert(e_it!=C_j.end());
368  next_it=C_j.begin();
369 
370  const abstract_eventt &e1=egraph[*e_it];
371  const abstract_eventt &e2=egraph[*next_it];
372 
373  if(e1.operation==abstract_eventt::Write
374  && e2.operation==abstract_eventt::Read
375  && e1.thread!=e2.thread)
376  {
377  if( edges.insert(add_invisible_edge(edget(*e_it, *next_it))).second )
378  ++constraints_number;
379  }
380 #endif
381 }
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
operationt operation
Definition: wmm.h:23
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)
Definition: fence.cpp:18
const wmm_grapht::edgest & po_out(event_idt n) const
Definition: event_graph.h:400
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
Definition: event_graph.h:395
virtual bool filter_cycles(unsigned cycle_id) const
bool are_po_ordered(event_idt a, event_idt b)
Definition: event_graph.h:481
wmm_grapht::node_indext event_idt
Definition: event_graph.h:32
std::set< delayt > unsafe_pairs
Definition: event_graph.h:163
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)
Definition: wmm.h:19
ILP construction for all cycles and resolution.
void porw_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
instrumentert & instrumenter
event_grapht egraph
Definition: goto2graph.h:283
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
Definition: goto2graph.h:289
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