cprover
event_graph.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: graph of abstract events
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H
16 
17 #include <list>
18 #include <set>
19 #include <map>
20 #include <iosfwd>
21 
22 #include <util/graph.h>
23 #include <util/invariant.h>
24 
25 #include "abstract_event.h"
26 #include "data_dp.h"
27 #include "wmm.h"
28 
29 class messaget;
30 class namespacet;
31 
34 
36 {
37 public:
38  /* critical cycle */
39  class critical_cyclet final
40  {
41  typedef std::list<event_idt> data_typet;
43 
45 
46  bool is_not_uniproc() const;
47  bool is_not_weak_uniproc() const;
48 
49  std::string print_detail(const critical_cyclet &reduced,
50  std::map<std::string, std::string> &map_id2var,
51  std::map<std::string, std::string> &map_var2id) const;
52  std::string print_name(const critical_cyclet &redyced,
53  memory_modelt model) const;
54 
55  bool check_AC(
56  data_typet::const_iterator s_it,
57  const abstract_eventt &first,
58  const abstract_eventt &second) const;
59  bool check_BC(
60  data_typet::const_iterator it,
61  const abstract_eventt &first,
62  const abstract_eventt &second) const;
63 
64  public:
65  unsigned id;
67 
68  // NOLINTNEXTLINE(readability/identifiers)
69  typedef data_typet::iterator iterator;
70  // NOLINTNEXTLINE(readability/identifiers)
71  typedef data_typet::const_iterator const_iterator;
72  // NOLINTNEXTLINE(readability/identifiers)
73  typedef data_typet::value_type value_type;
74 
75  iterator begin() { return data.begin(); }
76  const_iterator begin() const { return data.begin(); }
77  const_iterator cbegin() const { return data.cbegin(); }
78 
79  iterator end() { return data.end(); }
80  const_iterator end() const { return data.end(); }
81  const_iterator cend() const { return data.cend(); }
82 
83  template <typename T>
84  void push_front(T &&t) { data.push_front(std::forward<T>(t)); }
85 
86  template <typename T>
87  void push_back(T &&t) { data.push_back(std::forward<T>(t)); }
88 
89  value_type &front() { return data.front(); }
90  const value_type &front() const { return data.front(); }
91 
92  value_type &back() { return data.back(); }
93  const value_type &back() const { return data.back(); }
94 
95  size_t size() const { return data.size(); }
96 
97  critical_cyclet(event_grapht &_egraph, unsigned _id)
98  :egraph(_egraph), id(_id), has_user_defined_fence(false)
99  {
100  }
101 
102  void operator()(const critical_cyclet &cyc)
103  {
104  data.clear();
105  for(auto it=cyc.data.cbegin();
106  it!=cyc.data.cend();
107  ++it)
108  data.push_back(*it);
110  }
111 
112  bool is_cycle()
113  {
114  /* size check */
115  if(data.size()<4)
116  return false;
117 
118  /* po order check */
119  auto it=data.cbegin();
120  auto n_it=it;
121  ++n_it;
122  for(; it!=data.cend() && n_it!=data.cend(); ++it, ++n_it)
123  {
124  if(egraph[*it].thread==egraph[*n_it].thread
125  && !egraph.are_po_ordered(*it, *n_it))
126  return false;
127  }
128 
129  return true;
130  }
131 
132  /* removes internal events (e.g. podWW Rfi gives podWR)
133  from.hide_internals(&target) */
134  void hide_internals(critical_cyclet &reduced) const;
135 
138  bool is_unsafe(memory_modelt model, bool fast=false);
139 
140  /* do not update the unsafe pairs set */
142  {
143  return is_unsafe(model, true);
144  }
145 
147  {
148  is_unsafe(model);
149  }
150 
151  bool is_unsafe_asm(memory_modelt model, bool fast=false);
152 
153  bool is_not_uniproc(memory_modelt model) const
154  {
155  if(model==RMO)
156  return is_not_weak_uniproc();
157  else
158  return is_not_uniproc();
159  }
160 
161  bool is_not_thin_air() const;
162 
163  /* pair of events in a cycle */
164  struct delayt
165  {
168  bool is_po;
169 
170  explicit delayt(event_idt _first):
171  first(_first), is_po(true)
172  {
173  }
174 
175  delayt(event_idt _first, event_idt _second):
176  first(_first), second(_second), is_po(false)
177  {
178  }
179 
180  delayt(event_idt _first, event_idt _second, bool _is_po):
181  first(_first), second(_second), is_po(_is_po)
182  {
183  }
184 
185  bool operator==(const delayt &other) const
186  {
187  return (is_po ? first==other.first :
188  first==other.first && second==other.second);
189  }
190 
191  bool operator<(const delayt &other) const
192  {
193  return (is_po ? first<other.first :
194  first<other.first ||
195  (first==other.first && second<other.second));
196  }
197  };
198 
199  std::set<delayt> unsafe_pairs;
200 
201  /* print events or ids in the cycles*/
202  std::string print() const;
203  std::string print_events() const;
204 
205  /* print outputs */
206  std::string print_name(memory_modelt model) const
207  {
208  return print_name(*this, model);
209  }
210  std::string print_name(memory_modelt model, bool hide_internals) const
211  {
212  if(hide_internals)
213  {
214  critical_cyclet reduced(egraph, id);
215  this->hide_internals(reduced);
216  INVARIANT(!reduced.data.empty(), "reduced must not be empty");
217  return print_name(reduced, model);
218  }
219  else
220  return print_name(*this, model);
221  }
222 
223  std::string print_unsafes() const;
224  std::string print_output() const;
225  std::string print_all(memory_modelt model,
226  std::map<std::string, std::string> &map_id2var,
227  std::map<std::string, std::string> &map_var2id,
228  bool hide_internals) const;
229 
230  void print_dot(std::ostream &str,
231  unsigned colour, memory_modelt model) const;
232 
233  bool operator<(const critical_cyclet &other) const
234  {
235  return data<other.data;
236  }
237  };
238 
239 protected:
240  /* graph contains po and com transitions */
243 
244  /* parameters limiting the exploration */
245  unsigned max_var;
246  unsigned max_po_trans;
248 
249  /* graph explorer (for each cycles collection) */
251  {
252  public:
254  {
255  }
256 
257  protected:
259 
260  /* parameters limiting the exploration */
261  unsigned max_var;
262  unsigned max_po_trans;
263 
264  /* constraints for graph exploration */
265  std::map<irep_idt, unsigned char> writes_per_variable;
266  std::map<irep_idt, unsigned char> reads_per_variable;
267  std::map<unsigned, unsigned char> events_per_thread;
268 
269  /* for thread and filtering in backtrack */
270  virtual inline bool filtering(event_idt)
271  {
272  return false;
273  }
274 
275  virtual inline std::list<event_idt>* order_filtering(
276  std::list<event_idt>* order)
277  {
278  return order;
279  }
280 
281  /* number of cycles met so far */
282  unsigned cycle_nb;
283 
284  /* events in thin-air executions met so far */
285  /* any execution blocked by thin-air is guaranteed
286  to have all its events in this set */
287  std::set<event_idt> thin_air_events;
288 
289  /* after the collection, eliminates the executions forbidden by an
290  indirect thin-air */
291  void filter_thin_air(std::set<critical_cyclet> &set_of_cycles);
292 
293  public:
295  event_grapht &_egraph,
296  unsigned _max_var,
297  unsigned _max_po_trans):
298  egraph(_egraph),
299  max_var(_max_var),
300  max_po_trans(_max_po_trans),
301  cycle_nb(0)
302  {
303  }
304 
305  /* structures for graph exploration */
306  std::map<event_idt, bool> mark;
307  std::stack<event_idt> marked_stack;
308  std::stack<event_idt> point_stack;
309 
310  std::set<event_idt> skip_tracked;
311 
313  event_idt source, unsigned number_of_cycles);
314 
315  bool backtrack(std::set<critical_cyclet> &set_of_cycles,
316  event_idt source,
317  event_idt vertex,
318  bool unsafe_met,
319  event_idt po_trans,
320  bool same_var_pair,
321  bool lwsync_met,
322  bool has_to_be_unsafe,
323  irep_idt var_to_avoid,
324  memory_modelt model);
325 
326  /* Tarjan 1972 adapted and modified for events + po-transitivity */
327  void collect_cycles(
328  std::set<critical_cyclet> &set_of_cycles,
329  memory_modelt model);
330  };
331 
332  /* explorer for thread */
334  {
335  protected:
336  const std::set<event_idt> &filter;
337 
338  public:
339  graph_conc_explorert(event_grapht &_egraph, unsigned _max_var,
340  unsigned _max_po_trans, const std::set<event_idt> &_filter)
341  :graph_explorert(_egraph, _max_var, _max_po_trans), filter(_filter)
342  {
343  }
344 
346  {
347  return filter.find(u)==filter.end();
348  }
349 
350  std::list<event_idt>* initial_filtering(std::list<event_idt>* order)
351  {
352  static std::list<event_idt> new_order;
353 
354  /* intersection */
355  for(const auto &evt : *order)
356  if(filter.find(evt)!=filter.end())
357  new_order.push_back(evt);
358 
359  return &new_order;
360  }
361  };
362 
363  /* explorer for pairs collection a la Pensieve */
365  {
366  protected:
367  std::set<event_idt> visited_nodes;
368  bool naive;
369 
370  bool find_second_event(event_idt source);
371 
372  public:
373  graph_pensieve_explorert(event_grapht &_egraph, unsigned _max_var,
374  unsigned _max_po_trans)
375  :graph_explorert(_egraph, _max_var, _max_po_trans), naive(false)
376  {}
377 
378  void set_naive() {naive=true;}
379  void collect_pairs();
380  };
381 
382 public:
383  explicit event_grapht(messaget &_message):
384  max_var(0),
385  max_po_trans(0),
386  ignore_arrays(false),
387  filter_thin_air(true),
388  filter_uniproc(true),
389  message(_message)
390  {
391  }
392 
396 
397  /* data dependencies per thread */
398  std::map<unsigned, data_dpt> map_data_dp;
399 
400  /* orders */
401  std::list<event_idt> po_order;
402  std::list<event_idt> poUrfe_order;
403 
404  std::set<std::pair<event_idt, event_idt> > loops;
405 
407  {
408  const event_idt po_no=po_graph.add_node();
409  const event_idt com_no=com_graph.add_node();
410  INVARIANT(po_no==com_no, "node added with same id in both graphs");
411  return po_no;
412  }
413 
415  {
416  return po_graph[n];
417  }
418 
419  bool has_po_edge(event_idt i, event_idt j) const
420  {
421  return po_graph.has_edge(i, j);
422  }
423 
425  {
426  return com_graph.has_edge(i, j);
427  }
428 
429  std::size_t size() const
430  {
431  return po_graph.size();
432  }
433 
435  {
436  return po_graph.in(n);
437  }
438 
440  {
441  return po_graph.out(n);
442  }
443 
445  {
446  return com_graph.in(n);
447  }
448 
450  {
451  return com_graph.out(n);
452  }
453 
455  {
456  assert(a!=b);
457  assert(operator[](a).thread==operator[](b).thread);
458  po_graph.add_edge(a, b);
459  po_order.push_back(a);
460  poUrfe_order.push_back(a);
461  }
462 
464  {
465  assert(a!=b);
466  assert(operator[](a).thread==operator[](b).thread);
467  po_graph.add_edge(a, b);
468  po_order.push_back(a);
469  poUrfe_order.push_back(a);
470  loops.insert(std::pair<event_idt, event_idt>(a, b));
471  loops.insert(std::pair<event_idt, event_idt>(b, a));
472  }
473 
475  {
476  assert(a!=b);
477  com_graph.add_edge(a, b);
478  poUrfe_order.push_back(a);
479  }
480 
482  {
483  assert(a!=b);
484  add_com_edge(a, b);
485  add_com_edge(b, a);
486  }
487 
489  {
490  po_graph.remove_edge(a, b);
491  }
492 
494  {
495  com_graph.remove_edge(a, b);
496  }
497 
499  {
500  remove_po_edge(a, b);
501  remove_com_edge(a, b);
502  }
503 
504  /* copies the sub-graph G between begin and end into G', connects
505  G.end with G'.begin, and returns G'.end */
506  void explore_copy_segment(std::set<event_idt> &explored, event_idt begin,
507  event_idt end) const;
509 
510  /* to keep track of the loop already copied */
511  std::set<std::pair<const abstract_eventt&, const abstract_eventt&>>
513 
515  {
516  return operator[](a).local;
517  }
518 
519  /* a -po-> b -- transitive */
521  {
522  if(operator[](a).thread!=operator[](b).thread)
523  return false;
524 
525  /* if back-edge, a-po->b \/ b-po->a */
526  if( loops.find(std::pair<event_idt, event_idt>(a, b))!=loops.end() )
527  return true;
528 
529  // would be true if no cycle in po
530  for(const auto &evt : po_order)
531  if(evt==a)
532  return true;
533  else if(evt==b)
534  return false;
535 
536  return false;
537  }
538 
539  void clear()
540  {
541  po_graph.clear();
542  com_graph.clear();
543  map_data_dp.clear();
544  }
545 
546  /* prints to graph.dot */
547  void print_graph();
548  void print_rec_graph(std::ofstream &file, event_idt node_id,
549  std::set<event_idt> &visited);
550 
551  /* Tarjan 1972 adapted and modified for events + po-transitivity */
552  void collect_cycles(std::set<critical_cyclet> &set_of_cycles,
553  memory_modelt model,
554  const std::set<event_idt> &filter)
555  {
556  graph_conc_explorert exploration(*this, max_var, max_po_trans, filter);
557  exploration.collect_cycles(set_of_cycles, model);
558  }
559 
560  void collect_cycles(std::set<critical_cyclet> &set_of_cycles,
561  memory_modelt model)
562  {
563  graph_explorert exploration(*this, max_var, max_po_trans);
564  exploration.collect_cycles(set_of_cycles, model);
565  }
566 
568  unsigned _max_var=0,
569  unsigned _max_po_trans=0,
570  bool _ignore_arrays=false)
571  {
572  max_var = _max_var;
573  max_po_trans = _max_po_trans;
574  ignore_arrays = _ignore_arrays;
575  }
576 
577  /* collects all the pairs of events with respectively at least one cmp,
578  regardless of the architecture (Pensieve'05 strategy) */
580  {
581  graph_pensieve_explorert exploration(*this, max_var, max_po_trans);
582  exploration.collect_pairs();
583  }
584 
586  {
587  graph_pensieve_explorert exploration(*this, max_var, max_po_trans);
588  exploration.set_naive();
589  exploration.collect_pairs();
590  }
591 };
592 #endif // CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H
event_grapht::has_po_edge
bool has_po_edge(event_idt i, event_idt j) const
Definition: event_graph.h:419
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
event_grapht::critical_cyclet::back
const value_type & back() const
Definition: event_graph.h:93
event_grapht::critical_cyclet::hide_internals
void hide_internals(critical_cyclet &reduced) const
Definition: event_graph.cpp:1157
grapht::size
std::size_t size() const
Definition: graph.h:213
event_grapht::critical_cyclet::check_AC
bool check_AC(data_typet::const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const
Definition: event_graph.cpp:187
event_grapht::critical_cyclet::is_unsafe_asm
bool is_unsafe_asm(memory_modelt model, bool fast=false)
same as is_unsafe, but with ASM fences
Definition: event_graph.cpp:563
event_grapht::com_out
const wmm_grapht::edgest & com_out(event_idt n) const
Definition: event_graph.h:449
event_grapht::graph_conc_explorert::graph_conc_explorert
graph_conc_explorert(event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans, const std::set< event_idt > &_filter)
Definition: event_graph.h:339
event_grapht::graph_explorert::graph_explorert
graph_explorert(event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)
Definition: event_graph.h:294
event_grapht::po_graph
wmm_grapht po_graph
Definition: event_graph.h:241
event_grapht::graph_pensieve_explorert::graph_pensieve_explorert
graph_pensieve_explorert(event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)
Definition: event_graph.h:373
event_grapht::critical_cyclet::delayt::is_po
bool is_po
Definition: event_graph.h:168
event_grapht::graph_pensieve_explorert::find_second_event
bool find_second_event(event_idt source)
Definition: pair_collection.cpp:67
event_grapht::critical_cyclet::compute_unsafe_pairs
void compute_unsafe_pairs(memory_modelt model)
Definition: event_graph.h:146
event_grapht::graph_explorert::extract_cycle
critical_cyclet extract_cycle(event_idt vertex, event_idt source, unsigned number_of_cycles)
extracts a (whole, unreduced) cycle from the stack.
Definition: cycle_collection.cpp:119
event_grapht::graph_explorert::egraph
event_grapht & egraph
Definition: event_graph.h:258
RMO
@ RMO
Definition: wmm.h:22
event_grapht::graph_pensieve_explorert::visited_nodes
std::set< event_idt > visited_nodes
Definition: event_graph.h:367
abstract_event.h
abstract events
event_grapht::critical_cyclet::print_name
std::string print_name(memory_modelt model, bool hide_internals) const
Definition: event_graph.h:210
event_grapht::add_undirected_com_edge
void add_undirected_com_edge(event_idt a, event_idt b)
Definition: event_graph.h:481
grapht::has_edge
bool has_edge(node_indext i, node_indext j) const
Definition: graph.h:193
data
Definition: kdev_t.h:24
grapht< abstract_eventt >
event_grapht::has_com_edge
bool has_com_edge(event_idt i, event_idt j) const
Definition: event_graph.h:424
event_grapht::map_data_dp
std::map< unsigned, data_dpt > map_data_dp
Definition: event_graph.h:398
file
Definition: kdev_t.h:19
invariant.h
event_grapht::critical_cyclet::end
const_iterator end() const
Definition: event_graph.h:80
event_grapht::filter_uniproc
bool filter_uniproc
Definition: event_graph.h:394
event_grapht::graph_explorert::filtering
virtual bool filtering(event_idt)
Definition: event_graph.h:270
event_grapht::clear
void clear()
Definition: event_graph.h:539
grapht::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:181
event_grapht::graph_explorert::writes_per_variable
std::map< irep_idt, unsigned char > writes_per_variable
Definition: event_graph.h:265
event_grapht::graph_explorert::thin_air_events
std::set< event_idt > thin_air_events
Definition: event_graph.h:287
event_grapht::critical_cyclet::is_unsafe_fast
bool is_unsafe_fast(memory_modelt model)
Definition: event_graph.h:141
event_grapht::graph_explorert::point_stack
std::stack< event_idt > point_stack
Definition: event_graph.h:308
event_grapht::graph_pensieve_explorert
Definition: event_graph.h:365
event_grapht::critical_cyclet::size
size_t size() const
Definition: event_graph.h:95
event_grapht::operator[]
grapht< abstract_eventt >::nodet & operator[](event_idt n)
Definition: event_graph.h:414
event_grapht::collect_pairs
void collect_pairs()
Definition: event_graph.h:579
event_grapht::critical_cyclet::const_iterator
data_typet::const_iterator const_iterator
Definition: event_graph.h:71
event_grapht::critical_cyclet::push_front
void push_front(T &&t)
Definition: event_graph.h:84
event_grapht::critical_cyclet::print_name
std::string print_name(memory_modelt model) const
Definition: event_graph.h:206
event_grapht::critical_cyclet::is_not_uniproc
bool is_not_uniproc(memory_modelt model) const
Definition: event_graph.h:153
event_grapht::graph_conc_explorert
Definition: event_graph.h:334
event_idt
wmm_grapht::node_indext event_idt
Definition: event_graph.h:33
event_grapht::graph_explorert::reads_per_variable
std::map< irep_idt, unsigned char > reads_per_variable
Definition: event_graph.h:266
grapht< abstract_eventt >::edgest
nodet::edgest edgest
Definition: graph.h:171
event_grapht::poUrfe_order
std::list< event_idt > poUrfe_order
Definition: event_graph.h:402
event_grapht::graph_conc_explorert::filter
const std::set< event_idt > & filter
Definition: event_graph.h:336
grapht< abstract_eventt >::node_indext
nodet::node_indext node_indext
Definition: graph.h:174
event_grapht::critical_cyclet::print_name
std::string print_name(const critical_cyclet &redyced, memory_modelt model) const
Definition: event_graph.cpp:1233
event_grapht::critical_cyclet::data
data_typet data
Definition: event_graph.h:42
event_grapht::loops
std::set< std::pair< event_idt, event_idt > > loops
Definition: event_graph.h:404
event_grapht::critical_cyclet::front
value_type & front()
Definition: event_graph.h:89
event_grapht::graph_pensieve_explorert::naive
bool naive
Definition: event_graph.h:368
event_grapht::critical_cyclet::delayt::operator==
bool operator==(const delayt &other) const
Definition: event_graph.h:185
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
event_grapht::critical_cyclet::cbegin
const_iterator cbegin() const
Definition: event_graph.h:77
grapht::in
const edgest & in(node_indext n) const
Definition: graph.h:223
event_grapht::ignore_arrays
bool ignore_arrays
Definition: event_graph.h:247
event_grapht::explore_copy_segment
void explore_copy_segment(std::set< event_idt > &explored, event_idt begin, event_idt end) const
copies the segment
Definition: event_graph.cpp:73
event_grapht::critical_cyclet::delayt
Definition: event_graph.h:165
event_grapht::po_order
std::list< event_idt > po_order
Definition: event_graph.h:401
event_grapht::max_var
unsigned max_var
Definition: event_graph.h:245
data_dp.h
data dependencies
event_grapht::remove_po_edge
void remove_po_edge(event_idt a, event_idt b)
Definition: event_graph.h:488
event_grapht::graph_explorert::collect_cycles
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
Tarjan 1972 adapted and modified for events.
Definition: cycle_collection.cpp:51
event_grapht::critical_cyclet::unsafe_pairs
std::set< delayt > unsafe_pairs
Definition: event_graph.h:199
event_grapht::critical_cyclet::end
iterator end()
Definition: event_graph.h:79
event_grapht::remove_com_edge
void remove_com_edge(event_idt a, event_idt b)
Definition: event_graph.h:493
event_grapht::copy_segment
event_idt copy_segment(event_idt begin, event_idt end)
Definition: event_graph.cpp:91
event_grapht::critical_cyclet::back
value_type & back()
Definition: event_graph.h:92
event_grapht::critical_cyclet::is_unsafe
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...
Definition: event_graph.cpp:281
data::size
int size
Definition: kdev_t.h:25
event_grapht::collect_cycles
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
Definition: event_graph.h:552
event_grapht::critical_cyclet::is_cycle
bool is_cycle()
Definition: event_graph.h:112
event_grapht::critical_cyclet::is_not_weak_uniproc
bool is_not_weak_uniproc() const
Definition: event_graph.cpp:934
event_grapht::graph_explorert::max_po_trans
unsigned max_po_trans
Definition: event_graph.h:262
event_grapht::graph_explorert::mark
std::map< event_idt, bool > mark
Definition: event_graph.h:306
event_grapht::graph_pensieve_explorert::set_naive
void set_naive()
Definition: event_graph.h:378
event_grapht::critical_cyclet::iterator
data_typet::iterator iterator
Definition: event_graph.h:69
event_grapht::critical_cyclet::delayt::delayt
delayt(event_idt _first, event_idt _second, bool _is_po)
Definition: event_graph.h:180
event_grapht::graph_explorert::backtrack
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
Definition: cycle_collection.cpp:159
event_grapht::critical_cyclet::is_not_thin_air
bool is_not_thin_air() const
Definition: event_graph.cpp:971
event_grapht::critical_cyclet::print
std::string print() const
Definition: event_graph.cpp:1019
event_grapht::critical_cyclet::begin
const_iterator begin() const
Definition: event_graph.h:76
event_grapht::critical_cyclet::operator<
bool operator<(const critical_cyclet &other) const
Definition: event_graph.h:233
event_grapht::critical_cyclet::egraph
event_grapht & egraph
Definition: event_graph.h:44
wmm_grapht
grapht< abstract_eventt > wmm_grapht
Definition: event_graph.h:30
event_grapht::critical_cyclet::cend
const_iterator cend() const
Definition: event_graph.h:81
grapht::add_edge
void add_edge(node_indext a, node_indext b)
Definition: graph.h:233
memory_modelt
memory_modelt
Definition: wmm.h:18
abstract_eventt
Definition: abstract_event.h:23
event_grapht::graph_explorert::max_var
unsigned max_var
Definition: event_graph.h:261
event_grapht::critical_cyclet::check_BC
bool check_BC(data_typet::const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const
Definition: event_graph.cpp:228
event_grapht::critical_cyclet::is_not_uniproc
bool is_not_uniproc() const
Definition: event_graph.cpp:896
event_grapht::graph_pensieve_explorert::collect_pairs
void collect_pairs()
Definition: pair_collection.cpp:25
event_grapht::graph_explorert::marked_stack
std::stack< event_idt > marked_stack
Definition: event_graph.h:307
event_grapht::add_po_back_edge
void add_po_back_edge(event_idt a, event_idt b)
Definition: event_graph.h:463
event_grapht::add_com_edge
void add_com_edge(event_idt a, event_idt b)
Definition: event_graph.h:474
event_grapht::graph_explorert::cycle_nb
unsigned cycle_nb
Definition: event_graph.h:282
grapht::out
const edgest & out(node_indext n) const
Definition: graph.h:228
event_grapht::critical_cyclet::print_unsafes
std::string print_unsafes() const
Definition: event_graph.cpp:1027
event_grapht::critical_cyclet::print_output
std::string print_output() const
Definition: event_graph.cpp:1086
event_grapht::com_graph
wmm_grapht com_graph
Definition: event_graph.h:242
graph.h
A Template Class for Graphs.
event_grapht::po_in
const wmm_grapht::edgest & po_in(event_idt n) const
Definition: event_graph.h:434
event_grapht::graph_explorert::filter_thin_air
void filter_thin_air(std::set< critical_cyclet > &set_of_cycles)
after the collection, eliminates the executions forbidden by an indirect thin-air
Definition: cycle_collection.cpp:20
event_grapht::graph_explorert::order_filtering
virtual std::list< event_idt > * order_filtering(std::list< event_idt > *order)
Definition: event_graph.h:275
event_grapht::critical_cyclet::front
const value_type & front() const
Definition: event_graph.h:90
event_grapht::size
std::size_t size() const
Definition: event_graph.h:429
event_grapht::critical_cyclet::operator()
void operator()(const critical_cyclet &cyc)
Definition: event_graph.h:102
event_grapht::graph_conc_explorert::initial_filtering
std::list< event_idt > * initial_filtering(std::list< event_idt > *order)
Definition: event_graph.h:350
event_grapht::graph_explorert
Definition: event_graph.h:251
event_grapht::critical_cyclet::push_back
void push_back(T &&t)
Definition: event_graph.h:87
event_grapht::po_out
const wmm_grapht::edgest & po_out(event_idt n) const
Definition: event_graph.h:439
event_grapht::collect_pairs_naive
void collect_pairs_naive()
Definition: event_graph.h:585
event_grapht::set_parameters_collection
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: event_graph.h:567
event_grapht
Definition: event_graph.h:36
event_grapht::critical_cyclet::begin
iterator begin()
Definition: event_graph.h:75
event_grapht::critical_cyclet::critical_cyclet
critical_cyclet(event_grapht &_egraph, unsigned _id)
Definition: event_graph.h:97
event_grapht::critical_cyclet::value_type
data_typet::value_type value_type
Definition: event_graph.h:73
event_grapht::critical_cyclet::print_dot
void print_dot(std::ostream &str, unsigned colour, memory_modelt model) const
Definition: event_graph.cpp:1538
event_grapht::graph_explorert::~graph_explorert
virtual ~graph_explorert()
Definition: event_graph.h:253
event_grapht::are_po_ordered
bool are_po_ordered(event_idt a, event_idt b)
Definition: event_graph.h:520
event_grapht::add_po_edge
void add_po_edge(event_idt a, event_idt b)
Definition: event_graph.h:454
event_grapht::com_in
const wmm_grapht::edgest & com_in(event_idt n) const
Definition: event_graph.h:444
event_grapht::message
messaget & message
Definition: event_graph.h:395
event_grapht::critical_cyclet::delayt::delayt
delayt(event_idt _first, event_idt _second)
Definition: event_graph.h:175
event_grapht::print_rec_graph
void print_rec_graph(std::ofstream &file, event_idt node_id, std::set< event_idt > &visited)
Definition: event_graph.cpp:28
event_grapht::graph_explorert::skip_tracked
std::set< event_idt > skip_tracked
Definition: event_graph.h:310
event_grapht::remove_edge
void remove_edge(event_idt a, event_idt b)
Definition: event_graph.h:498
event_grapht::critical_cyclet::print_detail
std::string print_detail(const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id) const
Definition: event_graph.cpp:1099
event_grapht::event_grapht
event_grapht(messaget &_message)
Definition: event_graph.h:383
grapht::remove_edge
void remove_edge(node_indext a, node_indext b)
Definition: graph.h:239
grapht::clear
void clear()
Definition: graph.h:261
wmm.h
memory models
event_grapht::critical_cyclet
Definition: event_graph.h:40
event_grapht::add_node
event_idt add_node()
Definition: event_graph.h:406
event_grapht::critical_cyclet::print_all
std::string print_all(memory_modelt model, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, bool hide_internals) const
Definition: event_graph.cpp:1127
event_grapht::is_local
bool is_local(event_idt a)
Definition: event_graph.h:514
event_grapht::critical_cyclet::data_typet
std::list< event_idt > data_typet
Definition: event_graph.h:41
event_grapht::filter_thin_air
bool filter_thin_air
Definition: event_graph.h:393
event_grapht::duplicated_bodies
std::set< std::pair< const abstract_eventt &, const abstract_eventt & > > duplicated_bodies
Definition: event_graph.h:512
event_grapht::critical_cyclet::delayt::operator<
bool operator<(const delayt &other) const
Definition: event_graph.h:191
event_grapht::collect_cycles
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
Definition: event_graph.h:560
event_grapht::critical_cyclet::has_user_defined_fence
bool has_user_defined_fence
Definition: event_graph.h:66
event_grapht::print_graph
void print_graph()
Definition: event_graph.cpp:56
event_grapht::max_po_trans
unsigned max_po_trans
Definition: event_graph.h:246
event_grapht::critical_cyclet::print_events
std::string print_events() const
Definition: event_graph.cpp:1074
event_grapht::graph_conc_explorert::filtering
bool filtering(event_idt u)
Definition: event_graph.h:345
event_grapht::critical_cyclet::id
unsigned id
Definition: event_graph.h:65
event_grapht::critical_cyclet::delayt::delayt
delayt(event_idt _first)
Definition: event_graph.h:170
event_grapht::critical_cyclet::delayt::second
event_idt second
Definition: event_graph.h:167
validation_modet::INVARIANT
@ INVARIANT
event_grapht::critical_cyclet::delayt::first
event_idt first
Definition: event_graph.h:166
event_grapht::graph_explorert::events_per_thread
std::map< unsigned, unsigned char > events_per_thread
Definition: event_graph.h:267