cprover
memory_model_sc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Memory model for partial order concurrency
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #include "memory_model_sc.h"
13 
14 #include <util/std_expr.h>
15 
17 {
18  statistics() << "Adding SC constraints" << eom;
19 
20  build_event_lists(equation);
22 
23  read_from(equation);
25  program_order(equation);
26  from_read(equation);
27 }
28 
30 {
32  e1, e2, AX_PROPAGATION);
33 }
34 
38 {
39  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
40  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
41 
42  return false;
43 }
44 
46  const symex_target_equationt &equation,
47  per_thread_mapt &dest) const
48 {
49  // this orders the events within a thread
50 
51  for(eventst::const_iterator
52  e_it=equation.SSA_steps.begin();
53  e_it!=equation.SSA_steps.end();
54  e_it++)
55  {
56  // concurrency-related?
57  if(!e_it->is_shared_read() &&
58  !e_it->is_shared_write() &&
59  !e_it->is_spawn() &&
60  !e_it->is_memory_barrier()) continue;
61 
62  dest[e_it->source.thread_nr].push_back(e_it);
63  }
64 }
65 
67  symex_target_equationt &equation,
68  const per_thread_mapt &per_thread_map)
69 {
70  // thread spawn: the spawn precedes the first
71  // instruction of the new thread in program order
72 
73  unsigned next_thread_id=0;
74  for(eventst::const_iterator
75  e_it=equation.SSA_steps.begin();
76  e_it!=equation.SSA_steps.end();
77  e_it++)
78  {
79  if(e_it->is_spawn())
80  {
81  per_thread_mapt::const_iterator next_thread=
82  per_thread_map.find(++next_thread_id);
83  if(next_thread==per_thread_map.end())
84  continue;
85 
86  // add a constraint for all events,
87  // considering regression/cbmc-concurrency/pthread_create_tso1
88  for(event_listt::const_iterator
89  n_it=next_thread->second.begin();
90  n_it!=next_thread->second.end();
91  n_it++)
92  {
93  if(!(*n_it)->is_memory_barrier())
95  equation,
96  before(e_it, *n_it),
97  "thread-spawn",
98  e_it->source);
99  }
100  }
101  }
102 }
103 
104 #if 0
106  symex_target_equationt &equation,
107  const per_thread_mapt &per_thread_map)
108 {
109  // thread spawn: the spawn precedes the first
110  // instruction of the new thread in program order
111 
112  unsigned next_thread_id=0;
113  for(eventst::const_iterator
114  e_it=equation.SSA_steps.begin();
115  e_it!=equation.SSA_steps.end();
116  e_it++)
117  {
118  if(is_spawn(e_it))
119  {
120  per_thread_mapt::const_iterator next_thread=
121  per_thread_map.find(++next_thread_id);
122  if(next_thread==per_thread_map.end())
123  continue;
124 
125  // For SC and several weaker memory models a memory barrier
126  // at the beginning of a thread can simply be ignored, because
127  // we enforce program order in the thread-spawn constraint
128  // anyway. Memory models with cumulative memory barriers
129  // require explicit handling of these.
130  event_listt::const_iterator n_it=next_thread->second.begin();
131  for( ;
132  n_it!=next_thread->second.end() &&
133  (*n_it)->is_memory_barrier();
134  ++n_it)
135  {
136  }
137 
138  if(n_it!=next_thread->second.end())
140  equation,
141  before(e_it, *n_it),
142  "thread-spawn",
143  e_it->source);
144  }
145  }
146 }
147 #endif
148 
150  symex_target_equationt &equation)
151 {
152  per_thread_mapt per_thread_map;
153  build_per_thread_map(equation, per_thread_map);
154 
155  thread_spawn(equation, per_thread_map);
156 
157  // iterate over threads
158 
159  for(per_thread_mapt::const_iterator
160  t_it=per_thread_map.begin();
161  t_it!=per_thread_map.end();
162  t_it++)
163  {
164  const event_listt &events=t_it->second;
165 
166  // iterate over relevant events in the thread
167 
168  event_it previous=equation.SSA_steps.end();
169 
170  for(event_listt::const_iterator
171  e_it=events.begin();
172  e_it!=events.end();
173  e_it++)
174  {
175  if((*e_it)->is_memory_barrier())
176  continue;
177 
178  if(previous==equation.SSA_steps.end())
179  {
180  // first one?
181  previous=*e_it;
182  continue;
183  }
184 
186  equation,
187  before(previous, *e_it),
188  "po",
189  (*e_it)->source);
190 
191  previous=*e_it;
192  }
193  }
194 }
195 
197  symex_target_equationt &equation)
198 {
199  for(address_mapt::const_iterator
200  a_it=address_map.begin();
201  a_it!=address_map.end();
202  a_it++)
203  {
204  const a_rect &a_rec=a_it->second;
205 
206  // This is quadratic in the number of writes
207  // per address. Perhaps some better encoding
208  // based on 'places'?
209  for(event_listt::const_iterator
210  w_it1=a_rec.writes.begin();
211  w_it1!=a_rec.writes.end();
212  ++w_it1)
213  {
214  event_listt::const_iterator next=w_it1;
215  ++next;
216 
217  for(event_listt::const_iterator w_it2=next;
218  w_it2!=a_rec.writes.end();
219  ++w_it2)
220  {
221  // external?
222  if((*w_it1)->source.thread_nr==
223  (*w_it2)->source.thread_nr)
224  continue;
225 
226  // ws is a total order, no two elements have the same rank
227  // s -> w_evt1 before w_evt2; !s -> w_evt2 before w_evt1
228 
229  symbol_exprt s=nondet_bool_symbol("ws-ext");
230 
231  // write-to-write edge
233  equation,
234  implies_exprt(s, before(*w_it1, *w_it2)),
235  "ws-ext",
236  (*w_it1)->source);
237 
239  equation,
240  implies_exprt(not_exprt(s), before(*w_it2, *w_it1)),
241  "ws-ext",
242  (*w_it1)->source);
243  }
244  }
245  }
246 }
247 
249 {
250  // from-read: (w', w) in ws and (w', r) in rf -> (r, w) in fr
251 
252  for(address_mapt::const_iterator
253  a_it=address_map.begin();
254  a_it!=address_map.end();
255  a_it++)
256  {
257  const a_rect &a_rec=a_it->second;
258 
259  // This is quadratic in the number of writes per address.
260  for(event_listt::const_iterator
261  w_prime=a_rec.writes.begin();
262  w_prime!=a_rec.writes.end();
263  ++w_prime)
264  {
265  event_listt::const_iterator next=w_prime;
266  ++next;
267 
268  for(event_listt::const_iterator w=next;
269  w!=a_rec.writes.end();
270  ++w)
271  {
272  exprt ws1, ws2;
273 
274  if(po(*w_prime, *w) &&
275  !program_order_is_relaxed(*w_prime, *w))
276  {
277  ws1=true_exprt();
278  ws2=false_exprt();
279  }
280  else if(po(*w, *w_prime) &&
281  !program_order_is_relaxed(*w, *w_prime))
282  {
283  ws1=false_exprt();
284  ws2=true_exprt();
285  }
286  else
287  {
288  ws1=before(*w_prime, *w);
289  ws2=before(*w, *w_prime);
290  }
291 
292  // smells like cubic
293  for(choice_symbolst::const_iterator
294  c_it=choice_symbols.begin();
295  c_it!=choice_symbols.end();
296  c_it++)
297  {
298  event_it r=c_it->first.first;
299  exprt rf=c_it->second;
300  exprt cond;
301  cond.make_nil();
302 
303  if(c_it->first.second==*w_prime && !ws1.is_false())
304  {
305  exprt fr=before(r, *w);
306 
307  // the guard of w_prime follows from rf; with rfi
308  // optimisation such as the previous write_symbol_primed
309  // it would even be wrong to add this guard
310  cond=
312  and_exprt(r->guard, (*w)->guard, ws1, rf),
313  fr);
314  }
315  else if(c_it->first.second==*w && !ws2.is_false())
316  {
317  exprt fr=before(r, *w_prime);
318 
319  // the guard of w follows from rf; with rfi
320  // optimisation such as the previous write_symbol_primed
321  // it would even be wrong to add this guard
322  cond=
324  and_exprt(r->guard, (*w_prime)->guard, ws2, rf),
325  fr);
326  }
327 
328  if(cond.is_not_nil())
329  add_constraint(equation,
330  cond, "fr", r->source);
331  }
332  }
333  }
334  }
335 }
partial_order_concurrencyt::event_it
eventst::const_iterator event_it
Definition: partial_order_concurrency.h:30
partial_order_concurrencyt::add_constraint
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Simplify and add a constraint to equation.
Definition: partial_order_concurrency.cpp:202
irept::make_nil
void make_nil()
Definition: irep.h:475
partial_order_concurrencyt::a_rect
Definition: partial_order_concurrency.h:56
and_exprt
Boolean AND.
Definition: std_expr.h:2137
exprt
Base class for all expressions.
Definition: expr.h:53
memory_model_baset::read_from
void read_from(symex_target_equationt &equation)
For each read r from every address we collect the choice symbols S via register_read_from_choice_symb...
Definition: memory_model.cpp:43
memory_model_sct::program_order
void program_order(symex_target_equationt &equation)
Definition: memory_model_sc.cpp:149
memory_model_baset::per_thread_mapt
std::map< unsigned, event_listt > per_thread_mapt
Definition: memory_model.h:60
memory_model_sct::write_serialization_external
void write_serialization_external(symex_target_equationt &equation)
Definition: memory_model_sc.cpp:196
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
partial_order_concurrencyt::build_clock_type
void build_clock_type()
Initialize the clock_type so that it can be used to number events.
Definition: partial_order_concurrency.cpp:160
memory_model_sct::from_read
void from_read(symex_target_equationt &equation)
Definition: memory_model_sc.cpp:248
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
partial_order_concurrencyt::before
exprt before(event_it e1, event_it e2, unsigned axioms)
Build the partial order constraint for two events: if e1 and e2 are in the same atomic section then c...
Definition: partial_order_concurrency.cpp:168
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
memory_model_sct::before
virtual exprt before(event_it e1, event_it e2)
Definition: memory_model_sc.cpp:29
partial_order_concurrencyt::build_event_lists
void build_event_lists(symex_target_equationt &)
First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (w...
Definition: partial_order_concurrency.cpp:75
partial_order_concurrencyt::address_map
address_mapt address_map
Definition: partial_order_concurrency.h:61
next_thread_id
const std::string next_thread_id
Definition: java_bytecode_concurrency_instrumentation.cpp:21
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
memory_model_baset::po
bool po(event_it e1, event_it e2)
In-thread program order.
Definition: memory_model.cpp:31
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
partial_order_concurrencyt::AX_PROPAGATION
@ AX_PROPAGATION
Definition: partial_order_concurrency.h:38
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
memory_model_sct::operator()
virtual void operator()(symex_target_equationt &equation)
Definition: memory_model_sc.cpp:16
memory_model_baset::choice_symbols
choice_symbolst choice_symbols
Definition: memory_model.h:39
memory_model_sct::thread_spawn
void thread_spawn(symex_target_equationt &equation, const per_thread_mapt &per_thread_map)
Definition: memory_model_sc.cpp:66
memory_model_baset::nondet_bool_symbol
symbol_exprt nondet_bool_symbol(const std::string &prefix)
Definition: memory_model.cpp:25
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
partial_order_concurrencyt::event_listt
std::vector< event_it > event_listt
Definition: partial_order_concurrency.h:52
memory_model_sc.h
Memory models for partial order concurrency.
partial_order_concurrencyt::a_rect::writes
event_listt writes
Definition: partial_order_concurrency.h:57
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
r
static int8_t r
Definition: irep_hash.h:59
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
std_expr.h
API to expression classes.
memory_model_sct::program_order_is_relaxed
virtual bool program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
Definition: memory_model_sc.cpp:35
memory_model_sct::build_per_thread_map
void build_per_thread_map(const symex_target_equationt &equation, per_thread_mapt &dest) const
Definition: memory_model_sc.cpp:45
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
not_exprt
Boolean negation.
Definition: std_expr.h:2843