cprover
partial_order_concurrency.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Add constraints to equation encoding partial orders on events
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
13 #define CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
14 
15 #include <util/message.h>
16 
17 #include "symex_target_equation.h"
18 
20 {
21 public:
22  explicit partial_order_concurrencyt(const namespacet &_ns);
24 
27  typedef eventst::const_iterator event_it;
28 
29  // the name of a clock variable for a shared read/write
30  enum axiomt
31  {
36  };
37 
38  static irep_idt rw_clock_id(
39  event_it e,
40  axiomt axiom=AX_PROPAGATION);
41 
42 protected:
43  const namespacet &ns;
44 
45  typedef std::vector<event_it> event_listt;
46 
47  // lists of reads and writes per address
48  struct a_rect
49  {
51  };
52 
53  typedef std::map<irep_idt, a_rect> address_mapt;
55 
58 
59  // a per-thread numbering of the events
60  typedef std::map<event_it, unsigned> numberingt;
62 
63  // produces the symbol ID for an event
64  static inline irep_idt id(event_it event)
65  {
66  return event->ssa_lhs.get_identifier();
67  }
68 
69  // produces an address ID for an event
70  irep_idt address(event_it event) const
71  {
72  ssa_exprt tmp=event->ssa_lhs;
73  tmp.remove_level_2();
74  return tmp.get_identifier();
75  }
76 
77  // produce a clock symbol for some event
80  void build_clock_type();
81 
82  // preprocess and add a constraint to equation
83  void add_constraint(
84  symex_target_equationt &equation,
85  const exprt &cond,
86  const std::string &msg,
87  const symex_targett::sourcet &source) const;
88 
89  // the partial order constraint for two events
90  exprt before(event_it e1, event_it e2, unsigned axioms);
91  virtual exprt before(event_it e1, event_it e2)=0;
92 };
93 
94 #if 0
95 #include <list>
96 #include <map>
97 #include <vector>
98 #include <string>
99 
100 #include "abstract_event_structure.h"
101 
102 class memory_model_baset;
103 
104 class numbered_evtst
105 {
106  typedef abstract_eventt evtt;
107 
108 public:
109  typedef std::vector<evtt const*> ordered_evtst;
110  // NOLINTNEXTLINE(readability/identifiers)
111  typedef ordered_evtst::const_iterator const_iterator;
112  typedef std::map<evtt const*, ordered_evtst::size_type> ordered_evts_mapt;
113 
114  void add_event(const evtt &evt)
115  {
116  const ordered_evtst::size_type offset=ordered_evts.size();
117  ordered_evts.push_back(&evt);
118  if(!ordered_evts_map.insert(std::make_pair(&evt, offset)).second)
119  UNREACHABLE;
120  assert(ordered_evts.size()==ordered_evts_map.size());
121 
122  if(evt.direction==evtt::D_SYNC ||
123  evt.direction==evtt::D_LWSYNC)
124  barriers.insert(barriers.end(), offset);
125  }
126 
127  void add_events(const_iterator first, const_iterator last)
128  {
129  ordered_evts.reserve(ordered_evts.size()+last-first);
130  for( ; first!=last; ++first)
131  add_event(**first);
132  }
133 
134  const_iterator begin() const
135  {
136  return ordered_evts.begin();
137  }
138 
139  const_iterator end() const
140  {
141  return ordered_evts.end();
142  }
143 
144  const_iterator find(const evtt &evt) const
145  {
146  ordered_evts_mapt::const_iterator entry=ordered_evts_map.find(&evt);
147  if(entry==ordered_evts_map.end())
148  return end();
149 
150  return ordered_evts.begin()+entry->second;
151  }
152 
153  std::list<const_iterator> barriers_after(const evtt &evt) const
154  {
155  const_iterator entry=find(evt);
156  if(entry==end())
157  return std::list<const_iterator>();
158 
159  std::list<const_iterator> ret;
160  ordered_evtst::size_type offset=entry-begin();
161  for(std::set<ordered_evtst::size_type>::const_iterator
162  lb=barriers.lower_bound(offset);
163  lb!=barriers.end();
164  ++lb)
165  ret.push_back(ordered_evts.begin()+*lb);
166 
167  return ret;
168  }
169 
170  std::list<const_iterator> barriers_before(const evtt &evt) const
171  {
172  const_iterator entry=find(evt);
173  if(entry==end())
174  return std::list<const_iterator>();
175 
176  std::list<const_iterator> ret;
177  ordered_evtst::size_type offset=entry-begin();
178  for(std::set<ordered_evtst::size_type>::const_iterator
179  ub=barriers.begin();
180  ub!=barriers.end() && *ub<=offset;
181  ++ub)
182  ret.push_back(ordered_evts.begin()+*ub);
183 
184  return ret;
185  }
186 
187 private:
188  ordered_evtst ordered_evts;
189  ordered_evts_mapt ordered_evts_map;
190  std::set<ordered_evtst::size_type> barriers;
191 };
192 
194 {
195 public:
196  // the is-acyclic checks
197  enum acyclict
198  {
199  AC_UNIPROC=0,
200  AC_THINAIR=1,
201  AC_GHB=2,
202  AC_PPC_WS_FENCE=3,
203  AC_N_AXIOMS=4
204  };
205 
206  typedef abstract_eventt evtt;
207  typedef std::map<evtt const*, std::map<evtt const*, exprt> > adj_matrixt;
208  typedef adj_matrixt adj_matricest[AC_N_AXIOMS];
209  typedef std::list<evtt const*> per_valuet;
210  typedef std::map<irep_idt, per_valuet> per_address_mapt;
211  typedef std::vector<numbered_evtst> numbered_per_thread_evtst;
212 
214  memory_model_baset &_memory_model,
215  symex_target_equationt &_target,
216  const namespacet &_ns,
217  messaget &_message);
218 
219  void init(const abstract_events_in_program_ordert &abstract_events_in_po);
220  void add_atomic_sections();
221 
222  // collect all partial orders
223  void add_program_order(adj_matricest &po);
224  void add_read_from(adj_matricest &rf);
225  void add_write_serialisation(adj_matricest &ws);
226  void add_from_read(
227  const adj_matricest &rf,
228  const adj_matricest &ws,
229  adj_matricest &fr);
230  void add_barriers(
231  const adj_matricest &po,
232  const adj_matricest &rf,
233  const adj_matricest &fr);
234 
235  void acyclic();
236 
237  // steps as used in PLDI Power model
238 # define S_COMMIT 0
239 # define S_R_REQ 1
240 # define S_S_ACK 1
241 # define S_PROP(t) ((t+1)<<1)
243  const acyclict check,
244  const evtt &n,
245  const unsigned step) const;
247  const acyclict check,
248  const evtt &n,
249  const unsigned step,
250  const evtt::event_dirt other_dir) const;
251 
252  symbol_exprt fresh_nondet_bool();
253  void add_constraint(
254  exprt &expr,
255  const guardt &guard,
256  const symex_targett::sourcet &source,
257  const std::string &po_name);
258  void add_atomic_sections(const acyclict check);
259  void add_partial_order_constraint(
260  const acyclict check,
261  const std::string &po_name,
262  const evtt &n1,
263  const evtt &n2,
264  const exprt &cond);
265  void add_partial_order_constraint(
266  const acyclict check,
267  const std::string &po_name,
268  const evtt &n1,
269  const unsigned n1_step,
270  const evtt::event_dirt n1_o_d,
271  const evtt &n2,
272  const unsigned n2_step,
273  const evtt::event_dirt n2_o_d,
274  const exprt &cond);
275 
276  const evtt* first_of(const evtt &e1, const evtt &e2) const;
277  const numbered_evtst &get_thread(const evtt &e) const;
278  const numbered_per_thread_evtst &get_all_threads() const
279  {
280  return per_thread_evt_no;
281  }
282 
283  const namespacet &get_ns() const { return ns; }
284  messaget &get_message() { return message; }
285  std::map<std::string, unsigned> num_concurrency_constraints;
286 
287 private:
288  memory_model_baset &memory_model;
289  symex_target_equationt &target;
290  const namespacet &ns;
291  messaget &message;
292 
293  // collect all reads and writes to each address
294  per_address_mapt reads_per_address, writes_per_address;
295 
296  // initialisation events for uninitialised globals
297  std::map<irep_idt, evtt> init_val;
298 
299  // constraints added to the formula
300  const std::string prop_var;
301  unsigned prop_cnt;
302 
303  // number events according to po per thread, including parents
304  numbered_per_thread_evtst per_thread_evt_no;
305 
306  // map between events and (symbolic) integers
307  typet node_type;
308  std::map<evtt const*, unsigned> barrier_id;
309  symbol_exprt node_symbol(
310  const evtt &evt,
311  const std::string &prefix) const;
312  std::vector<std::pair<symbol_exprt, symbol_exprt>>
313  atomic_section_bounds[AC_N_AXIOMS];
314 
315  std::list<exprt> acyclic_constraints[AC_N_AXIOMS];
316  static std::string check_to_string(const acyclict check);
317 
318  // map point-wise order to a single Boolean symbol
319  typedef std::pair<evtt const*, std::pair<unsigned, evtt::event_dirt>>
320  evt_dir_pairt;
321  typedef std::map<std::pair<evt_dir_pairt, evt_dir_pairt>,
322  symbol_exprt> pointwise_mapt;
323  pointwise_mapt edge_cache[AC_N_AXIOMS];
324  typedef std::map<evtt const*,
325  std::list<std::pair<evtt const*, std::pair<exprt, std::string> > > >
326  edge_to_guardt;
327  edge_to_guardt edge_to_guard[AC_N_AXIOMS];
328 
329  void add_sub_clock_rules();
330 
331  typedef std::map<std::pair<irep_idt, irep_idt>, symbol_exprt> clock_mapt;
332  clock_mapt clock_constraint_cache;
333  symbol_exprt add_clock_constraint(
334  const symbol_exprt &n1_sym,
335  const symbol_exprt &n2_sym,
336  const symex_targett::sourcet &source,
337  const std::string &po_name);
338  const symbol_exprt &get_partial_order_constraint(
339  const acyclict check,
340  const std::string &po_name,
341  const evtt &n1,
342  const unsigned n1_step,
343  const evtt::event_dirt n1_o_d,
344  const evtt &n2,
345  const unsigned n2_step,
346  const evtt::event_dirt n2_o_d);
347  void build_partial_order_constraint(
348  const acyclict check,
349  const std::string &po_name,
350  const evtt &n1,
351  const unsigned n1_step,
352  const evtt::event_dirt n1_o_d,
353  const evtt &n2,
354  const unsigned n2_step,
355  const evtt::event_dirt n2_o_d,
356  symbol_exprt &dest);
357 
358  // debugging output
359  std::string event_to_string(const evtt &evt) const;
360  void print_graph(
361  const adj_matrixt &graph,
362  const std::string &edge_label,
363  namespacet const &ns) const;
364 };
365 #endif
366 
367 #endif // CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
The type of an expression.
Definition: type.h:22
irep_idt address(event_it event) const
Generate Equation using Symbolic Execution.
const irep_idt & get_identifier() const
Definition: std_expr.h:128
symbol_exprt clock(event_it e, axiomt axiom)
Definition: guard.h:19
unsignedbv_typet size_type()
Definition: c_types.cpp:58
exprt before(event_it e1, event_it e2, unsigned axioms)
static irep_idt id(event_it event)
void build_event_lists(symex_target_equationt &)
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
std::map< irep_idt, a_rect > address_mapt
void remove_level_2()
Definition: ssa_expr.h:101
void add_init_writes(symex_target_equationt &)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
partial_order_concurrencyt(const namespacet &_ns)
std::list< SSA_stept > SSA_stepst
eventst::const_iterator event_it
Base class for all expressions.
Definition: expr.h:42
#define UNREACHABLE
Definition: invariant.h:271
std::map< event_it, unsigned > numberingt
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::vector< event_it > event_listt
symex_target_equationt::SSA_stepst eventst
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_target_equationt::SSA_stept eventt