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  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
43  PRECONDITION(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 = false_exprt();
85  exprt mb_guard_w = false_exprt();
86 
87  for(event_listt::const_iterator
88  e_it2=next;
89  e_it2!=events.end();
90  e_it2++)
91  {
92  if(((*e_it)->is_spawn() && !(*e_it2)->is_memory_barrier()) ||
93  (*e_it2)->is_spawn())
94  {
96  equation,
97  before(*e_it, *e_it2),
98  "po",
99  (*e_it)->source);
100 
101  if((*e_it2)->is_spawn())
102  break;
103  else
104  continue;
105  }
106 
107  if((*e_it2)->is_memory_barrier())
108  {
109  const codet &code = (*e_it2)->source.pc->code;
110 
111  if((*e_it)->is_shared_read() &&
112  !code.get_bool(ID_RRfence) &&
113  !code.get_bool(ID_RWfence))
114  continue;
115  else if((*e_it)->is_shared_write() &&
116  !code.get_bool(ID_WRfence) &&
117  !code.get_bool(ID_WWfence))
118  continue;
119 
120  if(code.get_bool(ID_RRfence) ||
121  code.get_bool(ID_WRfence))
122  mb_guard_r=or_exprt(mb_guard_r, (*e_it2)->guard);
123 
124  if(code.get_bool(ID_RWfence) ||
125  code.get_bool(ID_WWfence))
126  mb_guard_w=or_exprt(mb_guard_w, (*e_it2)->guard);
127 
128  continue;
129  }
130 
131  exprt cond=true_exprt();
132  exprt ordering=nil_exprt();
133 
134  if(address(*e_it)==address(*e_it2))
135  {
137  *e_it, *e_it2, AX_SC_PER_LOCATION);
138  }
139  else if(program_order_is_relaxed(*e_it, *e_it2))
140  {
141  if((*e_it2)->is_shared_read())
142  cond=mb_guard_r;
143  else
144  cond=mb_guard_w;
145 
146  simplify(cond, ns);
147  }
148 
149  if(!cond.is_false())
150  {
151  if(ordering.is_nil())
153  *e_it, *e_it2, AX_PROPAGATION);
154 
156  equation,
157  implies_exprt(cond, ordering),
158  "po",
159  (*e_it)->source);
160  }
161  }
162  }
163  }
164 }
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:2531
std::map< unsigned, event_listt > per_thread_mapt
Definition: memory_model.h:42
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
exprt before(event_it e1, event_it e2, unsigned axioms)
void build_event_lists(symex_target_equationt &)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
Boolean implication.
Definition: std_expr.h:2485
The Boolean constant true.
Definition: std_expr.h:4443
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:4461
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)
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
void write_serialization_external(symex_target_equationt &equation)
The Boolean constant false.
Definition: std_expr.h:4452
static eomt eom
Definition: message.h:284
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:54
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
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
mstreamt & statistics() const
Definition: message.h:406
bool simplify(exprt &expr, const namespacet &ns)