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

#include <partial_order_concurrency.h>

Inheritance diagram for partial_order_concurrencyt:

Collaboration diagram for partial_order_concurrencyt:

Classes
struct	a_rect

Public Types
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

Public Member Functions
	partial_order_concurrencyt (const namespacet &_ns)

virtual	~partial_order_concurrencyt ()

Static Public Member Functions
static irep_idt	rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION)
	Build identifier for the read/write clock variable. More...

Protected Types
typedef std::vector< event_it >	event_listt

typedef std::map< irep_idt, a_rect >	address_mapt

typedef std::map< event_it, unsigned >	numberingt

Protected Member Functions
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...

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. More...

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 202 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_tsot, and memory_model_sct.

◆ 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 168 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 160 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)

Parameters

equation	the target equation (containing the events to be processed)
message_handler	message handler to output statistics

Definition at line 74 of file partial_order_concurrency.cpp.

◆ clock()

symbol_exprt partial_order_concurrencyt::clock	(	event_it	e,
		axiomt	axiom
	)

protected

Produce a clock symbol for some event.

Parameters

e	event is either shared read/write or spawn
axiom	clock variable

Returns: symbol of type clock_type with id from rw_clock_id

Definition at line 137 of file partial_order_concurrency.cpp.

◆ id()

static irep_idt partial_order_concurrencyt::id ( event_it event )

inlinestaticprotected

Produce the symbol ID for an event.

Parameters

event SSA step for the event

Returns: identifier

Definition at line 86 of file partial_order_concurrency.h.

◆ rw_clock_id()

irep_idt partial_order_concurrencyt::rw_clock_id	(	event_it	e,
		axiomt	axiom = `AX_PROPAGATION`
	)

static

Build identifier for the read/write clock variable.

Parameters

e	either shared read or shared write event
axiom	the clock variable to be used (as part of the identifier)

Returns: identifier representing the clock variable of the event

Definition at line 125 of file partial_order_concurrency.cpp.

Member Data Documentation

◆ address_map

address_mapt partial_order_concurrencyt::address_map

protected

Definition at line 59 of file partial_order_concurrency.h.

◆ clock_type

typet partial_order_concurrencyt::clock_type

protected

Definition at line 99 of file partial_order_concurrency.h.

◆ ns

const namespacet& partial_order_concurrencyt::ns

protected

Definition at line 48 of file partial_order_concurrency.h.

◆ numbering

numberingt partial_order_concurrencyt::numbering

protected

Definition at line 81 of file partial_order_concurrency.h.

The documentation for this class was generated from the following files:

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

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ address_mapt

◆ event_it

◆ event_listt

◆ eventst

◆ eventt

◆ numberingt

Member Enumeration Documentation

◆ axiomt

Constructor & Destructor Documentation

◆ partial_order_concurrencyt()

◆ ~partial_order_concurrencyt()

Member Function Documentation

◆ add_constraint()

◆ add_init_writes()

◆ address()

◆ before() [1/2]

◆ before() [2/2]

◆ build_clock_type()

◆ build_event_lists()

◆ clock()

◆ id()

◆ rw_clock_id()

Member Data Documentation

◆ address_map

◆ clock_type

◆ ns

◆ numbering