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