cprover
memory_model_pso.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_pso.h"
13 
15 {
16  statistics() << "Adding PSO constraints" << eom;
17 
18  build_event_lists(equation);
19  build_clock_type(equation);
20 
21  read_from(equation);
23  program_order(equation);
24 #ifndef CPROVER_MEMORY_MODEL_SUP_CLOCK
25  from_read(equation);
26 #endif
27 }
28 
32 {
33  assert(e1->is_shared_read() || e1->is_shared_write());
34  assert(e2->is_shared_read() || e2->is_shared_write());
35 
36  // no po relaxation within atomic sections
37  if(e1->atomic_section_id!=0 &&
38  e1->atomic_section_id==e2->atomic_section_id)
39  return false;
40 
41  // no relaxation if induced wsi
42  if(e1->is_shared_write() && e2->is_shared_write() &&
43  address(e1)==address(e2))
44  return false;
45 
46  // only read/read and read/write are maintained
47  return e1->is_shared_write();
48 }
void read_from(symex_target_equationt &equation)
irep_idt address(event_it event) const
void from_read(symex_target_equationt &equation)
Memory models for partial order concurrency.
void build_clock_type(const symex_target_equationt &)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void build_event_lists(symex_target_equationt &)
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 write_serialization_external(symex_target_equationt &equation)
mstreamt & statistics()
Definition: message.h:243
eventst::const_iterator event_it
virtual void operator()(symex_target_equationt &equation)