12 #ifndef CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
13 #define CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
87 return event->ssa_lhs.get_identifier();
117 const std::string &msg,
138 #include "abstract_event_structure.h"
147 typedef std::vector<evtt const*> ordered_evtst;
149 typedef ordered_evtst::const_iterator const_iterator;
150 typedef std::map<evtt const*, ordered_evtst::size_type> ordered_evts_mapt;
152 void add_event(
const evtt &evt)
155 ordered_evts.push_back(&evt);
156 if(!ordered_evts_map.insert(std::make_pair(&evt, offset)).second)
158 assert(ordered_evts.size()==ordered_evts_map.size());
160 if(evt.direction==evtt::D_SYNC ||
161 evt.direction==evtt::D_LWSYNC)
162 barriers.insert(barriers.end(), offset);
165 void add_events(const_iterator first, const_iterator last)
167 ordered_evts.reserve(ordered_evts.size()+last-first);
168 for( ; first!=last; ++first)
172 const_iterator begin()
const
174 return ordered_evts.begin();
177 const_iterator end()
const
179 return ordered_evts.end();
182 const_iterator find(
const evtt &evt)
const
184 ordered_evts_mapt::const_iterator entry=ordered_evts_map.find(&evt);
185 if(entry==ordered_evts_map.end())
188 return ordered_evts.begin()+entry->second;
191 std::list<const_iterator> barriers_after(
const evtt &evt)
const
193 const_iterator entry=find(evt);
195 return std::list<const_iterator>();
197 std::list<const_iterator> ret;
199 for(std::set<ordered_evtst::size_type>::const_iterator
200 lb=barriers.lower_bound(offset);
203 ret.push_back(ordered_evts.begin()+*lb);
208 std::list<const_iterator> barriers_before(
const evtt &evt)
const
210 const_iterator entry=find(evt);
212 return std::list<const_iterator>();
214 std::list<const_iterator> ret;
216 for(std::set<ordered_evtst::size_type>::const_iterator
218 ub!=barriers.end() && *ub<=offset;
220 ret.push_back(ordered_evts.begin()+*ub);
226 ordered_evtst ordered_evts;
227 ordered_evts_mapt ordered_evts_map;
228 std::set<ordered_evtst::size_type> barriers;
245 typedef std::map<evtt const*, std::map<evtt const*, exprt> > adj_matrixt;
246 typedef adj_matrixt adj_matricest[AC_N_AXIOMS];
247 typedef std::list<evtt const*> per_valuet;
248 typedef std::map<irep_idt, per_valuet> per_address_mapt;
249 typedef std::vector<numbered_evtst> numbered_per_thread_evtst;
257 void init(
const abstract_events_in_program_ordert &abstract_events_in_po);
258 void add_atomic_sections();
261 void add_program_order(adj_matricest &po);
262 void add_read_from(adj_matricest &rf);
263 void add_write_serialisation(adj_matricest &ws);
265 const adj_matricest &rf,
266 const adj_matricest &ws,
269 const adj_matricest &po,
270 const adj_matricest &rf,
271 const adj_matricest &fr);
279 # define S_PROP(t) ((t+1)<<1)
281 const acyclict check,
283 const unsigned step)
const;
285 const acyclict check,
288 const evtt::event_dirt other_dir)
const;
295 const std::string &po_name);
296 void add_atomic_sections(
const acyclict check);
297 void add_partial_order_constraint(
298 const acyclict check,
299 const std::string &po_name,
303 void add_partial_order_constraint(
304 const acyclict check,
305 const std::string &po_name,
307 const unsigned n1_step,
308 const evtt::event_dirt n1_o_d,
310 const unsigned n2_step,
311 const evtt::event_dirt n2_o_d,
314 const evtt* first_of(
const evtt &e1,
const evtt &e2)
const;
315 const numbered_evtst &get_thread(
const evtt &e)
const;
316 const numbered_per_thread_evtst &get_all_threads()
const
318 return per_thread_evt_no;
323 std::map<std::string, unsigned> num_concurrency_constraints;
332 per_address_mapt reads_per_address, writes_per_address;
335 std::map<irep_idt, evtt> init_val;
338 const std::string prop_var;
342 numbered_per_thread_evtst per_thread_evt_no;
346 std::map<evtt const*, unsigned> barrier_id;
349 const std::string &prefix)
const;
350 std::vector<std::pair<symbol_exprt, symbol_exprt>>
351 atomic_section_bounds[AC_N_AXIOMS];
353 std::list<exprt> acyclic_constraints[AC_N_AXIOMS];
354 static std::string check_to_string(
const acyclict check);
357 typedef std::pair<evtt const*, std::pair<unsigned, evtt::event_dirt>>
359 typedef std::map<std::pair<evt_dir_pairt, evt_dir_pairt>,
361 pointwise_mapt edge_cache[AC_N_AXIOMS];
362 typedef std::map<evtt
const*,
363 std::list<std::pair<evtt const*, std::pair<exprt, std::string> > > >
365 edge_to_guardt edge_to_guard[AC_N_AXIOMS];
367 void add_sub_clock_rules();
369 typedef std::map<std::pair<irep_idt, irep_idt>,
symbol_exprt> clock_mapt;
370 clock_mapt clock_constraint_cache;
375 const std::string &po_name);
377 const acyclict check,
378 const std::string &po_name,
380 const unsigned n1_step,
381 const evtt::event_dirt n1_o_d,
383 const unsigned n2_step,
384 const evtt::event_dirt n2_o_d);
385 void build_partial_order_constraint(
386 const acyclict check,
387 const std::string &po_name,
389 const unsigned n1_step,
390 const evtt::event_dirt n1_o_d,
392 const unsigned n2_step,
393 const evtt::event_dirt n2_o_d,
397 std::string event_to_string(
const evtt &evt)
const;
399 const adj_matrixt &graph,
400 const std::string &edge_label,
405 #endif // CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H