39 assert(e1->is_shared_read() || e1->is_shared_write());
40 assert(e2->is_shared_read() || e2->is_shared_write());
51 for(eventst::const_iterator
57 if(!e_it->is_shared_read() &&
58 !e_it->is_shared_write() &&
60 !e_it->is_memory_barrier())
continue;
62 dest[e_it->source.thread_nr].push_back(e_it);
74 for(eventst::const_iterator
81 per_thread_mapt::const_iterator next_thread=
83 if(next_thread==per_thread_map.end())
88 for(event_listt::const_iterator
89 n_it=next_thread->second.begin();
90 n_it!=next_thread->second.end();
93 if(!(*n_it)->is_memory_barrier())
107 const per_thread_mapt &per_thread_map)
113 for(eventst::const_iterator
120 per_thread_mapt::const_iterator next_thread=
122 if(next_thread==per_thread_map.end())
130 event_listt::const_iterator n_it=next_thread->second.begin();
132 n_it!=next_thread->second.end() &&
133 (*n_it)->is_memory_barrier();
138 if(n_it!=next_thread->second.end())
159 for(per_thread_mapt::const_iterator
160 t_it=per_thread_map.begin();
161 t_it!=per_thread_map.end();
170 for(event_listt::const_iterator
175 if((*e_it)->is_memory_barrier())
199 for(address_mapt::const_iterator
204 const a_rect &a_rec=a_it->second;
209 for(event_listt::const_iterator
210 w_it1=a_rec.
writes.begin();
211 w_it1!=a_rec.
writes.end();
214 event_listt::const_iterator next=w_it1;
217 for(event_listt::const_iterator w_it2=next;
218 w_it2!=a_rec.
writes.end();
222 if((*w_it1)->source.thread_nr==
223 (*w_it2)->source.thread_nr)
252 for(address_mapt::const_iterator
257 const a_rect &a_rec=a_it->second;
260 for(event_listt::const_iterator
261 w_prime=a_rec.
writes.begin();
262 w_prime!=a_rec.
writes.end();
265 event_listt::const_iterator next=w_prime;
268 for(event_listt::const_iterator w=next;
274 if(
po(*w_prime, *w) &&
280 else if(
po(*w, *w_prime) &&
293 for(choice_symbolst::const_iterator
299 exprt rf=c_it->second;
303 if(c_it->first.second==*w_prime && !ws1.
is_false())
315 else if(c_it->first.second==*w && !ws2.
is_false())
324 and_exprt(
r->guard, (*w_prime)->guard, ws2, rf),
330 cond,
"fr",
r->source);
symbol_exprt nondet_bool_symbol(const std::string &prefix)
void read_from(symex_target_equationt &equation)
void from_read(symex_target_equationt &equation)
virtual bool program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
std::map< unsigned, event_listt > per_thread_mapt
exprt before(event_it e1, event_it e2, unsigned axioms)
static mstreamt & eom(mstreamt &m)
void program_order(symex_target_equationt &equation)
void build_event_lists(symex_target_equationt &)
The boolean constant true.
API to expression classes.
void write_serialization_external(symex_target_equationt &equation)
The boolean constant false.
bool po(event_it e1, event_it e2)
choice_symbolst choice_symbols
void build_per_thread_map(const symex_target_equationt &equation, per_thread_mapt &dest) const
void thread_spawn(symex_target_equationt &equation, const per_thread_mapt &per_thread_map)
virtual exprt before(event_it e1, event_it e2)
eventst::const_iterator event_it
Base class for all expressions.
const std::string next_thread_id
Memory models for partial order concurrency.
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)
std::vector< event_it > event_listt
mstreamt & statistics() const
virtual void operator()(symex_target_equationt &equation)