cprover
|
#include <event_graph.h>
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_idt > | marked_stack |
std::stack< event_idt > | point_stack |
std::set< event_idt > | skip_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_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 |
Definition at line 214 of file event_graph.h.
|
inlinevirtual |
Definition at line 217 of file event_graph.h.
|
inline |
Definition at line 258 of file event_graph.h.
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 | ||
) |
see event_grapht::collect_cycles
get_po_only | used for po-transitivity |
Definition at line 151 of file cycle_collection.cpp.
References event_grapht::are_po_ordered(), abstract_eventt::ASMfence, event_grapht::com_out(), cycle_nb, messaget::debug(), egraph, messaget::eom(), events_per_thread, extract_cycle(), abstract_eventt::Fence, event_grapht::filter_thin_air, event_grapht::filter_uniproc, filtering(), event_grapht::critical_cyclet::hide_internals(), id2string(), event_grapht::ignore_arrays, event_grapht::critical_cyclet::is_cycle(), is_lwfence(), event_grapht::critical_cyclet::is_not_thin_air(), event_grapht::critical_cyclet::is_not_uniproc(), event_grapht::critical_cyclet::is_unsafe(), abstract_eventt::local, abstract_eventt::Lwfence, event_grapht::map_data_dp, mark, marked_stack, max_var, event_grapht::message, abstract_eventt::operation, event_grapht::po_out(), point_stack, event_grapht::critical_cyclet::print_name(), abstract_eventt::Read, reads_per_variable, event_grapht::remove_com_edge(), skip_tracked, thin_air_events, abstract_eventt::thread, abstract_eventt::unsafe_pair(), abstract_eventt::variable, abstract_eventt::WRfence, abstract_eventt::Write, and writes_per_variable.
Referenced by 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.
References backtrack(), messaget::debug(), egraph, messaget::eom(), filter_thin_air(), event_grapht::filter_thin_air, mark, marked_stack, max_po_trans, event_grapht::message, order_filtering(), event_grapht::po_order, event_grapht::poUrfe_order, Power, PSO, RMO, event_grapht::size(), TSO, and Unknown.
Referenced by event_grapht::collect_cycles().
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().
|
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().
|
inlineprotectedvirtual |
Definition at line 234 of file event_graph.h.
Referenced by backtrack().
|
inlineprotectedvirtual |
Definition at line 239 of file event_graph.h.
Referenced by collect_cycles().
|
protected |
Definition at line 246 of file event_graph.h.
Referenced by backtrack().
|
protected |
Definition at line 222 of file event_graph.h.
Referenced by backtrack(), collect_cycles(), event_grapht::graph_pensieve_explorert::collect_pairs(), extract_cycle(), filter_thin_air(), and event_grapht::graph_pensieve_explorert::find_second_event().
|
protected |
Definition at line 231 of file event_graph.h.
Referenced by backtrack().
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().
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().
|
protected |
Definition at line 226 of file event_graph.h.
Referenced by collect_cycles().
|
protected |
Definition at line 225 of file event_graph.h.
Referenced by backtrack().
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().
|
protected |
Definition at line 230 of file event_graph.h.
Referenced by backtrack().
std::set<event_idt> event_grapht::graph_explorert::skip_tracked |
Definition at line 274 of file event_graph.h.
Referenced by backtrack().
|
protected |
Definition at line 251 of file event_graph.h.
Referenced by backtrack(), and filter_thin_air().
|
protected |
Definition at line 229 of file event_graph.h.
Referenced by backtrack().