14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H 15 #define CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H 47 std::map<std::string, std::string> &map_id2var,
48 std::map<std::string, std::string> &map_var2id,
71 for(const_iterator it=cyc.begin(); it!=cyc.end(); it++)
83 const_iterator it=begin();
84 const_iterator n_it=it;
86 for(; it!=end() && n_it!=end(); ++it, ++n_it)
166 std::string
print()
const;
180 assert(!reduced.empty());
190 std::map<std::string, std::string> &map_id2var,
191 std::map<std::string, std::string> &map_var2id,
199 return ( ((std::list<event_idt>) *
this) < (std::list<event_idt>)other);
240 std::list<event_idt>* order)
261 unsigned _max_po_trans):
270 std::map<event_idt, bool>
mark;
277 event_idt source,
unsigned number_of_cycles);
279 bool backtrack(std::set<critical_cyclet> &set_of_cycles,
286 bool has_to_be_unsafe,
292 std::set<critical_cyclet> &set_of_cycles,
304 unsigned _max_po_trans,
const std::set<event_idt> &_filter)
316 static std::list<event_idt> new_order;
319 for(
const auto &evt : *order)
321 new_order.push_back(evt);
338 unsigned _max_po_trans)
365 std::set<std::pair<event_idt, event_idt> >
loops;
371 assert(po_no == com_no);
418 assert(
operator[](a).thread==
operator[](b).thread);
427 assert(
operator[](a).thread==
operator[](b).thread);
431 loops.insert(std::pair<event_idt, event_idt>(a, b));
432 loops.insert(std::pair<event_idt, event_idt>(b, a));
472 std::set<std::pair<const abstract_eventt&, const abstract_eventt&>>
483 if(
operator[](a).thread!=
operator[](b).thread)
487 if(
loops.find(std::pair<event_idt, event_idt>(a, b))!=
loops.end() )
510 std::set<event_idt> &visited);
515 const std::set<event_idt> &filter)
530 unsigned _max_po_trans=0,
531 bool _ignore_arrays=
false)
553 #endif // CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H std::list< event_idt > po_order
std::list< event_idt > * initial_filtering(std::list< event_idt > *order)
void remove_po_edge(event_idt a, event_idt b)
grapht< abstract_eventt >::nodet & operator[](event_idt n)
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
Tarjan 1972 adapted and modified for events.
bool operator==(const delayt &other) const
std::string print_name(const critical_cyclet &redyced, memory_modelt model) const
std::stack< event_idt > marked_stack
void collect_pairs(namespacet &ns)
void filter_thin_air(std::set< critical_cyclet > &set_of_cycles)
after the collection, eliminates the executions forbidden by an indirect thin-air ...
std::map< event_idt, bool > mark
bool is_not_thin_air() const
std::string print_name(memory_modelt model, bool hide_internals) const
void print_dot(std::ostream &str, unsigned colour, memory_modelt model) const
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
bool check_BC(const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const
bool is_not_uniproc() const
bool has_po_edge(event_idt i, event_idt j) const
void remove_com_edge(event_idt a, event_idt b)
std::map< irep_idt, unsigned char > writes_per_variable
void hide_internals(critical_cyclet &reduced) const
void add_po_edge(event_idt a, event_idt b)
bool operator<(const delayt &other) const
bool has_edge(node_indext i, node_indext j) const
bool is_unsafe_asm(memory_modelt model, bool fast=false)
same as is_unsafe, but with ASM fences
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 compute_unsafe_pairs(memory_modelt model)
const wmm_grapht::edgest & po_out(event_idt n) const
std::map< irep_idt, unsigned char > reads_per_variable
std::map< unsigned, unsigned char > events_per_thread
std::string print_output() const
void operator()(const critical_cyclet &cyc)
graph_pensieve_explorert(event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)
bool filtering(event_idt u)
const edgest & out(node_indext n) const
const wmm_grapht::edgest & po_in(event_idt n) const
critical_cyclet(event_grapht &_egraph, unsigned _id)
event_idt copy_segment(event_idt begin, event_idt end)
grapht< abstract_eventt > wmm_grapht
void add_po_back_edge(event_idt a, event_idt b)
bool is_unsafe_fast(memory_modelt model)
nodet::node_indext node_indext
void add_undirected_com_edge(event_idt a, event_idt b)
const wmm_grapht::edgest & com_out(event_idt n) const
bool operator<(const critical_cyclet &other) const
bool are_po_ordered(event_idt a, event_idt b)
wmm_grapht::node_indext event_idt
bool has_com_edge(event_idt i, event_idt j) const
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_pairs_naive(namespacet &ns)
bool check_AC(const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const
graph_explorert(event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)
delayt(event_idt _first, event_idt _second, bool _is_po)
std::list< event_idt > poUrfe_order
virtual ~graph_explorert()
std::set< delayt > unsafe_pairs
void remove_edge(node_indext a, node_indext b)
A Template Class for Graphs.
bool find_second_event(event_idt source)
bool is_local(event_idt a)
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...
const wmm_grapht::edgest & com_in(event_idt n) const
std::set< event_idt > thin_air_events
void print_rec_graph(std::ofstream &file, event_idt node_id, std::set< event_idt > &visited)
critical_cyclet extract_cycle(event_idt vertex, event_idt source, unsigned number_of_cycles)
extracts a (whole, unreduced) cycle from the stack.
void collect_pairs(namespacet &ns)
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
std::set< event_idt > visited_nodes
delayt(event_idt _first, event_idt _second)
void add_com_edge(event_idt a, event_idt b)
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
virtual std::list< event_idt > * order_filtering(std::list< event_idt > *order)
void add_edge(node_indext a, node_indext b)
std::set< std::pair< event_idt, event_idt > > loops
std::string print_unsafes() const
std::string print_name(memory_modelt model) const
std::map< unsigned, data_dpt > map_data_dp
const edgest & in(node_indext n) const
bool is_not_weak_uniproc() const
event_grapht(messaget &_message)
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
bool has_user_defined_fence
std::string print() const
std::stack< event_idt > point_stack
const std::set< event_idt > & filter
std::set< event_idt > skip_tracked
void remove_edge(event_idt a, event_idt b)
graph_conc_explorert(event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans, const std::set< event_idt > &_filter)
std::string print_events() const
bool is_not_uniproc(memory_modelt model) const
std::set< std::pair< const abstract_eventt &, const abstract_eventt & > > duplicated_bodies
void explore_copy_segment(std::set< event_idt > &explored, event_idt begin, event_idt end) const
copies the segment
virtual bool filtering(event_idt u)