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_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. More... | |
| 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()
|
inlineexplicit |
Definition at line 20 of file memory_model_tso.h.
Member Function Documentation
◆ before()
Reimplemented from memory_model_sct.
Definition at line 34 of file memory_model_tso.cpp.
◆ operator()()
|
virtual |
Reimplemented from memory_model_sct.
Reimplemented in memory_model_psot.
Definition at line 17 of file memory_model_tso.cpp.
◆ program_order()
|
protected |
Definition at line 56 of file memory_model_tso.cpp.
◆ program_order_is_relaxed()
|
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
