cprover
memory_model_tso.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_tso.h"
13 
14 #include <util/std_expr.h>
15 #include <util/simplify_expr.h>
16 
18 {
19  statistics() << "Adding TSO constraints" << eom;
20 
21  build_event_lists(equation);
23 
24  read_from(equation);
26  program_order(equation);
27 #ifndef CPROVER_MEMORY_MODEL_SUP_CLOCK
28  from_read(equation);
29 #endif
30 }
31 
33 {
36 }
37 
41 {
42  assert(e1->is_shared_read() || e1->is_shared_write());
43  assert(e2->is_shared_read() || e2->is_shared_write());
44 
45  // no po relaxation within atomic sections
46  if(e1->atomic_section_id!=0 &&
47  e1->atomic_section_id==e2->atomic_section_id)
48  return false;
49 
50  // write to read program order is relaxed
51  return e1->is_shared_write() && e2->is_shared_read();
52 }
53 
55  symex_target_equationt &equation)
56 {
57  per_thread_mapt per_thread_map;
58  build_per_thread_map(equation, per_thread_map);
59 
60  thread_spawn(equation, per_thread_map);
61 
62  // iterate over threads
63 
64  for(per_thread_mapt::const_iterator
65  t_it=per_thread_map.begin();
66  t_it!=per_thread_map.end();
67  t_it++)
68  {
69  const event_listt &events=t_it->second;
70 
71  // iterate over relevant events in the thread
72 
73  for(event_listt::const_iterator
74  e_it=events.begin();
75  e_it!=events.end();
76  e_it++)
77  {
78  if((*e_it)->is_memory_barrier())
79  continue;
80 
81  event_listt::const_iterator next=e_it;
82  ++next;
83 
84  exprt mb_guard_r, mb_guard_w;
85  mb_guard_r.make_false();
86  mb_guard_w.make_false();
87 
88  for(event_listt::const_iterator
89  e_it2=next;
90  e_it2!=events.end();
91  e_it2++)
92  {
93  if(((*e_it)->is_spawn() && !(*e_it2)->is_memory_barrier()) ||
94  (*e_it2)->is_spawn())
95  {
97  equation,
98  before(*e_it, *e_it2),
99  "po",
100  (*e_it)->source);
101 
102  if((*e_it2)->is_spawn())
103  break;
104  else
105  continue;
106  }
107 
108  if((*e_it2)->is_memory_barrier())
109  {
110  const codet &code = (*e_it2)->source.pc->code;
111 
112  if((*e_it)->is_shared_read() &&
113  !code.get_bool(ID_RRfence) &&
114  !code.get_bool(ID_RWfence))
115  continue;
116  else if((*e_it)->is_shared_write() &&
117  !code.get_bool(ID_WRfence) &&
118  !code.get_bool(ID_WWfence))
119  continue;
120 
121  if(code.get_bool(ID_RRfence) ||
122  code.get_bool(ID_WRfence))
123  mb_guard_r=or_exprt(mb_guard_r, (*e_it2)->guard);
124 
125  if(code.get_bool(ID_RWfence) ||
126  code.get_bool(ID_WWfence))
127  mb_guard_w=or_exprt(mb_guard_w, (*e_it2)->guard);
128 
129  continue;
130  }
131 
132  exprt cond=true_exprt();
133  exprt ordering=nil_exprt();
134 
135  if(address(*e_it)==address(*e_it2))
136  {
138  *e_it, *e_it2, AX_SC_PER_LOCATION);
139  }
140  else if(program_order_is_relaxed(*e_it, *e_it2))
141  {
142  if((*e_it2)->is_shared_read())
143  cond=mb_guard_r;
144  else
145  cond=mb_guard_w;
146 
147  simplify(cond, ns);
148  }
149 
150  if(!cond.is_false())
151  {
152  if(ordering.is_nil())
154  *e_it, *e_it2, AX_PROPAGATION);
155 
157  equation,
158  implies_exprt(cond, ordering),
159  "po",
160  (*e_it)->source);
161  }
162  }
163  }
164  }
165 }
void read_from(symex_target_equationt &equation)
irep_idt address(event_it event) const
void from_read(symex_target_equationt &equation)
bool is_nil() const
Definition: irep.h:172
boolean OR
Definition: std_expr.h:2391
std::map< unsigned, event_listt > per_thread_mapt
Definition: memory_model.h:42
bool is_false() const
Definition: expr.cpp:131
exprt before(event_it e1, event_it e2, unsigned axioms)
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void build_event_lists(symex_target_equationt &)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
boolean implication
Definition: std_expr.h:2339
The boolean constant true.
Definition: std_expr.h:4486
virtual bool program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
The NIL expression.
Definition: std_expr.h:4508
void program_order(symex_target_equationt &equation)
virtual exprt before(event_it e1, event_it e2)
API to expression classes.
virtual void operator()(symex_target_equationt &equation)
void write_serialization_external(symex_target_equationt &equation)
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)
eventst::const_iterator event_it
Base class for all expressions.
Definition: expr.h:42
void make_false()
Definition: expr.cpp:150
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
std::vector< event_it > event_listt
A statement in a programming language.
Definition: std_code.h:21
mstreamt & statistics() const
Definition: message.h:322
bool simplify(exprt &expr, const namespacet &ns)