cprover
event_grapht::critical_cyclet Class Reference

#include <event_graph.h>

Inheritance diagram for event_grapht::critical_cyclet:
[legend]
Collaboration diagram for event_grapht::critical_cyclet:
[legend]

Classes

struct  delayt
 

Public Member Functions

 critical_cyclet (event_grapht &_egraph, unsigned _id)
 
void operator() (const critical_cyclet &cyc)
 
bool is_cycle ()
 
void hide_internals (critical_cyclet &reduced) const
 
bool is_unsafe (memory_modelt model, bool fast=false)
 checks whether there is at least one pair which is unsafe (takes fences and dependencies into account), and adds the unsafe pairs in the set More...
 
bool is_unsafe_fast (memory_modelt model)
 
void compute_unsafe_pairs (memory_modelt model)
 
bool is_unsafe_asm (memory_modelt model, bool fast=false)
 same as is_unsafe, but with ASM fences More...
 
bool is_not_uniproc (memory_modelt model) const
 
bool is_not_thin_air () const
 
std::string print () const
 
std::string print_events () const
 
std::string print_name (memory_modelt model) const
 
std::string print_name (memory_modelt model, bool hide_internals) const
 
std::string print_unsafes () const
 
std::string print_output () const
 
std::string print_all (memory_modelt model, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, bool hide_internals) const
 
void print_dot (std::ostream &str, unsigned colour, memory_modelt model) const
 
bool operator< (const critical_cyclet &other) const
 

Public Attributes

unsigned id
 
bool has_user_defined_fence
 
std::set< delaytunsafe_pairs
 

Protected Member Functions

bool is_not_uniproc () const
 
bool is_not_weak_uniproc () const
 
std::string print_detail (const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, memory_modelt model) const
 
std::string print_name (const critical_cyclet &redyced, memory_modelt model) const
 
bool check_AC (const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const
 
bool check_BC (const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const
 

Protected Attributes

event_graphtegraph
 

Detailed Description

Definition at line 38 of file event_graph.h.

Constructor & Destructor Documentation

§ critical_cyclet()

event_grapht::critical_cyclet::critical_cyclet ( event_grapht _egraph,
unsigned  _id 
)
inline

Definition at line 63 of file event_graph.h.

Member Function Documentation

§ check_AC()

bool event_grapht::critical_cyclet::check_AC ( const_iterator  s_it,
const abstract_eventt first,
const abstract_eventt second 
) const
protected

§ check_BC()

bool event_grapht::critical_cyclet::check_BC ( const_iterator  it,
const abstract_eventt first,
const abstract_eventt second 
) const
protected

§ compute_unsafe_pairs()

void event_grapht::critical_cyclet::compute_unsafe_pairs ( memory_modelt  model)
inline

Definition at line 110 of file event_graph.h.

References is_unsafe(), and is_unsafe_asm().

§ hide_internals()

void event_grapht::critical_cyclet::hide_internals ( critical_cyclet reduced) const

§ is_cycle()

bool event_grapht::critical_cyclet::is_cycle ( )
inline

§ is_not_thin_air()

bool event_grapht::critical_cyclet::is_not_thin_air ( ) const

§ is_not_uniproc() [1/2]

bool event_grapht::critical_cyclet::is_not_uniproc ( ) const
protected

§ is_not_uniproc() [2/2]

bool event_grapht::critical_cyclet::is_not_uniproc ( memory_modelt  model) const
inline

Definition at line 117 of file event_graph.h.

References is_not_thin_air(), is_not_uniproc(), is_not_weak_uniproc(), and RMO.

§ is_not_weak_uniproc()

bool event_grapht::critical_cyclet::is_not_weak_uniproc ( ) const
protected

§ is_unsafe()

bool event_grapht::critical_cyclet::is_unsafe ( memory_modelt  model,
bool  fast = false 
)

checks whether there is at least one pair which is unsafe (takes fences and dependencies into account), and adds the unsafe pairs in the set

Definition at line 280 of file event_graph.cpp.

References data_dpt::dp(), messaget::eom(), abstract_eventt::Fence, abstract_eventt::Lwfence, abstract_eventt::operation, Power, event_grapht::size(), abstract_eventt::thread, abstract_eventt::unsafe_pair(), abstract_eventt::unsafe_pair_lwfence(), and abstract_eventt::variable.

Referenced by event_grapht::graph_explorert::backtrack(), compute_unsafe_pairs(), is_cycle(), and is_unsafe_fast().

§ is_unsafe_asm()

bool event_grapht::critical_cyclet::is_unsafe_asm ( memory_modelt  model,
bool  fast = false 
)

§ is_unsafe_fast()

bool event_grapht::critical_cyclet::is_unsafe_fast ( memory_modelt  model)
inline

Definition at line 105 of file event_graph.h.

References is_unsafe().

§ operator()()

void event_grapht::critical_cyclet::operator() ( const critical_cyclet cyc)
inline

Definition at line 68 of file event_graph.h.

References event_grapht::clear(), and has_user_defined_fence.

§ operator<()

bool event_grapht::critical_cyclet::operator< ( const critical_cyclet other) const
inline

Definition at line 197 of file event_graph.h.

§ print()

std::string event_grapht::critical_cyclet::print ( ) const

Definition at line 1018 of file event_graph.cpp.

§ print_all()

std::string event_grapht::critical_cyclet::print_all ( memory_modelt  model,
std::map< std::string, std::string > &  map_id2var,
std::map< std::string, std::string > &  map_var2id,
bool  hide_internals 
) const

Definition at line 1127 of file event_graph.cpp.

References event_grapht::size().

Referenced by print_name().

§ print_detail()

std::string event_grapht::critical_cyclet::print_detail ( const critical_cyclet reduced,
std::map< std::string, std::string > &  map_id2var,
std::map< std::string, std::string > &  map_var2id,
memory_modelt  model 
) const
protected

§ print_dot()

void event_grapht::critical_cyclet::print_dot ( std::ostream &  str,
unsigned  colour,
memory_modelt  model 
) const

§ print_events()

std::string event_grapht::critical_cyclet::print_events ( ) const

§ print_name() [1/3]

§ print_name() [2/3]

std::string event_grapht::critical_cyclet::print_name ( memory_modelt  model) const
inline

Definition at line 170 of file event_graph.h.

References print_name().

§ print_name() [3/3]

std::string event_grapht::critical_cyclet::print_name ( memory_modelt  model,
bool  hide_internals 
) const
inline

§ print_output()

std::string event_grapht::critical_cyclet::print_output ( ) const

§ print_unsafes()

std::string event_grapht::critical_cyclet::print_unsafes ( ) const

Member Data Documentation

§ egraph

event_grapht& event_grapht::critical_cyclet::egraph
protected

Definition at line 41 of file event_graph.h.

§ has_user_defined_fence

bool event_grapht::critical_cyclet::has_user_defined_fence

§ id

unsigned event_grapht::critical_cyclet::id

Definition at line 59 of file event_graph.h.

§ unsafe_pairs


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