69 for(std::set<event_grapht::critical_cyclet>::const_iterator
78 std::set<event_idt> new_wr_set;
82 std::set<event_idt> new_ww_set;
86 std::set<event_idt> new_rw_set;
90 std::set<event_idt> new_rr_set;
96 std::set<event_idt> new_comset;
111 for(std::list<std::set<event_idt> >::const_iterator
117 for(std::set<event_idt>::const_iterator
122 std::set<unsigned> pt_set;
129 for(std::list<std::set<event_idt> >::const_iterator
135 for(std::set<event_idt>::const_iterator
136 e_nc_it=e_i->begin();
140 std::set<unsigned> pt_set;
147 for(std::list<std::set<event_idt> >::const_iterator
153 for(std::set<event_idt>::const_iterator
154 e_nc_it=e_i->begin();
158 std::set<unsigned> pt_set;
165 for(std::list<std::set<event_idt> >::const_iterator
171 for(std::set<event_idt>::const_iterator
172 e_nc_it=e_i->begin();
176 std::set<unsigned> pt_set;
185 for(std::list<std::set<event_idt> >::const_iterator
191 for(std::set<event_idt>::const_iterator
196 std::set<unsigned> ct_set;
202 std::set<unsigned> ct_not_powr_set;
219 const bool has_cost=1;
230 for(std::set<event_grapht::critical_cyclet>::const_iterator
240 std::list<event_idt>::const_iterator it;
241 for(it=C_j->begin(); it!=C_j->end() &&
col_to_var(i)!=*it; ++it)
255 const std::string name_dp=
"dp_"+std::to_string(i);
256 glp_set_col_name(ilp.lp, i, name_dp.c_str());
257 glp_set_col_bnds(ilp.lp, i, GLP_LO, 0.0, 0.0);
258 glp_set_obj_coef(ilp.lp, i, (has_cost?
fence_cost(
Dp):0)*freq_sum);
259 glp_set_col_kind(ilp.lp, i, GLP_BV);
262 const std::string name_f=
"f_"+std::to_string(i);
263 glp_set_col_name(ilp.lp, i+1, name_f.c_str());
264 glp_set_col_bnds(ilp.lp, i+1, GLP_LO, 0.0, 0.0);
265 glp_set_obj_coef(ilp.lp, i+1, (has_cost?
fence_cost(
Fence):0)*freq_sum);
266 glp_set_col_kind(ilp.lp, i+1, GLP_BV);
271 const std::string name_br=
"br_"+std::to_string(i);
272 glp_set_col_name(ilp.lp, i+2, name_br.c_str());
273 glp_set_col_bnds(ilp.lp, i+2, GLP_LO, 0.0, 0.0);
276 glp_set_col_kind(ilp.lp, i+2, GLP_BV);
279 const std::string name_cf=
"cf_"+std::to_string(i);
280 glp_set_col_name(ilp.lp, i+3, name_cf.c_str());
281 glp_set_col_bnds(ilp.lp, i+3, GLP_LO, 0.0, 0.0);
283 glp_set_col_kind(ilp.lp, i+3, GLP_BV);
289 const std::string name_lwf=
"lwf_"+std::to_string(i);
290 glp_set_col_name(ilp.lp, i+2, name_lwf.c_str());
291 glp_set_col_bnds(ilp.lp, i+2, GLP_LO, 0.0, 0.0);
292 glp_set_obj_coef(ilp.lp, i+2,
294 glp_set_col_kind(ilp.lp, i+2, GLP_BV);
300 const std::string name_f=
"f_"+std::to_string(i);
301 glp_set_col_name(ilp.lp, i, name_f.c_str());
302 glp_set_col_bnds(ilp.lp, i, GLP_LO, 0.0, 0.0);
304 glp_set_col_kind(ilp.lp, i, GLP_BV);
308 throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
320 std::list<std::set<event_idt> >::const_iterator c_wr_it =
326 for(std::size_t j=1; j<=c_wr_it->size(); ++j)
328 std::string name=
"C_"+std::to_string(i)+
"_c_wr_"+std::to_string(j);
329 glp_set_row_name(ilp.lp, i, name.c_str());
330 glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0);
336 for(std::list<std::set<event_idt> >::const_iterator
342 for(std::size_t j=1; j<=c_ww_it->size(); ++j)
344 std::string name=
"C_"+std::to_string(i)+
"_c_ww_"+std::to_string(j);
345 glp_set_row_name(ilp.lp, i, name.c_str());
346 glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0);
352 for(std::list<std::set<event_idt> >::const_iterator
358 for(std::size_t j=1; j<=c_rw_it->size(); ++j)
360 std::string name=
"C_"+std::to_string(i)+
"_c_rw_"+std::to_string(j);
361 glp_set_row_name(ilp.lp, i, name.c_str());
362 glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0);
369 std::list<std::set<event_idt> >::const_iterator c_rr_it =
375 for(std::size_t j=1; j<=c_rr_it->size(); ++j)
377 std::string name=
"C_"+std::to_string(i)+
"_c_rr_"+std::to_string(j);
378 glp_set_row_name(ilp.lp, i, name.c_str());
379 glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0);
386 for(std::list<std::set<event_idt> >::const_iterator
392 for(std::size_t j=1; j<=c_it->size(); ++j)
394 std::string name=
"C_"+std::to_string(i)+
"_c_"+std::to_string(j);
395 glp_set_row_name(ilp.lp, i, name.c_str());
396 glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0);
402 throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
409 unsigned const_constraints_number,
410 unsigned const_unique)
418 for(std::list<std::set<event_idt> >::const_iterator
424 for(std::set<event_idt>::const_iterator
429 std::set<unsigned> pt_set;
435 assert(row<=const_constraints_number);
449 if(pt_set.find(
col_to_var(col))!=pt_set.end() &&
462 for(std::list<std::set<event_idt> >::const_iterator
468 for(std::set<event_idt>::const_iterator
469 e_nc_it=e_i->begin();
473 std::set<unsigned> pt_set;
479 assert(row<=const_constraints_number);
485 if(pt_set.find(
col_to_var(col))!=pt_set.end() &&
493 if(pt_set.find(
col_to_var(col))!=pt_set.end() &&
506 for(std::list<std::set<event_idt> >::const_iterator
512 for(std::set<event_idt>::const_iterator
513 e_nc_it=e_i->begin();
517 std::set<unsigned> pt_set;
523 assert(row<=const_constraints_number);
530 (pt_set.find(
col_to_var(col))!=pt_set.end() &&
544 (pt_set.find(
col_to_var(col))!=pt_set.end() &&
556 if(pt_set.find(
col_to_var(col))!=pt_set.end() &&
573 for(std::list<std::set<event_idt> >::const_iterator
579 for(std::set<event_idt>::const_iterator
580 e_nc_it=e_i->begin();
584 std::set<unsigned> pt_set;
589 std::set<unsigned> it_set;
590 IT(
map_to_e.find(*e_nc_it)->second, it_set);
595 assert(row<=const_constraints_number);
602 (pt_set.find(
col_to_var(col))!=pt_set.end() &&
605 || (it_set.find(
col_to_var(col))!=it_set.end()
616 (pt_set.find(
col_to_var(col))!=pt_set.end() &&
619 || (it_set.find(
col_to_var(col))!=it_set.end()
629 if(pt_set.find(
col_to_var(col))!=pt_set.end() &&
644 for(std::list<std::set<event_idt> >::const_iterator
650 for(std::set<event_idt>::const_iterator
655 unsigned possibilities_met=0;
657 std::set<unsigned> ct_set;
663 std::set<unsigned> ct_not_powr_set;
665 *e_c_it)->second, ct_not_powr_set);
675 assert(row<=const_constraints_number);
679 if((ct_set.find(
col_to_var(col))!=ct_set.end() &&
681 (ct_not_powr_set.find(
col_to_var(col))!=ct_not_powr_set.end() &&
692 assert(possibilities_met);
699 throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
724 const unsigned const_unique=
unique;
726 const std::size_t mat_size=
736 ilp.set_size(mat_size);
751 for(i=1; i<=mat_size; ++i)
764 switch(glp_mip_status(ilp.lp))
775 <<
"yet not proven optimal, " 776 <<
"due to early termination" 781 <<
"No feasible solution, the system is UNSAT" <<
messaget::eom;
792 if(glp_mip_col_val(ilp.lp, j)>=1)
801 << egraph[delay.first].source_location <<
" and " 808 throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
820 std::set<std::string> non_redundant_display;
821 for(std::map<edget, fence_typet>::const_iterator it=
fenced_edges.begin();
825 std::ostringstream s;
831 non_redundant_display.insert(s.str());
834 std::ofstream results;
835 results.open(
"results.txt");
836 for(std::set<std::string>::const_iterator it=non_redundant_display.begin();
837 it!=non_redundant_display.end();
847 std::set<std::string> non_redundant_display;
848 for(std::map<edget, fence_typet>::const_iterator it=
fenced_edges.begin();
852 std::ostringstream s;
860 non_redundant_display.insert(s.str());
863 std::ofstream results;
864 results.open(
"results.txt");
865 for(std::set<std::string>::const_iterator it=non_redundant_display.begin();
866 it!=non_redundant_display.end();
876 std::set<std::string> non_redundant_display;
877 for(std::map<edget, fence_typet>::const_iterator it=
fenced_edges.begin();
881 std::ostringstream s;
894 non_redundant_display.insert(s.str());
899 <<
"Couldn't retrieve symbols of variables " << first.
variable 904 std::ofstream results;
905 results.open(
"results.txt");
906 for(std::set<std::string>::const_iterator it=non_redundant_display.begin();
907 it!=non_redundant_display.end();
917 std::set<std::string> non_redundant_display;
918 for(std::map<edget, fence_typet>::const_iterator it=
fenced_edges.begin();
922 std::ostringstream s;
938 non_redundant_display.insert(s.str());
940 catch (std::string s)
943 <<
"Couldn't retrieve types of variables " << first.
variable 948 std::ofstream results;
949 results.open(
"results.txt");
950 for(std::set<std::string>::const_iterator it=non_redundant_display.begin();
951 it!=non_redundant_display.end();
961 case Fence:
return "fence";
962 case Lwfence:
return "lwfence";
963 case Dp:
return "dp";
980 case 0:
return Fence;
1024 <<
"---- pos/pos+ (visible) variables ----" <<
messaget::eom;
1025 for(std::map<edget, unsigned>::const_iterator it=
map_from_e.begin();
1031 for(std::map<edget, unsigned>::const_iterator it=
1044 if(copy.find(
"[]")!=std::string::npos)
1045 copy=copy.substr(0, copy.find_last_of(
"[]")-1);
1052 std::list<std::string> fields;
1053 std::string current;
1056 std::string::const_iterator it=copy.begin();
1057 std::string::const_iterator next=it;
1058 for(; it!=copy.end(); ++it)
1062 if(!(*it==
'.' || (next!=copy.end() && *it==
'-' && *next==
'>')))
1069 fields.push_back(current);
1074 assert(next!=copy.end());
1086 std::list<std::string>::const_iterator it,
1087 std::list<std::string>::const_iterator end,
1093 if(type.
id()==ID_struct)
1101 if(type.
id()==ID_symbol)
std::map< unsigned, edget > & map_to_e
normal variables used almost every time
The type of an expression.
std::map< edget, unsigned > & map_from_e
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
std::string to_string(fence_typet f) const
unsigned col_to_var(unsigned u) const
virtual void process_cycles_selection()
const irep_idt & get_function() const
std::list< std::set< event_idt > > powr_constraints
static mstreamt & eom(mstreamt &m)
void CT_not_powr(const edget &e, std::set< unsigned > &edges)
typet get_type(const irep_idt &id)
const irep_idt & get_column() const
void poww_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
void powr_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
typet type_component(std::list< std::string >::const_iterator it, std::list< std::string >::const_iterator end, const typet &type)
std::map< edget, fence_typet > fenced_edges
const irep_idt & id() const
void CT(const edget &e, std::set< unsigned > &edges)
const irep_idt & get_line() const
std::map< edget, unsigned > map_from_e
void po_edges(std::set< event_idt > &edges)
const memory_modelt model
const irep_idt & get(const irep_namet &name) const
fence_typet col_to_fence(unsigned u) const
virtual unsigned fence_cost(fence_typet e) const
virtual bool filter_cycles(unsigned cycle_id) const
typet component_type(const irep_idt &component_name) const
std::list< std::set< event_idt > > porr_constraints
A Template Class for Graphs.
unsigned var_fence_to_col(fence_typet f, unsigned var) const
const irep_idt & get_file() const
void porr_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
void mip_fill_matrix(ilpt &ilp, unsigned &i, unsigned const_constraints_number, unsigned const_unique)
Base type of C structs and unions, and C++ classes.
std::list< std::set< event_idt > > com_constraints
ILP construction for all cycles and resolution.
void porw_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
instrumentert & instrumenter
void compute_fence_options()
source_locationt source_location
std::set< event_grapht::critical_cyclet > set_of_cycles
void mip_set_var(ilpt &ilp, unsigned &i)
cycles_visitort cycles_visitor
void PT(const edget &e, std::set< unsigned > &edges)
void com_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
std::list< std::set< event_idt > > porw_constraints
void mip_set_cst(ilpt &ilp, unsigned &i)
std::map< unsigned, edget > map_to_e
std::map< unsigned, float > freq_table
std::size_t constraints_number
number of constraints
std::list< std::set< event_idt > > poww_constraints