Interface to memconsistency::cats data structures. More...

#include <cats.hpp>

Public Member Functions
	EvtStateCats (mc::cats::ExecWitness ew, mc::cats::Architecture arch)

void	Reset ()

bool	Exhausted () const

template<std::size_t max_size_bytes, class Func >
EventPtrs< max_size_bytes >	MakeEvent (types::Pid pid, mc::Event::Type type, std::size_t size, Func mkevt)

mc::Event	MakeOther (types::Pid pid, mc::Event::Type type, types::Addr addr)

template<std::size_t max_size_bytes = sizeof(types::WriteID)>
EventPtrs< max_size_bytes >	MakeRead (types::Pid pid, mc::Event::Type type, types::Addr addr, std::size_t size=max_size_bytes)

template<std::size_t max_size_bytes = sizeof(types::WriteID)>
EventPtrs< max_size_bytes >	MakeWrite (types::Pid pid, mc::Event::Type type, types::Addr addr, types::WriteID *data, std::size_t size=max_size_bytes)

template<std::size_t max_size_bytes = sizeof(types::WriteID)>
EventPtrs< max_size_bytes >	GetWrite (const EventPtrs< max_size_bytes > &after, types::Addr addr, const types::WriteID *from_id, std::size_t size=max_size_bytes)

mc::cats::ExecWitness *	ew ()

const mc::cats::ExecWitness *	ew () const

mc::cats::Architecture *	arch ()

const mc::cats::Architecture *	arch () const

void	set_addr_mask (types::Addr val)

types::Addr	addr_mask () const

Static Public Attributes
static constexpr std::size_t	kMaxOpSize = sizeof(types::WriteID) * 2

static constexpr std::size_t	kMaxOpEvents

static constexpr types::Poi	kMinOther

static constexpr types::Poi	kMaxOther

static constexpr types::WriteID	kInitWrite

static constexpr types::WriteID	kMinWrite = kInitWrite + 1

static constexpr types::WriteID	kMaxWrite

Private Types
typedef std::unordered_map< types::WriteID, const mc::Event * >	WriteID_EventPtr

Private Attributes
mc::cats::ExecWitness *	ew_

mc::cats::Architecture *	arch_

WriteID_EventPtr	writes_

types::WriteID	last_write_id_

types::Poi	last_other_id

types::Addr	addr_mask_

Detailed Description

Interface to memconsistency::cats data structures.

This class serves as a helper to interface with data structures in memconsistency::cats. Its primary function is the creation of new events by Operations.

Furthermore, as this is the interface to the consistency model descriptions and checker, we can encode efficient support for virtual address synonyms here by transforming the address used to construct events (see EvtStateCats::set_addr_mask). As described in [1], if we are working at the virtual address level, we are checking VAMC (Virtual Address Memory Consistency). Here we only consider the problem of synonym sets of virtual addresses mapping to the same physical address, and add simple support for it.

[1] Bogdan F. Romanescu, Alvin R. Lebeck, Daniel J. Sorin, "Specifying and dynamically verifying address translation-aware memory consistency", 2010.

Member Typedef Documentation

§ WriteID_EventPtr

typedef std::unordered_map<types::WriteID, const mc::Event *> mc2lib::codegen::EvtStateCats::WriteID_EventPtr

private

Constructor & Destructor Documentation

§ EvtStateCats()

mc2lib::codegen::EvtStateCats::EvtStateCats	(	mc::cats::ExecWitness *	ew,
		mc::cats::Architecture *	arch
	)

inlineexplicit

Member Function Documentation

§ addr_mask()

types::Addr mc2lib::codegen::EvtStateCats::addr_mask ( ) const

inline

§ arch() [1/2]

mc::cats::Architecture* mc2lib::codegen::EvtStateCats::arch ( )

inline

§ arch() [2/2]

const mc::cats::Architecture* mc2lib::codegen::EvtStateCats::arch ( ) const

inline

§ ew() [1/2]

mc::cats::ExecWitness* mc2lib::codegen::EvtStateCats::ew ( )

inline

§ ew() [2/2]

const mc::cats::ExecWitness* mc2lib::codegen::EvtStateCats::ew ( ) const

inline

§ Exhausted()

bool mc2lib::codegen::EvtStateCats::Exhausted ( ) const

inline

§ GetWrite()

template<std::size_t max_size_bytes = sizeof(types::WriteID)>

EventPtrs<max_size_bytes> mc2lib::codegen::EvtStateCats::GetWrite	(	const EventPtrs< max_size_bytes > &	after,
		types::Addr	addr,
		const types::WriteID *	from_id,
		std::size_t	size = `max_size_bytes`
	)

inline

§ MakeEvent()

template<std::size_t max_size_bytes, class Func >

