CBMC
memory_model_tsot Class Reference

#include <memory_model_tso.h>

+ Inheritance diagram for memory_model_tsot:
+ Collaboration diagram for memory_model_tsot:

Public Member Functions

 memory_model_tsot (const namespacet &_ns)
 
virtual void operator() (symex_target_equationt &equation, message_handlert &)
 
- Public Member Functions inherited from memory_model_sct
 memory_model_sct (const namespacet &_ns)
 
- Public Member Functions inherited from memory_model_baset
 memory_model_baset (const namespacet &_ns)
 
virtual ~memory_model_baset ()
 
- Public Member Functions inherited from partial_order_concurrencyt
 partial_order_concurrencyt (const namespacet &_ns)
 
virtual ~partial_order_concurrencyt ()
 

Protected Member Functions

virtual exprt before (event_it e1, event_it e2)
 
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)
 
- Protected Member Functions inherited from memory_model_sct
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)
 
void program_order (symex_target_equationt &equation)
 
void from_read (symex_target_equationt &equation)
 
void write_serialization_external (symex_target_equationt &equation)
 
- Protected Member Functions inherited from memory_model_baset
bool po (event_it e1, event_it e2)
 In-thread program order. More...
 
symbol_exprt nondet_bool_symbol (const std::string &prefix)
 
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_symbol (for potential read-write pairs) and add a constraint r.guard => \/S. More...
 
symbol_exprt register_read_from_choice_symbol (const event_it &r, const event_it &w, symex_target_equationt &equation)
 Introduce a new choice symbol s for the pair (r, w) add constraint s => (w.guard /\ r.lhs=w.lhs) add constraint s => before(w,r) [if w is from another thread]. More...
 
- Protected Member Functions inherited from partial_order_concurrencyt
void build_event_lists (symex_target_equationt &equation, message_handlert &message_handler)
 First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (with a list of reads/writes for the address of each event) 2) the numbering map (with per-thread unique number of every event) More...
 
void add_init_writes (symex_target_equationt &)
 For each shared read event and for each shared write event that appears after spawn or has false guard prepend a shared write SSA step with non-deterministic value. More...
 
irep_idt address (event_it event) const
 Produce an address ID for an event. More...
 
symbol_exprt clock (event_it e, axiomt axiom)
 Produce a clock symbol for some event. More...
 
void build_clock_type ()
 Initialize the clock_type so that it can be used to number events. More...
 
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. More...
 
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 constrain with equality between their clocks otherwise constrain with e1 clock being less than e2 clock. More...
 

Additional Inherited Members

- Public Types inherited from partial_order_concurrencyt
enum  axiomt { AX_SC_PER_LOCATION =1 , AX_NO_THINAIR =2 , AX_OBSERVATION =4 , AX_PROPAGATION =8 }
 
typedef SSA_stept eventt
 
typedef symex_target_equationt::SSA_stepst eventst
 
typedef eventst::const_iterator event_it
 
- Static Public Member Functions inherited from partial_order_concurrencyt
static irep_idt rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION)
 Build identifier for the read/write clock variable. More...
 
- Protected Types inherited from memory_model_baset
typedef std::map< std::pair< event_it, event_it >, symbol_exprtchoice_symbolst
 
typedef std::map< unsigned, event_listtper_thread_mapt
 
- Protected Types inherited from partial_order_concurrencyt
typedef std::vector< event_itevent_listt
 
typedef std::map< irep_idt, a_rectaddress_mapt
 
typedef std::map< event_it, unsigned > numberingt
 
- Static Protected Member Functions inherited from partial_order_concurrencyt
static irep_idt id (event_it event)
 Produce the symbol ID for an event. More...
 
- Protected Attributes inherited from memory_model_baset
unsigned var_cnt
 
choice_symbolst choice_symbols
 
- Protected Attributes inherited from partial_order_concurrencyt
const namespacetns
 
address_mapt address_map
 
numberingt numbering
 
typet clock_type
 

Detailed Description

Definition at line 17 of file memory_model_tso.h.

Constructor & Destructor Documentation

◆ memory_model_tsot()

memory_model_tsot::memory_model_tsot ( const namespacet _ns)
inlineexplicit

Definition at line 20 of file memory_model_tso.h.

Member Function Documentation

◆ before()

exprt memory_model_tsot::before ( event_it  e1,
event_it  e2 
)
protectedvirtual

Reimplemented from memory_model_sct.

Definition at line 34 of file memory_model_tso.cpp.

◆ operator()()

void memory_model_tsot::operator() ( symex_target_equationt equation,
message_handlert message_handler 
)
virtual

Reimplemented from memory_model_sct.

Reimplemented in memory_model_psot.

Definition at line 17 of file memory_model_tso.cpp.

◆ program_order()

void memory_model_tsot::program_order ( symex_target_equationt equation)
protected

Definition at line 56 of file memory_model_tso.cpp.

◆ program_order_is_relaxed()

bool memory_model_tsot::program_order_is_relaxed ( partial_order_concurrencyt::event_it  e1,
partial_order_concurrencyt::event_it  e2 
) const
protectedvirtual

Reimplemented from memory_model_sct.

Reimplemented in memory_model_psot.

Definition at line 40 of file memory_model_tso.cpp.


The documentation for this class was generated from the following files: