cprover
event_grapht::graph_explorert Class Reference

#include <event_graph.h>

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

Public Member Functions

virtual ~graph_explorert ()
 
 graph_explorert (event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)
 
critical_cyclet extract_cycle (event_idt vertex, event_idt source, unsigned number_of_cycles)
 extracts a (whole, unreduced) cycle from the stack. More...
 
bool backtrack (std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwsync_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model)
 see event_grapht::collect_cycles More...
 
void collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
 Tarjan 1972 adapted and modified for events. More...
 

Public Attributes

std::map< event_idt, bool > mark
 
std::stack< event_idtmarked_stack
 
std::stack< event_idtpoint_stack
 
std::set< event_idtskip_tracked
 

Protected Member Functions

virtual bool filtering (event_idt u)
 
virtual std::list< event_idt > * order_filtering (std::list< event_idt > *order)
 
void filter_thin_air (std::set< critical_cyclet > &set_of_cycles)
 after the collection, eliminates the executions forbidden by an indirect thin-air More...
 

Protected Attributes

event_graphtegraph
 
unsigned max_var
 
unsigned max_po_trans
 
std::map< irep_idt, unsigned char > writes_per_variable
 
std::map< irep_idt, unsigned char > reads_per_variable
 
std::map< unsigned, unsigned char > events_per_thread
 
unsigned cycle_nb
 
std::set< event_idtthin_air_events
 

Detailed Description

Definition at line 214 of file event_graph.h.

Constructor & Destructor Documentation

§ ~graph_explorert()

virtual event_grapht::graph_explorert::~graph_explorert ( )
inlinevirtual

Definition at line 217 of file event_graph.h.

§ graph_explorert()

event_grapht::graph_explorert::graph_explorert ( event_grapht _egraph,
unsigned  _max_var,
unsigned  _max_po_trans 
)
inline

Definition at line 258 of file event_graph.h.

Member Function Documentation

§ backtrack()

bool event_grapht::graph_explorert::backtrack ( std::set< critical_cyclet > &  set_of_cycles,
event_idt  source,
event_idt  vertex,
bool  unsafe_met,
event_idt  po_trans,
bool  same_var_pair,
bool  lwfence_met,
bool  has_to_be_unsafe,
irep_idt  var_to_avoid,
memory_modelt  model 
)

§ collect_cycles()

void event_grapht::graph_explorert::collect_cycles ( std::set< critical_cyclet > &  set_of_cycles,
memory_modelt  model 
)

§ extract_cycle()

event_grapht::critical_cyclet event_grapht::graph_explorert::extract_cycle ( event_idt  vertex,
event_idt  source,
unsigned  number 
)

extracts a (whole, unreduced) cycle from the stack.

Note: it may not be a real cycle yet – we cannot check the size before a call to this function.

Definition at line 110 of file cycle_collection.cpp.

References messaget::debug(), egraph, messaget::eom(), event_grapht::critical_cyclet::has_user_defined_fence, event_grapht::message, point_stack, and stack.

Referenced by backtrack().

§ filter_thin_air()

void event_grapht::graph_explorert::filter_thin_air ( std::set< critical_cyclet > &  set_of_cycles)
protected

after the collection, eliminates the executions forbidden by an indirect thin-air

Definition at line 20 of file cycle_collection.cpp.

References messaget::debug(), egraph, messaget::eom(), event_grapht::message, and thin_air_events.

Referenced by collect_cycles().

§ filtering()

virtual bool event_grapht::graph_explorert::filtering ( event_idt  u)
inlineprotectedvirtual

Definition at line 234 of file event_graph.h.

Referenced by backtrack().

§ order_filtering()

virtual std::list<event_idt>* event_grapht::graph_explorert::order_filtering ( std::list< event_idt > *  order)
inlineprotectedvirtual

Definition at line 239 of file event_graph.h.

Referenced by collect_cycles().

Member Data Documentation

§ cycle_nb

unsigned event_grapht::graph_explorert::cycle_nb
protected

Definition at line 246 of file event_graph.h.

Referenced by backtrack().

§ egraph

§ events_per_thread

std::map<unsigned, unsigned char> event_grapht::graph_explorert::events_per_thread
protected

Definition at line 231 of file event_graph.h.

Referenced by backtrack().

§ mark

std::map<event_idt, bool> event_grapht::graph_explorert::mark

Definition at line 270 of file event_graph.h.

Referenced by backtrack(), and collect_cycles().

§ marked_stack

std::stack<event_idt> event_grapht::graph_explorert::marked_stack

Definition at line 271 of file event_graph.h.

Referenced by backtrack(), and collect_cycles().

§ max_po_trans

unsigned event_grapht::graph_explorert::max_po_trans
protected

Definition at line 226 of file event_graph.h.

Referenced by collect_cycles().

§ max_var

unsigned event_grapht::graph_explorert::max_var
protected

Definition at line 225 of file event_graph.h.

Referenced by backtrack().

§ point_stack

std::stack<event_idt> event_grapht::graph_explorert::point_stack

Definition at line 272 of file event_graph.h.

Referenced by backtrack(), and extract_cycle().

§ reads_per_variable

std::map<irep_idt, unsigned char> event_grapht::graph_explorert::reads_per_variable
protected

Definition at line 230 of file event_graph.h.

Referenced by backtrack().

§ skip_tracked

std::set<event_idt> event_grapht::graph_explorert::skip_tracked

Definition at line 274 of file event_graph.h.

Referenced by backtrack().

§ thin_air_events

std::set<event_idt> event_grapht::graph_explorert::thin_air_events
protected

Definition at line 251 of file event_graph.h.

Referenced by backtrack(), and filter_thin_air().

§ writes_per_variable

std::map<irep_idt, unsigned char> event_grapht::graph_explorert::writes_per_variable
protected

Definition at line 229 of file event_graph.h.

Referenced by backtrack().


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