EventPtrs<max_size_bytes> mc2lib::codegen::EvtStateCats::MakeEvent	(	types::Pid	pid,
		mc::Event::Type	type,
		std::size_t	size,
		Func	mkevt
	)

inline

§ MakeOther()

mc::Event mc2lib::codegen::EvtStateCats::MakeOther	(	types::Pid	pid,
		mc::Event::Type	type,
		types::Addr	addr
	)

inline

§ MakeRead()

template<std::size_t max_size_bytes = sizeof(types::WriteID)>

EventPtrs<max_size_bytes> mc2lib::codegen::EvtStateCats::MakeRead	(	types::Pid	pid,
		mc::Event::Type	type,
		types::Addr	addr,
		std::size_t	size = `max_size_bytes`
	)

inline

§ MakeWrite()

template<std::size_t max_size_bytes = sizeof(types::WriteID)>

EventPtrs<max_size_bytes> mc2lib::codegen::EvtStateCats::MakeWrite	(	types::Pid	pid,
		mc::Event::Type	type,
		types::Addr	addr,
		types::WriteID *	data,
		std::size_t	size = `max_size_bytes`
	)

inline

§ Reset()

void mc2lib::codegen::EvtStateCats::Reset ( )

inline

§ set_addr_mask()

void mc2lib::codegen::EvtStateCats::set_addr_mask ( types::Addr val )

inline

When using virtual addresses, this can be used to mask test memory addresses, s.t. synonyms map to the same address used by the checker. Although we could modify the checker to permit sets of addresses, this would be much more expensive in terms of storage and hash-map lookup by the checker. Assumes that synonym range start addresses are multiples of 2**n (the size of memory).

Member Data Documentation

§ addr_mask_

types::Addr mc2lib::codegen::EvtStateCats::addr_mask_

private

§ arch_

mc::cats::Architecture* mc2lib::codegen::EvtStateCats::arch_

private

§ ew_

mc::cats::ExecWitness* mc2lib::codegen::EvtStateCats::ew_

private

§ kInitWrite

constexpr types::WriteID mc2lib::codegen::EvtStateCats::kInitWrite

static

Initial value:

=

std::numeric_limits<types::WriteID>::min()

§ kMaxOpEvents

constexpr std::size_t mc2lib::codegen::EvtStateCats::kMaxOpEvents

static

Initial value:

=

kMaxOpSize / sizeof(types::WriteID)

§ kMaxOpSize

constexpr std::size_t mc2lib::codegen::EvtStateCats::kMaxOpSize = sizeof(types::WriteID) * 2

static

§ kMaxOther

constexpr types::Poi mc2lib::codegen::EvtStateCats::kMaxOther

static

Initial value:

=

std::numeric_limits<types::Poi>::max() - (kMaxOpEvents - 1)

§ kMaxWrite

constexpr types::WriteID mc2lib::codegen::EvtStateCats::kMaxWrite

static

Initial value:

=
      (lt__(std::numeric_limits<types::WriteID>::max(), kMinOther)
           ? std::numeric_limits<types::WriteID>::max()
           : kMinOther - 1) -
      (kMaxOpEvents - 1)

§ kMinOther

constexpr types::Poi mc2lib::codegen::EvtStateCats::kMinOther

static

Initial value:

= static_cast<types::Poi>(1)

<< (sizeof(types::Poi) * 8 - 1)

§ kMinWrite

constexpr types::WriteID mc2lib::codegen::EvtStateCats::kMinWrite = kInitWrite + 1

static

§ last_other_id

types::Poi mc2lib::codegen::EvtStateCats::last_other_id

private

§ last_write_id_

types::WriteID mc2lib::codegen::EvtStateCats::last_write_id_

private

§ writes_

WriteID_EventPtr mc2lib::codegen::EvtStateCats::writes_

private

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

include/mc2lib/codegen/cats.hpp

Public Member Functions

Static Public Attributes

Private Types

Private Attributes

Detailed Description

Member Typedef Documentation

§ WriteID_EventPtr

Constructor & Destructor Documentation

§ EvtStateCats()

Member Function Documentation

§ addr_mask()

§ arch() [1/2]

§ arch() [2/2]

§ ew() [1/2]

§ ew() [2/2]

§ Exhausted()

§ GetWrite()

§ MakeEvent()

§ MakeOther()

§ MakeRead()

§ MakeWrite()

§ Reset()

§ set_addr_mask()

Member Data Documentation

§ addr_mask_

§ arch_

§ ew_

§ kInitWrite

§ kMaxOpEvents

§ kMaxOpSize

§ kMaxOther

§ kMaxWrite

§ kMinOther

§ kMinWrite

§ last_other_id

§ last_write_id_

§ writes_