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.

virtual exprt before (event_it e1, event_it e2)=0

Static Protected Member Functions

static irep_idt id (event_it event)

Produce the symbol ID for an event.

Protected Attributes

const namespacet & ns

address_mapt address_map

numberingt numbering

typet clock_type

Detailed Description

Base class for implementing memory models via additional constraints for SSA equations.

Provides methods for encoding ordering of shared read/write events.

Definition at line 20 of file partial_order_concurrency.h.

Member Typedef Documentation

◆ address_mapt

typedef std::map<irep_idt, a_rect> partial_order_concurrencyt::address_mapt

protected

Definition at line 58 of file partial_order_concurrency.h.

◆ event_it

typedef eventst::const_iterator partial_order_concurrencyt::event_it

Definition at line 28 of file partial_order_concurrency.h.

◆ event_listt

typedef std::vector<event_it> partial_order_concurrencyt::event_listt

protected

Definition at line 50 of file partial_order_concurrency.h.

◆ eventst

typedef symex_target_equationt::SSA_stepst partial_order_concurrencyt::eventst

Definition at line 27 of file partial_order_concurrency.h.

◆ eventt

typedef SSA_stept partial_order_concurrencyt::eventt

Definition at line 26 of file partial_order_concurrency.h.

◆ numberingt

typedef std::map<event_it, unsigned> partial_order_concurrencyt::numberingt

protected

Definition at line 80 of file partial_order_concurrency.h.

Member Enumeration Documentation

◆ axiomt

enum partial_order_concurrencyt::axiomt

Enumerator
AX_SC_PER_LOCATION
AX_NO_THINAIR
AX_OBSERVATION
AX_PROPAGATION

Definition at line 31 of file partial_order_concurrency.h.

Constructor & Destructor Documentation

◆ partial_order_concurrencyt()

partial_order_concurrencyt::partial_order_concurrencyt ( const namespacet & _ns )

explicit

Definition at line 18 of file partial_order_concurrency.cpp.

◆ ~partial_order_concurrencyt()

partial_order_concurrencyt::~partial_order_concurrencyt ( )

virtual

Definition at line 23 of file partial_order_concurrency.cpp.

Member Function Documentation

◆ add_constraint()

void partial_order_concurrencyt::add_constraint ( symex_target_equationt & equation,

const exprt & cond,

const std::string & msg,

const symex_targett::sourcet & source

) const

protected

Simplify and add a constraint to equation.

Parameters: equation target equation to be constrained with the cond

cond condition expressing the constraint

msg message for the constraint

source the location of the constraint

Definition at line 200 of file partial_order_concurrency.cpp.

◆ add_init_writes()

void partial_order_concurrencyt::add_init_writes ( symex_target_equationt & equation )

protected

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.

Parameters: equation the target equation to be modified

Definition at line 27 of file partial_order_concurrency.cpp.

◆ address()

irep_idt partial_order_concurrencyt::address ( event_it event ) const

inlineprotected

Produce an address ID for an event.

Parameters: event SSA step for the event

Returns: L1-renamed identifier

Definition at line 94 of file partial_order_concurrency.h.

◆ before() [1/2]

virtual exprt partial_order_concurrencyt::before ( event_it e1,

event_it e2

)

protectedpure virtual

Implemented in memory_model_sct, and memory_model_tsot.

◆ before() [2/2]

exprt partial_order_concurrencyt::before ( event_it e1,

event_it e2,

unsigned axioms

)

protected

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.

Parameters: e1 preceding event

e2 succeeding event

axioms clocks to be included in the resulting constraint

Returns: conjunction of constraints (one of each clock)

Definition at line 166 of file partial_order_concurrency.cpp.

◆ build_clock_type()

void partial_order_concurrencyt::build_clock_type ( )

protected

Initialize the clock_type so that it can be used to number events.

Definition at line 158 of file partial_order_concurrency.cpp.

◆ build_event_lists()

void partial_order_concurrencyt::build_event_lists ( symex_target_equationt & equation,

message_handlert & message_handler

)

protected

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)