#include <memory_model_pso.h>
+ Inheritance diagram for memory_model_psot:
+ Collaboration diagram for memory_model_psot:
Protected Member Functions
In-thread program order.
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.
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].
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)
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.
Produce an address ID for an event.
Produce a clock symbol for some event.
Initialize the clock_type so that it can be used to number events.
Simplify and add a constraint to equation.
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
Build identifier for the read/write clock variable.
Produce the symbol ID for an event.
Detailed Description
Constructor & Destructor Documentation
◆ memory_model_psot()
Member Function Documentation
◆ operator()()
◆ program_order_is_relaxed()
The documentation for this class was generated from the following files:
