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 }
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
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_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
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
memory_model_tsot::program_order
void program_order(symex_target_equationt &equation)
Definition: memory_model_tso.cpp:54
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
partial_order_concurrencyt::ns
const namespacet & ns
Definition: partial_order_concurrency.h:50
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::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
or_exprt
Boolean OR.
Definition: std_expr.h:2245
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
irept::is_nil
bool is_nil() const
Definition: irep.h:398
memory_model_tsot::operator()
virtual void operator()(symex_target_equationt &equation)
Definition: memory_model_tso.cpp:17
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
partial_order_concurrencyt::AX_PROPAGATION
@ AX_PROPAGATION
Definition: partial_order_concurrency.h:38
partial_order_concurrencyt::AX_SC_PER_LOCATION
@ AX_SC_PER_LOCATION
Definition: partial_order_concurrency.h:35
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
simplify_expr.h
memory_model_tso.h
Memory models for partial order concurrency.
memory_model_tsot::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_tso.cpp:38
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_tsot::before
virtual exprt before(event_it e1, event_it e2)
Definition: memory_model_tso.cpp:32
partial_order_concurrencyt::event_listt
std::vector< event_it > event_listt
Definition: partial_order_concurrency.h:52
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
std_expr.h
API to expression classes.
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
partial_order_concurrencyt::address
irep_idt address(event_it event) const
Produce an address ID for an event.
Definition: partial_order_concurrency.h:93
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35