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