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);
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  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
34  PRECONDITION(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 }
partial_order_concurrencyt::event_it
eventst::const_iterator event_it
Definition: partial_order_concurrency.h:30
memory_model_pso.h
Memory models for partial order concurrency.
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_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_psot::operator()
virtual void operator()(symex_target_equationt &equation)
Definition: memory_model_pso.cpp:14
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
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
memory_model_psot::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_pso.cpp:29
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
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