CBMC: memory_model_tsot Class Reference

CBMC

Loading...

Searching...

No Matches

Public Member Functions | Protected Member Functions | List of all members

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

memory_model_tsot
Generated by doxygen 1.9.8