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.
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.
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].
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)
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.
irep_idt	address (event_it event) const
	Produce an address ID for an event.
symbol_exprt	clock (event_it e, axiomt axiom)
	Produce a clock symbol for some event.
void	build_clock_type ()
	Initialize the clock_type so that it can be used to number events.
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.
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.

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.
Protected Types inherited from memory_model_baset
typedef std::map< std::pair< event_it, event_it >, symbol_exprt >	choice_symbolst
typedef std::map< unsigned, event_listt >	per_thread_mapt
Protected Types inherited from partial_order_concurrencyt
typedef std::vector< event_it >	event_listt
typedef std::map< irep_idt, a_rect >	address_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.
Protected Attributes inherited from memory_model_baset
unsigned	var_cnt
choice_symbolst	choice_symbols
Protected Attributes inherited from partial_order_concurrencyt
const namespacet &	ns
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:

• /home/runner/work/cbmc/cbmc/src/goto-symex/memory_model_tso.h
• /home/runner/work/cbmc/cbmc/src/goto-symex/memory_model_tso.cpp