23 {
"red",
"blue",
"black",
"green",
"yellow",
24 "orange",
"blueviolet",
"cyan",
"cadetblue",
"magenta",
"palegreen",
25 "deeppink",
"indigo",
"olivedrab"};
26 #define print_colour(u) colour_map[u%NB_COLOURS] 29 std::set<event_idt> &visited)
34 visited.insert(node_id);
36 for(wmm_grapht::edgest::const_iterator
37 it=
po_out(node_id).begin();
38 it!=
po_out(node_id).end(); ++it)
40 file << node_id <<
"->" << it->first <<
"[]\n";
41 file <<
"{rank=same; " << node_id <<
"; " << it->first <<
"}\n";
42 if(visited.find(it->first)==visited.end())
46 for(wmm_grapht::edgest::const_iterator
48 it!=
com_out(node_id).end(); ++it)
50 file << node_id <<
"->" << it->first <<
"[style=\"dotted\"]\n";
51 if(visited.find(it->first)==visited.end())
59 std::set<event_idt> visited;
62 file.open(
"graph.dot");
63 file <<
"digraph G {\n";
64 file <<
"rankdir=LR;\n";
76 if(explored.find(begin)!=explored.end())
79 explored.insert(begin);
84 for(wmm_grapht::edgest::const_iterator it=
po_out(begin).begin();
111 std::set<event_idt> covered;
123 std::map<event_idt, event_idt> orig2copy;
126 for(std::set<event_idt>::const_iterator it=covered.begin();
132 orig2copy[*it]=new_node;
140 for(std::set<event_idt>::const_iterator it_i=covered.begin();
144 for(std::set<event_idt>::const_iterator it_j=covered.begin();
162 for(std::set<event_idt>::const_iterator it_i=covered.begin();
183 return orig2copy[end];
194 for(; AC_it!=
end(); ++AC_it)
211 for(AC_it=
begin(); ; ++AC_it)
245 for(; BC_it!=begin(); --BC_it)
260 if(BC_it==begin() && egraph[back()].thread==first.
thread)
283 bool unsafe_met=
false;
290 unsigned thread=egraph[*begin()].thread;
293 th_it!=end() && thread==egraph[*th_it].thread; ++th_it)
294 thread=egraph[*th_it].thread;
302 for(; it!=end() && next!=end(); ++next, ++it)
350 if(check_AC(s_it, first, second))
353 if(check_BC(it, first, second))
363 && (first.
thread!=second.
thread || egraph.are_po_ordered(*it, *s_it)))
377 after_second=begin();
383 && egraph[*before_first].thread!=first.
thread 384 && egraph[*after_second].thread!=second.
thread)
395 unsafe_pairs.insert(delay);
405 && (first.
thread!=second.
thread || egraph.are_po_ordered(*it, *s_it)))
419 after_second=begin();
425 && egraph[*before_first].thread!=first.
thread 426 && egraph[*after_second].thread!=second.
thread)
437 unsafe_pairs.insert(delay);
482 if(check_AC(s_it, first, second))
485 if(check_BC(begin(), first, second))
493 && (first.
thread!=second.
thread || egraph.are_po_ordered(back(), *s_it)))
495 std::list<event_idt>::const_iterator before_first;
496 std::list<event_idt>::const_iterator after_second;
507 && egraph[*before_first].thread!=first.
thread 508 && egraph[*after_second].thread!=second.
thread)
517 unsafe_pairs.insert(delay);
527 && (first.
thread!=second.
thread || egraph.are_po_ordered(back(), *s_it)))
529 std::list<event_idt>::const_iterator before_first;
530 std::list<event_idt>::const_iterator after_second;
541 && egraph[*before_first].thread!=first.
thread 542 && egraph[*after_second].thread!=second.
thread)
551 unsafe_pairs.insert(delay);
567 bool unsafe_met=
false;
568 unsigned char fences_met=0;
575 unsigned thread=egraph[*begin()].thread;
578 th_it!=end() && thread==egraph[*th_it].thread; ++th_it)
579 thread=egraph[*th_it].thread;
609 fences_met |= egraph[*s_it].fence_value();
640 AC_it!=end() && egraph[*AC_it].thread==second.
thread;
643 && egraph[*AC_it].is_cumul()
644 && egraph[*AC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
653 if(AC_it==end() && egraph[front()].thread==second.
thread)
656 !(egraph[*AC_it]==first) && egraph[*AC_it].thread==second.
thread;
659 egraph[*AC_it].is_cumul() &&
660 egraph[*AC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
683 BC_it!=begin() && egraph[*BC_it].thread==first.
thread;
687 egraph[*BC_it].is_cumul() &&
688 egraph[*BC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
698 if(BC_it==begin() && egraph[back()].thread==first.
thread)
701 !(egraph[*BC_it]==second) && egraph[*BC_it].thread==first.
thread;
704 egraph[*BC_it].is_cumul() &&
705 egraph[*BC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
722 && (first.
thread!=second.
thread || egraph.are_po_ordered(*it, *s_it)))
729 unsafe_pairs.insert(delay);
740 && (first.
thread!=second.
thread || egraph.are_po_ordered(*it, *s_it)))
747 unsafe_pairs.insert(delay);
767 fences_met |= egraph[*s_it].fence_value();
795 AC_it!=end() && egraph[*AC_it].thread==second.
thread;
798 && egraph[*AC_it].is_cumul()
799 && egraph[*AC_it].is_corresponding_fence(first, second))
808 if(AC_it==end() && egraph[front()].thread==second.
thread)
811 !(egraph[*AC_it]==first) && egraph[*AC_it].thread==second.
thread;
814 egraph[*AC_it].is_cumul() &&
815 egraph[*AC_it].is_corresponding_fence(first, second))
830 BC_it!=begin() && egraph[*BC_it].thread==first.
thread;
833 && egraph[*BC_it].is_cumul()
834 && egraph[*BC_it].is_corresponding_fence(first, second))
843 if(BC_it==begin() && egraph[back()].thread==first.
thread)
848 !(egraph[*BC_it]==second) && egraph[*BC_it].thread==first.
thread;
851 && egraph[*BC_it].is_cumul()
852 && egraph[*BC_it].is_corresponding_fence(first, second))
867 && (first.
thread!=second.
thread || egraph.are_po_ordered(back(), *s_it)))
872 unsafe_pairs.insert(delay);
881 && (first.
thread!=second.
thread || egraph.are_po_ordered(back(), *s_it)))
886 unsafe_pairs.insert(delay);
900 for(; it!=end(); ++it)
913 const irep_idt &var=egraph[*it].variable;
917 if(!egraph.ignore_arrays &&
id2string(var).find(
"[]")!=std::string::npos)
920 for(; it!=end(); ++it)
938 for(; it!=end(); it++)
951 const irep_idt &var=egraph[*it].variable;
954 for(; it!=end(); prev=it, ++it)
995 if(dep.
dp(current, next))
1012 if(dep.
dp(current, next))
1020 std::string cycle=
"Cycle: ";
1023 return cycle +
" End of cycle.";
1028 std::string name=
"Unsafe pairs: ";
1029 for(std::set<delayt>::const_iterator it=unsafe_pairs.begin();
1030 it!=unsafe_pairs.end();
1075 std::string cycle=
"Cycle: ";
1082 return cycle+
" End of cycle.";
1100 std::map<std::string, std::string> &map_id2var,
1101 std::map<std::string, std::string> &map_var2id)
const 1109 if(map_var2id.find(var_name)!=map_var2id.end())
1112 cycle += map_var2id[var_name] +
") ";
1116 const std::string new_id=
"var@" +
std::to_string(map_var2id.size());
1117 map_var2id[var_name]=new_id;
1118 map_id2var[new_id]=var_name;
1120 cycle += new_id +
") ";
1128 std::map<std::string, std::string> &map_id2var,
1129 std::map<std::string, std::string> &map_var2id,
1130 bool hide_internals)
const 1140 this->hide_internals(reduced);
1141 assert(reduced.
size() > 0);
1142 cycle+=print_detail(reduced, map_id2var, map_var2id);
1144 cycle+=print_name(reduced, model);
1148 cycle+=print_detail(*
this, map_id2var, map_var2id);
1150 cycle+=print_name(*
this, model);
1159 std::set<event_idt> reduced_evts;
1163 for(first_it=begin(); first_it!=end(); ++first_it)
1166 if(prev_it!=end() && egraph[*prev_it].thread!=first.
thread 1171 assert(first_it!=end());
1173 reduced_evts.insert(*first_it);
1187 if(cur.
thread!=egraph[*next_it].thread)
1189 if(reduced_evts.find(*cur_it)==reduced_evts.end())
1192 reduced_evts.insert(*cur_it);
1194 for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1195 assert(next_it!=end());
1196 if(reduced_evts.find(*next_it)==reduced_evts.end())
1199 reduced_evts.insert(*next_it);
1212 assert(next_it!=end());
1214 if(cur.
thread!=egraph[*next_it].thread)
1216 if(reduced_evts.find(*cur_it)==reduced_evts.end())
1219 reduced_evts.insert(*cur_it);
1221 for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1222 assert(next_it!=end());
1223 if(reduced_evts.find(*next_it)==reduced_evts.end())
1226 reduced_evts.insert(*next_it);
1236 assert(reduced.
size()>=2);
1237 unsigned extra_fence_count=0;
1241 bool first_done=
false;
1246 if(prev_it!=reduced.
end())
1254 ++extra_fence_count;
1261 bool wraparound=
false;
1265 if(n_it==reduced.
end())
1267 assert(!wraparound);
1270 ++extra_fence_count;
1271 n_it=reduced.
begin();
1281 ++extra_fence_count;
1286 name += (model==
Power?
" Sync":
" MFence");
1293 std::string cand_name=
" LwSync";
1295 bool wraparound=
false;
1299 if(n_it==reduced.
end())
1301 assert(!wraparound);
1304 ++extra_fence_count;
1305 n_it=reduced.
begin();
1315 cand_name=(model==
Power?
" Sync":
" MFence");
1319 ++extra_fence_count;
1331 std::string cand_name;
1333 cand_name=(model==
Power?
" Sync":
" MFence");
1335 cand_name=
" LwSync";
1337 bool wraparound=
false;
1341 if(n_it==reduced.
end())
1343 assert(!wraparound);
1346 ++extra_fence_count;
1347 n_it=reduced.
begin();
1357 cand_name=(model==
Power?
" Sync":
" MFence");
1361 ++extra_fence_count;
1429 auto n_events=extra_fence_count;
1430 for(std::string::const_iterator it=name.begin();
1435 assert(n_events==reduced.
size());
1451 std::string cand_name=
" LwSync";
1453 for( ; it!=reduced.
end(); ++it)
1464 cand_name=(model==
Power?
" Sync":
" MFence");
1466 assert(it!=reduced.
begin() && it!=reduced.
end());
1471 name += (last.
variable==succ.variable?
"s":
"d")
1507 dep.
dp(last, first))
1526 for(std::string::const_iterator it=name.begin();
1531 assert(n_events==reduced.
size());
1548 str <<
"/* " <<
id <<
" */\n";
1552 str <<
"{" << ev.
variable <<
"} {} @thread" << ev.
thread <<
"\"];\n";
1562 str <<
"/* " <<
id <<
" */\n";
1569 str << prev.
id <<
"->";
1575 n_it!=end() ? egraph[*n_it] : egraph[front()];
1576 str << succ.
id <<
"[label=\"";
1577 str << (model==
Power?
"Sync":
"MFence");
1586 n_it!=end() ? egraph[*n_it] : egraph[front()];
1587 str << succ.
id <<
"[label=\"";
1595 str << cur.
id <<
"[label=\"";
1602 str << cur.
id <<
"[label=\"";
1611 str << cur.
id <<
"[label=\"";
1617 str << cur.
id <<
"[label=\"";
1622 str << cur.
id <<
"[label=\"?";
1634 str <<
"/* " <<
id <<
" */\n";
1637 str << last.
id <<
"->";
1643 str << succ.
id <<
"[label=\"";
1644 str << (model==
Power?
"Sync":
"MFence");
1653 str << succ.
id <<
"[label=\"";
1661 str << first.
id <<
"[label=\"";
1668 str << first.
id <<
"[label=\"";
1677 str << first.
id <<
"[label=\"";
1683 str << first.
id <<
"[label=\"";
1688 str << first.
id <<
"[label=\"?";
std::list< event_idt > po_order
grapht< abstract_eventt >::nodet & operator[](event_idt n)
const std::string & id2string(const irep_idt &d)
std::string print_name(const critical_cyclet &redyced, memory_modelt model) const
bool is_not_thin_air() const
bool unsafe_pair_asm(const abstract_eventt &next, memory_modelt model, unsigned char met) const
const irep_idt & get_function() const
std::string as_string() const
void print_dot(std::ostream &str, unsigned colour, memory_modelt model) const
bool is_not_uniproc() const
bool has_po_edge(event_idt i, event_idt j) const
void hide_internals(critical_cyclet &reduced) const
void add_po_edge(event_idt a, event_idt b)
unsignedbv_typet size_type()
static mstreamt & eom(mstreamt &m)
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
unsigned char fence_value() const
data_typet::const_iterator const_iterator
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
const wmm_grapht::edgest & po_out(event_idt n) const
std::string print_output() const
bool unsafe_pair_lwfence(const abstract_eventt &next, memory_modelt model) const
event_idt copy_segment(event_idt begin, event_idt end)
std::string get_operation() const
const wmm_grapht::edgest & com_out(event_idt n) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::string print_detail(const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id) const
wmm_grapht::node_indext event_idt
bool has_com_edge(event_idt i, event_idt j) 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...
const irep_idt & get_file() const
void print_rec_graph(std::ofstream &file, event_idt node_id, std::set< event_idt > &visited)
mstreamt & status() const
void add_com_edge(event_idt a, event_idt b)
bool check_AC(data_typet::const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
static const char * colour_map[14]
std::string print_unsafes() const
source_locationt source_location
bool is_not_weak_uniproc() const
bool check_BC(data_typet::const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
std::string print() const
std::string print_events() 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