cprover
Loading...
Searching...
No Matches
event_grapht::graph_explorert Class Reference

#include <event_graph.h>

Inheritance diagram for event_grapht::graph_explorert:
Collaboration diagram for event_grapht::graph_explorert:

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.
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
void collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
 Tarjan 1972 adapted and modified for events.

Public Attributes

std::map< event_idt, bool > mark
std::stack< event_idt > marked_stack
std::stack< event_idt > point_stack
std::set< event_idt > skip_tracked

Protected Member Functions

virtual bool filtering (event_idt)
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

Protected Attributes

event_grapht & egraph
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_idt > thin_air_events

Detailed Description

Definition at line 249 of file event_graph.h.

Constructor & Destructor Documentation

◆ ~graph_explorert()

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

Definition at line 252 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 293 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 lwsync_met,
bool has_to_be_unsafe,
irep_idt var_to_avoid,
memory_modelt model )

see event_grapht::collect_cycles

Definition at line 159 of file cycle_collection.cpp.

◆ collect_cycles()

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

Tarjan 1972 adapted and modified for events.

Definition at line 51 of file cycle_collection.cpp.

◆ 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 119 of file cycle_collection.cpp.

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

◆ filtering()

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

Reimplemented in event_grapht::graph_conc_explorert.

Definition at line 269 of file event_graph.h.

◆ order_filtering()

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

Definition at line 274 of file event_graph.h.

Member Data Documentation

◆ cycle_nb

unsigned event_grapht::graph_explorert::cycle_nb
protected

Definition at line 281 of file event_graph.h.

◆ egraph

event_grapht& event_grapht::graph_explorert::egraph
protected

Definition at line 257 of file event_graph.h.

◆ events_per_thread

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

Definition at line 266 of file event_graph.h.

◆ mark

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

Definition at line 305 of file event_graph.h.

◆ marked_stack

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

Definition at line 306 of file event_graph.h.

◆ max_po_trans

unsigned event_grapht::graph_explorert::max_po_trans
protected

Definition at line 261 of file event_graph.h.

◆ max_var

unsigned event_grapht::graph_explorert::max_var
protected

Definition at line 260 of file event_graph.h.

◆ point_stack

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

Definition at line 307 of file event_graph.h.

◆ reads_per_variable

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

Definition at line 265 of file event_graph.h.

◆ skip_tracked

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

Definition at line 309 of file event_graph.h.

◆ thin_air_events

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

Definition at line 286 of file event_graph.h.

◆ writes_per_variable

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

Definition at line 264 of file event_graph.h.

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