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)
32 file << node_id <<
"[label=\"" << node <<
", " << node.
source_location <<
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];
192 const_iterator AC_it=s_it;
194 for(; AC_it!=end(); ++AC_it)
209 if(AC_it==end() && egraph[front()].thread==second.
thread)
211 for(AC_it=begin(); ; ++AC_it)
234 const_iterator BC_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;
291 const_iterator th_it;
293 th_it!=end() && thread==egraph[*th_it].thread; ++th_it)
294 thread=egraph[*th_it].thread;
299 const_iterator it=begin();
300 const_iterator next=it;
302 for(; it!=end() && next!=end(); ++next, ++it)
319 const_iterator s_it=next;
350 if(check_AC(s_it, first, second))
353 if(check_BC(it, first, second))
357 const_iterator n_it=it;
363 && (first.
thread!=second.
thread || egraph.are_po_ordered(*it, *s_it)))
365 const_iterator before_first;
366 const_iterator after_second;
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)))
407 const_iterator before_first;
408 const_iterator after_second;
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;
576 const_iterator th_it;
578 th_it!=end() && thread==egraph[*th_it].thread; ++th_it)
579 thread=egraph[*th_it].thread;
584 for(const_iterator it=begin(); it!=end() && ++it!=end(); it++)
602 const_iterator s_it=++it;
609 fences_met |= egraph[*s_it].fence_value();
637 const_iterator AC_it=++s_it;
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]))
671 const_iterator BC_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();
792 const_iterator AC_it=++s_it;
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))
826 const_iterator BC_it=end();
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);
897 const_iterator it=begin();
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)
935 const_iterator it=begin();
938 for(; it!=end(); it++)
951 const irep_idt &var=egraph[*it].variable;
953 const_iterator prev=it;
954 for(; it!=end(); prev=it, ++it)
976 for(const_iterator it=begin(); it!=end(); ++it)
978 const_iterator n_it=it;
995 if(dep.
dp(current, next))
1012 if(dep.
dp(current, next))
1020 std::string cycle=
"Cycle: ";
1021 for(const_iterator it=begin(); it!=end(); ++it)
1022 cycle += std::to_string(egraph[*it].
id) +
"; ";
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: ";
1076 for(const_iterator it=begin(); it!=end(); ++it)
1082 return cycle+
" End of cycle.";
1088 for(const_iterator it=begin(); it!=end(); ++it)
1093 cycle +=
" thread " + std::to_string(it_evt.
thread) +
") ";
1100 std::map<std::string, std::string> &map_id2var,
1101 std::map<std::string, std::string> &map_var2id,
1105 for(const_iterator it=reduced.begin(); it!=reduced.end(); ++it)
1110 if(map_var2id.find(var_name)!=map_var2id.end())
1112 cycle +=
"t" + std::to_string(it_evt.
thread) +
" (";
1113 cycle += map_var2id[var_name] +
") ";
1117 const std::string new_id=
"var@" + std::to_string(map_var2id.size());
1118 map_var2id[var_name]=new_id;
1119 map_id2var[new_id]=var_name;
1120 cycle +=
"t" + std::to_string(it_evt.
thread) +
" (";
1121 cycle += new_id +
") ";
1129 std::map<std::string, std::string> &map_id2var,
1130 std::map<std::string, std::string> &map_var2id,
1131 bool hide_internals)
const 1141 this->hide_internals(reduced);
1142 assert(reduced.size() > 0);
1143 cycle+=print_detail(reduced, map_id2var, map_var2id, model);
1145 cycle+=print_name(reduced, model);
1149 cycle+=print_detail(*
this, map_id2var, map_var2id, model);
1151 cycle+=print_name(*
this, model);
1160 std::set<event_idt> reduced_evts;
1161 const_iterator first_it, prev_it=end();
1164 for(first_it=begin(); first_it!=end(); ++first_it)
1167 if(prev_it!=end() && egraph[*prev_it].thread!=first.
thread 1172 assert(first_it!=end());
1173 reduced.push_back(*first_it);
1174 reduced_evts.insert(*first_it);
1177 for(const_iterator cur_it=first_it; cur_it!=end(); ++cur_it)
1183 const_iterator next_it=cur_it;
1188 if(cur.
thread!=egraph[*next_it].thread)
1190 if(reduced_evts.find(*cur_it)==reduced_evts.end())
1192 reduced.push_back(*cur_it);
1193 reduced_evts.insert(*cur_it);
1195 for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1196 assert(next_it!=end());
1197 if(reduced_evts.find(*next_it)==reduced_evts.end())
1199 reduced.push_back(*next_it);
1200 reduced_evts.insert(*next_it);
1205 for(const_iterator cur_it=begin(); cur_it!=first_it; ++cur_it)
1211 const_iterator next_it=cur_it;
1213 assert(next_it!=end());
1215 if(cur.
thread!=egraph[*next_it].thread)
1217 if(reduced_evts.find(*cur_it)==reduced_evts.end())
1219 reduced.push_back(*cur_it);
1220 reduced_evts.insert(*cur_it);
1222 for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1223 assert(next_it!=end());
1224 if(reduced_evts.find(*next_it)==reduced_evts.end())
1226 reduced.push_back(*next_it);
1227 reduced_evts.insert(*next_it);
1237 assert(reduced.size()>=2);
1238 unsigned extra_fence_count=0;
1241 const_iterator prev_it=reduced.end();
1242 bool first_done=
false;
1243 for(const_iterator cur_it=reduced.begin(); cur_it!=reduced.end(); ++cur_it)
1247 if(prev_it!=reduced.end())
1255 ++extra_fence_count;
1261 const_iterator n_it=cur_it;
1262 bool wraparound=
false;
1266 if(n_it==reduced.end())
1268 assert(!wraparound);
1271 ++extra_fence_count;
1272 n_it=reduced.begin();
1282 ++extra_fence_count;
1287 name += (model==
Power?
" Sync":
" MFence");
1294 std::string cand_name=
" LwSync";
1295 const_iterator n_it=cur_it;
1296 bool wraparound=
false;
1300 if(n_it==reduced.end())
1302 assert(!wraparound);
1305 ++extra_fence_count;
1306 n_it=reduced.begin();
1316 cand_name=(model==
Power?
" Sync":
" MFence");
1320 ++extra_fence_count;
1332 std::string cand_name;
1334 cand_name=(model==
Power?
" Sync":
" MFence");
1336 cand_name=
" LwSync";
1337 const_iterator n_it=cur_it;
1338 bool wraparound=
false;
1342 if(n_it==reduced.end())
1344 assert(!wraparound);
1347 ++extra_fence_count;
1348 n_it=reduced.begin();
1358 cand_name=(model==
Power?
" Sync":
" MFence");
1362 ++extra_fence_count;
1431 for(std::string::const_iterator it=name.begin();
1436 assert(n_events==reduced.size());
1452 std::string cand_name=
" LwSync";
1453 const_iterator it=reduced.begin();
1454 for( ; it!=reduced.end(); ++it)
1465 cand_name=(model==
Power?
" Sync":
" MFence");
1467 assert(it!=reduced.begin() && it!=reduced.end());
1472 name += (last.
variable==succ.variable?
"s":
"d")
1487 && (last.
thread!=first.
thread || reduced.back() > reduced.front()))
1496 (last.
thread!=first.
thread || reduced.back() > reduced.front()))
1508 dep.
dp(last, first))
1527 for(std::string::const_iterator it=name.begin();
1532 assert(n_events==reduced.size());
1544 for(const_iterator it=begin(); it!=end(); ++it)
1549 str <<
"/* " <<
id <<
" */\n";
1553 str <<
"{" << ev.
variable <<
"} {} @thread" << ev.
thread <<
"\"];\n";
1557 const_iterator prev_it=end();
1558 for(const_iterator cur_it=begin(); cur_it!=end(); ++cur_it)
1563 str <<
"/* " <<
id <<
" */\n";
1570 str << prev.
id <<
"->";
1573 const_iterator n_it=cur_it;
1576 n_it!=end() ? egraph[*n_it] : egraph[front()];
1577 str << succ.
id <<
"[label=\"";
1578 str << (model==
Power?
"Sync":
"MFence");
1584 const_iterator n_it=cur_it;
1587 n_it!=end() ? egraph[*n_it] : egraph[front()];
1588 str << succ.
id <<
"[label=\"";
1596 str << cur.
id <<
"[label=\"";
1603 str << cur.
id <<
"[label=\"";
1612 str << cur.
id <<
"[label=\"";
1618 str << cur.
id <<
"[label=\"";
1623 str << cur.
id <<
"[label=\"?";
1635 str <<
"/* " <<
id <<
" */\n";
1638 str << last.
id <<
"->";
1641 const_iterator next=begin();
1644 str << succ.
id <<
"[label=\"";
1645 str << (model==
Power?
"Sync":
"MFence");
1651 const_iterator next=begin();
1654 str << succ.
id <<
"[label=\"";
1662 str << first.
id <<
"[label=\"";
1669 str << first.
id <<
"[label=\"";
1678 str << first.
id <<
"[label=\"";
1684 str << first.
id <<
"[label=\"";
1689 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 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 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
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
wmm_grapht::node_indext event_idt
bool has_com_edge(event_idt i, event_idt j) const
bool check_AC(const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) 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)
void add_com_edge(event_idt a, event_idt b)
static const char * colour_map[14]
std::string print_unsafes() const
source_locationt source_location
bool is_not_weak_uniproc() const
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 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