cprover
abstract_event.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: abstract events
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
16 
17 #include <util/source_location.h>
18 #include <util/graph.h>
19 
20 #include "wmm.h"
21 
22 class abstract_eventt:public graph_nodet<empty_edget>
23 {
24 protected:
26  memory_modelt model, bool lwsync_met) const;
27 
28 public:
29  /* for now, both fence functions and asm fences accepted */
30  enum class operationt { Write, Read, Fence, Lwfence, ASMfence };
31 
33  unsigned thread;
35  unsigned id;
37  bool local;
38 
39  // for ASMfence
40  bool WRfence;
41  bool WWfence;
42  bool RRfence;
43  bool RWfence;
44  bool WWcumul;
45  bool RWcumul;
46  bool RRcumul;
47 
49  {
50  }
51 
53  operationt _op, unsigned _th, irep_idt _var,
54  unsigned _id, source_locationt _loc, bool _local)
55  :operation(_op), thread(_th), variable(_var), id(_id),
56  source_location(_loc), local(_local)
57  {
58  }
59 
61  operationt _op,
62  unsigned _th,
63  irep_idt _var,
64  unsigned _id,
65  source_locationt _loc,
66  bool _local,
67  bool WRf,
68  bool WWf,
69  bool RRf,
70  bool RWf,
71  bool WWc,
72  bool RWc,
73  bool RRc):
74  operation(_op),
75  thread(_th),
76  variable(_var),
77  id(_id),
78  source_location(_loc),
79  local(_local),
80  WRfence(RWf),
81  WWfence(WWf),
82  RRfence(RRf),
83  RWfence(WRf),
84  WWcumul(WWc),
85  RWcumul(RWc),
86  RRcumul(RRc)
87  {
88  }
89 
90  /* post declaration (through graph) -- doesn't copy */
91  void operator()(const abstract_eventt &other)
92  {
93  operation=other.operation;
94  thread=other.thread;
95  variable=other.variable;
96  id=other.id;
97  source_location=other.source_location;
98  local=other.local;
99  }
100 
101  bool operator==(const abstract_eventt &other) const
102  {
103  return (id == other.id);
104  }
105 
106  bool operator<(const abstract_eventt &other) const
107  {
108  return (id < other.id);
109  }
110 
111  bool is_fence() const
112  {
113  return operation==operationt::Fence ||
114  operation==operationt::Lwfence ||
115  operation==operationt::ASMfence;
116  }
117 
118  /* checks the safety of the pair locally (i.e., w/o taking fences
119  or dependencies into account -- use is_unsafe on the whole
120  critical cycle for this) */
121  bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
122  {
123  return unsafe_pair_lwfence_param(next, model, false);
124  }
125 
127  const abstract_eventt &next,
128  memory_modelt model) const
129  {
130  return unsafe_pair_lwfence_param(next, model, true);
131  }
132 
133  bool unsafe_pair_asm(
134  const abstract_eventt &next,
135  memory_modelt model,
136  unsigned char met) const;
137 
138  std::string get_operation() const
139  {
140  switch(operation)
141  {
142  case operationt::Write: return "W";
143  case operationt::Read: return "R";
144  case operationt::Fence: return "F";
145  case operationt::Lwfence: return "f";
146  case operationt::ASMfence: return "asm:";
147  }
148  assert(false);
149  return "?";
150  }
151 
153  const abstract_eventt &second) const
154  {
155  return
156  (WRfence &&
157  first.operation==operationt::Write &&
158  second.operation==operationt::Read) ||
159  ((WWfence || WWcumul) &&
160  first.operation==operationt::Write &&
161  second.operation==operationt::Write) ||
162  ((RWfence || RWcumul) &&
163  first.operation==operationt::Read &&
164  second.operation==operationt::Write) ||
165  ((RRfence || RRcumul) &&
166  first.operation==operationt::Read &&
167  second.operation==operationt::Read);
168  }
169 
170  bool is_direct() const { return WWfence || WRfence || RRfence || RWfence; }
171  bool is_cumul() const { return WWcumul || RWcumul || RRcumul; }
172 
173  unsigned char fence_value() const
174  {
175  unsigned char value = WRfence + 2*WWfence + 4*RRfence + 8*RWfence
176  + 16*WWcumul + 32*RWcumul + 64*RRcumul;
177  return value;
178  }
179 };
180 
181 inline std::ostream &operator<<(
182  std::ostream &s,
183  const abstract_eventt &e)
184 {
185  return s << e.get_operation() << e.variable;
186 }
187 
188 #endif // CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
memory models
bool unsafe_pair_lwfence_param(const abstract_eventt &next, memory_modelt model, bool lwsync_met) const
bool operator<(const abstract_eventt &other) const
bool unsafe_pair_asm(const abstract_eventt &next, memory_modelt model, unsigned char met) const
operationt operation
bool is_fence() const
bool is_cumul() const
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
unsigned char fence_value() const
abstract_eventt(operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local, bool WRf, bool WWf, bool RRf, bool RWf, bool WWc, bool RWc, bool RRc)
memory_modelt
Definition: wmm.h:17
void operator()(const abstract_eventt &other)
bool is_corresponding_fence(const abstract_eventt &first, const abstract_eventt &second) const
bool unsafe_pair_lwfence(const abstract_eventt &next, memory_modelt model) const
abstract_eventt(operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local)
std::string get_operation() const
bool operator==(const abstract_eventt &other) const
A Template Class for Graphs.
bool is_direct() const
source_locationt source_location
This class represents a node in a directed graph.
Definition: graph.h:33
std::ostream & operator<<(std::ostream &s, const abstract_eventt &e)