CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/memory_model_sc.cpp Source File

CBMC
Loading...
Searching...
No Matches
memory_model_sc.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Memory model for partial order concurrency
4
5Author: 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
17operator()(symex_target_equationt &equation, message_handlert &message_handler)
18{
19 messaget log{message_handler};
20 log.statistics() << "Adding SC constraints" << messaget::eom;
21
22 build_event_lists(equation, message_handler);
24
25 read_from(equation);
27 program_order(equation);
28 from_read(equation);
29}
30
36
40{
41 PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
42 PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
43
44 return false;
45}
46
48 const symex_target_equationt &equation,
49 per_thread_mapt &dest) const
50{
51 // this orders the events within a thread
52
53 for(eventst::const_iterator
54 e_it=equation.SSA_steps.begin();
55 e_it!=equation.SSA_steps.end();
56 e_it++)
57 {
58 // concurrency-related?
59 if(!e_it->is_shared_read() &&
60 !e_it->is_shared_write() &&
61 !e_it->is_spawn() &&
62 !e_it->is_memory_barrier()) continue;
63
64 dest[e_it->source.thread_nr].push_back(e_it);
65 }
66}
67
69 symex_target_equationt &equation,
71{
72 // thread spawn: the spawn precedes the first
73 // instruction of the new thread in program order
74
75 unsigned next_thread_id=0;
76 for(eventst::const_iterator
77 e_it=equation.SSA_steps.begin();
78 e_it!=equation.SSA_steps.end();
79 e_it++)
80 {
81 if(e_it->is_spawn())
82 {
83 per_thread_mapt::const_iterator next_thread=
86 continue;
87
88 // add a constraint for all events,
89 // considering regression/cbmc-concurrency/pthread_create_tso1
90 for(event_listt::const_iterator
91 n_it=next_thread->second.begin();
92 n_it!=next_thread->second.end();
93 n_it++)
94 {
95 if(!(*n_it)->is_memory_barrier())
97 equation,
98 before(e_it, *n_it),
99 "thread-spawn",
100 e_it->source);
101 }
102 }
103 }
104}
105
106#if 0
107void memory_model_sct::thread_spawn(
108 symex_target_equationt &equation,
109 const per_thread_mapt &per_thread_map)
110{
111 // thread spawn: the spawn precedes the first
112 // instruction of the new thread in program order
113
114 unsigned next_thread_id=0;
115 for(eventst::const_iterator
116 e_it=equation.SSA_steps.begin();
117 e_it!=equation.SSA_steps.end();
118 e_it++)
119 {
120 if(is_spawn(e_it))
121 {
122 per_thread_mapt::const_iterator next_thread=
123 per_thread_map.find(++next_thread_id);
124 if(next_thread==per_thread_map.end())
125 continue;
126
127 // For SC and several weaker memory models a memory barrier
128 // at the beginning of a thread can simply be ignored, because
129 // we enforce program order in the thread-spawn constraint
130 // anyway. Memory models with cumulative memory barriers
131 // require explicit handling of these.
132 event_listt::const_iterator n_it=next_thread->second.begin();
133 for( ;
134 n_it!=next_thread->second.end() &&
135 (*n_it)->is_memory_barrier();
136 ++n_it)
137 {
138 }
139
140 if(n_it!=next_thread->second.end())
141 add_constraint(
142 equation,
143 before(e_it, *n_it),
144 "thread-spawn",
145 e_it->source);
146 }
147 }
148}
149#endif
150
152 symex_target_equationt &equation)
153{
156
157 thread_spawn(equation, per_thread_map);
158
159 // iterate over threads
160
161 for(per_thread_mapt::const_iterator
162 t_it=per_thread_map.begin();
163 t_it!=per_thread_map.end();
164 t_it++)
165 {
166 const event_listt &events=t_it->second;
167
168 // iterate over relevant events in the thread
169
170 event_it previous=equation.SSA_steps.end();
171
172 for(event_listt::const_iterator
173 e_it=events.begin();
174 e_it!=events.end();
175 e_it++)
176 {
177 if((*e_it)->is_memory_barrier())
178 continue;
179
180 if(previous==equation.SSA_steps.end())
181 {
182 // first one?
183 previous=*e_it;
184 continue;
185 }
186
188 equation,
189 before(previous, *e_it),
190 "po",
191 (*e_it)->source);
192
193 previous=*e_it;
194 }
195 }
196}
197
199 symex_target_equationt &equation)
200{
201 for(address_mapt::const_iterator
202 a_it=address_map.begin();
203 a_it!=address_map.end();
204 a_it++)
205 {
206 const a_rect &a_rec=a_it->second;
207
208 // This is quadratic in the number of writes
209 // per address. Perhaps some better encoding
210 // based on 'places'?
211 for(event_listt::const_iterator
212 w_it1=a_rec.writes.begin();
213 w_it1!=a_rec.writes.end();
214 ++w_it1)
215 {
216 event_listt::const_iterator next=w_it1;
217 ++next;
218
219 for(event_listt::const_iterator w_it2=next;
220 w_it2!=a_rec.writes.end();
221 ++w_it2)
222 {
223 // external?
224 if((*w_it1)->source.thread_nr==
225 (*w_it2)->source.thread_nr)
226 continue;
227
228 // ws is a total order, no two elements have the same rank
229 // s -> w_evt1 before w_evt2; !s -> w_evt2 before w_evt1
230
232
233 // write-to-write edge
235 equation,
237 "ws-ext",
238 (*w_it1)->source);
239
241 equation,
243 "ws-ext",
244 (*w_it1)->source);
245 }
246 }
247 }
248}
249
251{
252 // from-read: (w', w) in ws and (w', r) in rf -> (r, w) in fr
253
254 for(address_mapt::const_iterator
255 a_it=address_map.begin();
256 a_it!=address_map.end();
257 a_it++)
258 {
259 const a_rect &a_rec=a_it->second;
260
261 // This is quadratic in the number of writes per address.
262 for(event_listt::const_iterator
263 w_prime=a_rec.writes.begin();
264 w_prime!=a_rec.writes.end();
265 ++w_prime)
266 {
267 event_listt::const_iterator next=w_prime;
268 ++next;
269
270 for(event_listt::const_iterator w=next;
271 w!=a_rec.writes.end();
272 ++w)
273 {
274 exprt ws1, ws2;
275
276 if(po(*w_prime, *w) &&
278 {
279 ws1=true_exprt();
281 }
282 else if(po(*w, *w_prime) &&
284 {
286 ws2=true_exprt();
287 }
288 else
289 {
290 ws1=before(*w_prime, *w);
291 ws2=before(*w, *w_prime);
292 }
293
294 // smells like cubic
295 for(choice_symbolst::const_iterator
296 c_it=choice_symbols.begin();
297 c_it!=choice_symbols.end();
298 c_it++)
299 {
300 event_it r=c_it->first.first;
301 exprt rf=c_it->second;
302 exprt cond;
303 cond.make_nil();
304
305 if(c_it->first.second == *w_prime && ws1 != false)
306 {
307 exprt fr=before(r, *w);
308
309 // the guard of w_prime follows from rf; with rfi
310 // optimisation such as the previous write_symbol_primed
311 // it would even be wrong to add this guard
312 cond=
314 and_exprt(r->guard, (*w)->guard, ws1, rf),
315 fr);
316 }
317 else if(c_it->first.second == *w && ws2 != false)
318 {
320
321 // the guard of w follows from rf; with rfi
322 // optimisation such as the previous write_symbol_primed
323 // it would even be wrong to add this guard
324 cond=
326 and_exprt(r->guard, (*w_prime)->guard, ws2, rf),
327 fr);
328 }
329
330 if(cond.is_not_nil())
331 add_constraint(equation,
332 cond, "fr", r->source);
333 }
334 }
335 }
336 }
337}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
Base class for all expressions.
Definition expr.h:57
The Boolean constant false.
Definition std_expr.h:3135
Boolean implication.
Definition std_expr.h:2154
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
symbol_exprt nondet_bool_symbol(const std::string &prefix)
bool po(event_it e1, event_it e2)
In-thread program order.
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...
choice_symbolst choice_symbols
Definition memory_model.h:39
std::map< unsigned, event_listt > per_thread_mapt
Definition memory_model.h:60
virtual void operator()(symex_target_equationt &equation, message_handlert &)
void build_per_thread_map(const symex_target_equationt &equation, per_thread_mapt &dest) const
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
void program_order(symex_target_equationt &equation)
void thread_spawn(symex_target_equationt &equation, const per_thread_mapt &per_thread_map)
void write_serialization_external(symex_target_equationt &equation)
virtual exprt before(event_it e1, event_it e2)
Definition message.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
Boolean negation.
Definition std_expr.h:2388
std::vector< event_it > event_listt
address_mapt address_map
@ AX_PROPAGATION
void build_event_lists(symex_target_equationt &equation, message_handlert &message_handler)
First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (w...
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...
void build_clock_type()
Initialize the clock_type so that it can be used to number events.
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.
eventst::const_iterator event_it
Expression to hold a symbol (variable)
Definition std_expr.h:132
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
SSA_stepst SSA_steps
The Boolean constant true.
Definition std_expr.h:3126
r
static int8_t r
Definition irep_hash.h:60
const std::string next_thread_id
double log(double x)
Definition math.c:2416
Memory models for partial order concurrency.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.

AltStyle によって変換されたページ (->オリジナル) /