cprover
fence_inserter.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ILP construction for all cycles and resolution
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #include "fence_inserter.h"
13 
14 #include <util/graph.h>
15 
16 #include <sstream>
17 #include <fstream>
18 
19 #ifdef HAVE_GLPK
20 #include <glpk.h>
21 #include <cstdlib>
22 #endif
23 
24 #include "ilp.h"
25 
26 class abstract_eventt;
27 
29 {
30  switch(f)
31  {
32  case Fence:
33  return 3;
34  case Lwfence:
35  return 2;
36  case Dp:
37  return 1;
38  case Branching:
39  return 2;
40  case Ctlfence:
41  return 1;
42  }
43  assert(false);
44  return 0;
45 }
46 
48 {
50  instrumenter.message.status() << "Preprocessing" << messaget::eom;
51  preprocess();
52  instrumenter.message.status() << "Solving" << messaget::eom;
53  if(unique>0)
54  solve();
55  else
56  instrumenter.message.result() << "no cycle concerned" << messaget::eom;
57 }
58 
60 {
62 
64 
65  /* TODO: replace lists by sets and carefully count the number of constraints
66  _with_ removing the existing ones (i.e., those which are not inserted) */
67 
68  instrumenter.message.status() << "Preparing cycles" << messaget::eom;
69  for(std::set<event_grapht::critical_cyclet>::const_iterator
70  C_j=instrumenter.set_of_cycles.begin();
71  C_j!=instrumenter.set_of_cycles.end();
72  ++C_j)
73  {
74  /* filtering */
75  if(filter_cycles(C_j->id))
76  continue;
77 
78  std::set<event_idt> new_wr_set;
79  cycles_visitor.powr_constraint(*C_j, new_wr_set);
80  powr_constraints.push_back(new_wr_set);
81 
82  std::set<event_idt> new_ww_set;
83  cycles_visitor.poww_constraint(*C_j, new_ww_set);
84  poww_constraints.push_back(new_ww_set);
85 
86  std::set<event_idt> new_rw_set;
87  cycles_visitor.porw_constraint(*C_j, new_rw_set);
88  porw_constraints.push_back(new_rw_set);
89 
90  std::set<event_idt> new_rr_set;
91  cycles_visitor.porr_constraint(*C_j, new_rr_set);
92  porr_constraints.push_back(new_rr_set);
93 
94  if(model==Power || model==Unknown)
95  {
96  std::set<event_idt> new_comset;
97  cycles_visitor.com_constraint(*C_j, new_comset);
98  com_constraints.push_back(new_comset);
99  }
100 
101  assert(powr_constraints.size()==poww_constraints.size());
102  assert(poww_constraints.size()==porw_constraints.size());
103  assert(porw_constraints.size()==porr_constraints.size());
104  }
105 
106  // Note: not true if filters
107  // assert(non_powr_constraints.size()==instrumenter.set_of_cycles.size());
108 
109  // NEW
110  /* first, powr constraints: for all C_j */
111  for(std::list<std::set<event_idt> >::const_iterator
112  e_i=powr_constraints.begin();
113  e_i!=powr_constraints.end();
114  ++e_i)
115  {
116  /* for all e */
117  for(std::set<event_idt>::const_iterator
118  e_c_it=e_i->begin();
119  e_c_it!=e_i->end();
120  ++e_c_it)
121  {
122  std::set<unsigned> pt_set;
123  assert(map_to_e.find(*e_c_it)!=map_to_e.end());
124  const_graph_visitor.PT(map_to_e.find(*e_c_it)->second, pt_set);
125  }
126  }
127 
128  /* then, poww constraints: for all C_j */
129  for(std::list<std::set<event_idt> >::const_iterator
130  e_i=poww_constraints.begin();
131  e_i!=poww_constraints.end();
132  ++e_i)
133  {
134  /* for all e */
135  for(std::set<event_idt>::const_iterator
136  e_nc_it=e_i->begin();
137  e_nc_it!=e_i->end();
138  ++e_nc_it)
139  {
140  std::set<unsigned> pt_set;
141  assert(map_to_e.find(*e_nc_it)!=map_to_e.end());
142  const_graph_visitor.PT(map_to_e.find(*e_nc_it)->second, pt_set);
143  }
144  }
145 
146  /* then, porw constraints: for all C_j */
147  for(std::list<std::set<event_idt> >::const_iterator
148  e_i=porw_constraints.begin();
149  e_i!=porw_constraints.end();
150  ++e_i)
151  {
152  /* for all e */
153  for(std::set<event_idt>::const_iterator
154  e_nc_it=e_i->begin();
155  e_nc_it!=e_i->end();
156  ++e_nc_it)
157  {
158  std::set<unsigned> pt_set;
159  assert(map_to_e.find(*e_nc_it)!=map_to_e.end());
160  const_graph_visitor.PT(map_to_e.find(*e_nc_it)->second, pt_set);
161  }
162  }
163 
164  /* then, porr constraints: for all C_j */
165  for(std::list<std::set<event_idt> >::const_iterator
166  e_i=porr_constraints.begin();
167  e_i!=porr_constraints.end();
168  ++e_i)
169  {
170  /* for all e */
171  for(std::set<event_idt>::const_iterator
172  e_nc_it=e_i->begin();
173  e_nc_it!=e_i->end();
174  ++e_nc_it)
175  {
176  std::set<unsigned> pt_set;
177  assert(map_to_e.find(*e_nc_it)!=map_to_e.end());
178  const_graph_visitor.PT(map_to_e.find(*e_nc_it)->second, pt_set);
179  }
180  }
181 
182  if(model==Power || model==Unknown)
183  {
184  /* finally, Power/ARM constraints for Rfes: for all C_j */
185  for(std::list<std::set<event_idt> >::const_iterator
186  e_i=com_constraints.begin();
187  e_i!=com_constraints.end();
188  ++e_i)
189  {
190  /* for all e */
191  for(std::set<event_idt>::const_iterator
192  e_c_it=e_i->begin();
193  e_c_it!=e_i->end();
194  ++e_c_it)
195  {
196  std::set<unsigned> ct_set;
197  assert(invisible_var.map_to_e.find(*e_c_it)!=
198  invisible_var.map_to_e.end());
199  const_graph_visitor.CT(invisible_var.map_to_e.find(*e_c_it)->second,
200  ct_set);
201 
202  std::set<unsigned> ct_not_powr_set;
204  invisible_var.map_to_e.find(*e_c_it)->second, ct_not_powr_set);
205  }
206  }
207  }
208 }
209 
211  ilpt &ilp,
212  unsigned &i)
213 {
214 #ifdef HAVE_GLPK
215  glp_add_cols(ilp.lp, unique*fence_options);
216  // unsigned i=1;
217  for(; i<=unique*fence_options; i+=fence_options)
218  {
219  const bool has_cost=1; // (po_plus.find(i)==po_plus.end());
220  /* has_cost==0 => invisible variable */
221  assert(has_cost); // not useful for this problem
222 
223  /* computes the sum of the frequencies of the cycles in which
224  this event appears, if requested */
225  float freq_sum=0;
226  if(with_freq)
227  {
228  assert(instrumenter.set_of_cycles.size()==freq_table.size());
229  freq_sum += epsilon;
230  for(std::set<event_grapht::critical_cyclet>::const_iterator
231  C_j=instrumenter.set_of_cycles.begin();
232  C_j!=instrumenter.set_of_cycles.end();
233  ++C_j)
234  {
235  /* filters */
236  if(filter_cycles(C_j->id))
237  continue;
238 
239  /* if(C_j->find( col_to_var(i) )!=C_j->end()) */
240  std::list<event_idt>::const_iterator it;
241  for(it=C_j->begin(); it!=C_j->end() && col_to_var(i)!=*it; ++it)
242  {
243  }
244 
245  if(it!=C_j->end())
246  freq_sum += freq_table[C_j->id];
247  }
248  }
249  else
250  freq_sum=1;
251 
252  if(model==Power || model==Unknown)
253  {
254  /* dp variable for e */
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);
260 
261  /* fence variable for e */
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);
267 
268 // Note: uncomment for br and cf fences
269 #if 0
270  /* br variable for e */
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);
274  glp_set_obj_coef(
275  ilp.lp, i+2, (has_cost?fence_cost(Branching):0)*freq_sum);
276  glp_set_col_kind(ilp.lp, i+2, GLP_BV);
277 
278  /* cf variable for e */
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);
282  glp_set_obj_coef(ilp.lp, i+3, (has_cost?fence_cost(Ctlfence):0)*freq_sum);
283  glp_set_col_kind(ilp.lp, i+3, GLP_BV);
284 #endif
285 
286  if(model==Power)
287  {
288  /* lwf variable for e */
289  const std::string name_lwf="lwf_"+std::to_string(i);
290  glp_set_col_name(ilp.lp, i+2/*4*/, name_lwf.c_str());
291  glp_set_col_bnds(ilp.lp, i+2/*4*/, GLP_LO, 0.0, 0.0);
292  glp_set_obj_coef(ilp.lp, i+2/*4*/,
293  (has_cost?fence_cost(Lwfence):0)*freq_sum);
294  glp_set_col_kind(ilp.lp, i+2/*4*/, GLP_BV);
295  }
296  }
297  else
298  {
299  /* fence variable for e */
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);
303  glp_set_obj_coef(ilp.lp, i, (has_cost?fence_cost(Fence):0)*freq_sum);
304  glp_set_col_kind(ilp.lp, i, GLP_BV);
305  }
306  }
307 #else
308  throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
309 #endif
310 }
311 
312 void inline fence_insertert::mip_set_cst(ilpt &ilp, unsigned &i)
313 {
314 #ifdef HAVE_GLPK
315  glp_add_rows(ilp.lp, constraints_number);
316  i=1;
317 
318  /* first the powr: for all C_j */
319  for(
320  std::list<std::set<event_idt> >::const_iterator c_wr_it =
321  powr_constraints.begin();
322  c_wr_it!=powr_constraints.end();
323  ++c_wr_it)
324  {
325  /* for all e */
326  for(std::size_t j=1; j<=c_wr_it->size(); ++j)
327  {
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); /* >= 1*/
331  ++i;
332  }
333  }
334 
335  /* then the poww: for all C_j */
336  for(std::list<std::set<event_idt> >::const_iterator
337  c_ww_it=poww_constraints.begin();
338  c_ww_it!=poww_constraints.end();
339  ++c_ww_it)
340  {
341  /* for all e */
342  for(std::size_t j=1; j<=c_ww_it->size(); ++j)
343  {
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); /* >= 1*/
347  ++i;
348  }
349  }
350 
351  /* then the porw: for all C_j */
352  for(std::list<std::set<event_idt> >::const_iterator
353  c_rw_it=porw_constraints.begin();
354  c_rw_it!=porw_constraints.end();
355  ++c_rw_it)
356  {
357  /* for all e */
358  for(std::size_t j=1; j<=c_rw_it->size(); ++j)
359  {
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); /* >= 1*/
363  ++i;
364  }
365  }
366 
367  /* and finally the porr: for all C_j */
368  for(
369  std::list<std::set<event_idt> >::const_iterator c_rr_it =
370  porr_constraints.begin();
371  c_rr_it!=porr_constraints.end();
372  ++c_rr_it)
373  {
374  /* for all e */
375  for(std::size_t j=1; j<=c_rr_it->size(); ++j)
376  {
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); /* >= 1*/
380  ++i;
381  }
382  }
383 
384  if(model==Power || model==Unknown)
385  {
386  for(std::list<std::set<event_idt> >::const_iterator
387  c_it=com_constraints.begin();
388  c_it!=com_constraints.end();
389  ++c_it)
390  {
391  /* for all e */
392  for(std::size_t j=1; j<=c_it->size(); ++j)
393  {
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); /* >= 1*/
397  ++i;
398  }
399  }
400  }
401 #else
402  throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
403 #endif
404 }
405 
407  ilpt &ilp,
408  unsigned &i,
409  unsigned const_constraints_number,
410  unsigned const_unique)
411 {
412 #ifdef HAVE_GLPK
413  unsigned col=1;
414  unsigned row=1;
415  i=1;
416 
417  /* first, powr constraints: for all C_j */
418  for(std::list<std::set<event_idt> >::const_iterator
419  e_i=powr_constraints.begin();
420  e_i!=powr_constraints.end();
421  ++e_i)
422  {
423  /* for all e */
424  for(std::set<event_idt>::const_iterator
425  e_c_it=e_i->begin();
426  e_c_it!=e_i->end();
427  ++e_c_it)
428  {
429  std::set<unsigned> pt_set;
430  assert(map_to_e.find(*e_c_it)!=map_to_e.end());
431  const_graph_visitor.PT(map_to_e.find(*e_c_it)->second, pt_set);
432  /* sum_e' f_e' */
433  for(col=1; col<=unique*fence_options; ++col)
434  {
435  assert(row<=const_constraints_number);
436  assert(col<=const_unique*fence_options);
437  ilp.imat[i]=row;
438  ilp.jmat[i]=col;
439  if(model==Power || model==Unknown)
440  {
441  if(pt_set.find(col_to_var(col))!=pt_set.end()
442  && col_to_fence(col)==Fence)
443  ilp.vmat[i]=1.0;
444  else
445  ilp.vmat[i]=0.0;
446  }
447  else
448  {
449  if(pt_set.find(col_to_var(col))!=pt_set.end() &&
450  col_to_fence(col)==Fence)
451  ilp.vmat[i]=1.0;
452  else
453  ilp.vmat[i]=0.0;
454  }
455  ++i;
456  }
457  ++row;
458  }
459  }
460 
461  /* then, poww constraints: for all C_j */
462  for(std::list<std::set<event_idt> >::const_iterator
463  e_i=poww_constraints.begin();
464  e_i!=poww_constraints.end();
465  ++e_i)
466  {
467  /* for all e */
468  for(std::set<event_idt>::const_iterator
469  e_nc_it=e_i->begin();
470  e_nc_it!=e_i->end();
471  ++e_nc_it)
472  {
473  std::set<unsigned> pt_set;
474  assert(map_to_e.find(*e_nc_it)!=map_to_e.end());
475  const_graph_visitor.PT(map_to_e.find(*e_nc_it)->second, pt_set);
476  /* sum_e' (f_e' + lwf_e') */
477  for(col=1; col<=unique*fence_options; ++col)
478  {
479  assert(row<=const_constraints_number);
480  assert(col<=const_unique*fence_options);
481  ilp.imat[i]=row;
482  ilp.jmat[i]=col;
483  if(model==Power)
484  {
485  if(pt_set.find(col_to_var(col))!=pt_set.end() &&
486  (col_to_fence(col)==Lwfence || col_to_fence(col)==Fence))
487  ilp.vmat[i]=1.0;
488  else
489  ilp.vmat[i]=0.0;
490  }
491  else
492  {
493  if(pt_set.find(col_to_var(col))!=pt_set.end() &&
494  col_to_fence(col)==Fence)
495  ilp.vmat[i]=1.0;
496  else
497  ilp.vmat[i]=0.0;
498  }
499  ++i;
500  }
501  ++row;
502  }
503  }
504 
505  /* then, porw constraints: for all C_j */
506  for(std::list<std::set<event_idt> >::const_iterator
507  e_i=porw_constraints.begin();
508  e_i!=porw_constraints.end();
509  ++e_i)
510  {
511  /* for all e */
512  for(std::set<event_idt>::const_iterator
513  e_nc_it=e_i->begin();
514  e_nc_it!=e_i->end();
515  ++e_nc_it)
516  {
517  std::set<unsigned> pt_set;
518  assert(map_to_e.find(*e_nc_it)!=map_to_e.end());
519  const_graph_visitor.PT(map_to_e.find(*e_nc_it)->second, pt_set);
520  /* dp_e + sum_e' (f_e' + lwf_e' + br_e') */
521  for(col=1; col<=unique*fence_options; ++col)
522  {
523  assert(row<=const_constraints_number);
524  assert(col<=const_unique*fence_options);
525  ilp.imat[i]=row;
526  ilp.jmat[i]=col;
527  if(model==Power)
528  {
529  if(col==var_fence_to_col(Dp, *e_nc_it) ||
530  (pt_set.find(col_to_var(col))!=pt_set.end() &&
531  (col_to_fence(col)==Lwfence ||
532  col_to_fence(col)==Fence
533 #if 0
534  || col_to_fence(col)==Branching
535 #endif
536  ))) // NOLINT(whitespace/parens)
537  ilp.vmat[i]=1.0;
538  else
539  ilp.vmat[i]=0.0;
540  }
541  else if(model==Unknown)
542  {
543  if(col==var_fence_to_col(Dp, *e_nc_it) ||
544  (pt_set.find(col_to_var(col))!=pt_set.end() &&
545  (col_to_fence(col)==Fence
546 #if 0
547  || col_to_fence(col)==Branching
548 #endif
549  ))) // NOLINT(whitespace/parens)
550  ilp.vmat[i]=1.0;
551  else
552  ilp.vmat[i]=0.0;
553  }
554  else
555  {
556  if(pt_set.find(col_to_var(col))!=pt_set.end() &&
557  (col_to_fence(col)==Fence
558 #if 0
559  || col_to_fence(col)==Branching
560 #endif
561  )) // NOLINT(whitespace/parens)
562  ilp.vmat[i]=1.0;
563  else
564  ilp.vmat[i]=0.0;
565  }
566  ++i;
567  }
568  ++row;
569  }
570  }
571 
572  /* then, porr constraints: for all C_j */
573  for(std::list<std::set<event_idt> >::const_iterator
574  e_i=porr_constraints.begin();
575  e_i!=porr_constraints.end();
576  ++e_i)
577  {
578  /* for all e */
579  for(std::set<event_idt>::const_iterator
580  e_nc_it=e_i->begin();
581  e_nc_it!=e_i->end();
582  ++e_nc_it)
583  {
584  std::set<unsigned> pt_set;
585  assert(map_to_e.find(*e_nc_it)!=map_to_e.end());
586  const_graph_visitor.PT(map_to_e.find(*e_nc_it)->second, pt_set);
587 // uncomment for cf
588 #if 0
589  std::set<unsigned> it_set;
590  IT(map_to_e.find(*e_nc_it)->second, it_set);
591 #endif
592  /* dp_e + sum_e' (f_e' + lwf_e') + sum_e'' cf_e'') */
593  for(col=1; col<=unique*fence_options; ++col)
594  {
595  assert(row<=const_constraints_number);
596  assert(col<=const_unique*fence_options);
597  ilp.imat[i]=row;
598  ilp.jmat[i]=col;
599  if(model==Power)
600  {
601  if(col==var_fence_to_col(Dp, *e_nc_it) ||
602  (pt_set.find(col_to_var(col))!=pt_set.end() &&
603  (col_to_fence(col)==Lwfence || col_to_fence(col)==Fence))
604 #if 0
605  || (it_set.find(col_to_var(col))!=it_set.end()
606  && col_to_fence(col)==Ctlfence)
607 #endif
608  )
609  ilp.vmat[i]=1.0;
610  else
611  ilp.vmat[i]=0.0;
612  }
613  else if(model==Unknown)
614  {
615  if(col==var_fence_to_col(Dp, *e_nc_it) ||
616  (pt_set.find(col_to_var(col))!=pt_set.end() &&
617  (col_to_fence(col)==Fence))
618 #if 0
619  || (it_set.find(col_to_var(col))!=it_set.end()
620  && col_to_fence(col)==Ctlfence)
621 #endif
622  )
623  ilp.vmat[i]=1.0;
624  else
625  ilp.vmat[i]=0.0;
626  }
627  else
628  {
629  if(pt_set.find(col_to_var(col))!=pt_set.end() &&
630  (col_to_fence(col)==Fence))
631  ilp.vmat[i]=1.0;
632  else
633  ilp.vmat[i]=0.0;
634  }
635  ++i;
636  }
637  ++row;
638  }
639  }
640 
641  if(model==Power || model==Unknown)
642  {
643  /* finally, Power/ARM constraints for Rfes: for all C_j */
644  for(std::list<std::set<event_idt> >::const_iterator
645  e_i=com_constraints.begin();
646  e_i!=com_constraints.end();
647  ++e_i)
648  {
649  /* for all e */
650  for(std::set<event_idt>::const_iterator
651  e_c_it=e_i->begin();
652  e_c_it!=e_i->end();
653  ++e_c_it)
654  {
655  unsigned possibilities_met=0;
656 
657  std::set<unsigned> ct_set;
658  assert(invisible_var.map_to_e.find(*e_c_it)!=
659  invisible_var.map_to_e.end());
660  const_graph_visitor.CT(invisible_var.map_to_e.find(*e_c_it)->second,
661  ct_set);
662 
663  std::set<unsigned> ct_not_powr_set;
665  *e_c_it)->second, ct_not_powr_set);
666 
667  instrumenter.message.statistics() << "size of CT for "
668  << invisible_var.map_to_e.find(*e_c_it)->second.first << ","
669  << invisible_var.map_to_e.find(*e_c_it)->second.second << ": "
670  << ct_set.size() << messaget::eom;
671 
672  /* sum_e' f_e' + sum_e'' lwf_e'' */
673  for(col=1; col<=unique*fence_options; ++col)
674  {
675  assert(row<=const_constraints_number);
676  assert(col<=const_unique*fence_options);
677  ilp.imat[i]=row;
678  ilp.jmat[i]=col;
679  if((ct_set.find(col_to_var(col))!=ct_set.end() &&
680  col_to_fence(col)==Fence) ||
681  (ct_not_powr_set.find(col_to_var(col))!=ct_not_powr_set.end() &&
682  col_to_fence(col)==Lwfence))
683  {
684  ilp.vmat[i]=1.0;
685  ++possibilities_met;
686  }
687  else
688  ilp.vmat[i]=0.0;
689  ++i;
690  }
691  ++row;
692  assert(possibilities_met);
693  }
694  }
695  }
696  instrumenter.message.debug() << "3: " << i << " row: " << row
697  << messaget::eom;
698 #else
699  throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
700 #endif
701 }
702 
704 {
705 #ifdef HAVE_GLPK
706  ilpt ilp;
707 
708  instrumenter.message.statistics() << "po^+ edges considered:"
709  << unique << " cycles:" << instrumenter.set_of_cycles.size()
710  << messaget::eom;
711 
712  /* sets the variables and coefficients */
713  // nb of po+ considered * types of fences (_e)
714  unsigned i=1;
715  mip_set_var(ilp, i);
716 
717  /* sets the constraints */
718  mip_set_cst(ilp, i);
719 
720  instrumenter.message.debug() << "3: " << i << messaget::eom;
721  assert(i-1==constraints_number);
722 
723  const std::size_t const_constraints_number=constraints_number;
724  const unsigned const_unique=unique;
725 
726  const std::size_t mat_size=
727  // NOLINTNEXTLINE(whitespace/operators)
728  const_unique*fence_options*const_constraints_number;
729  instrumenter.message.statistics() << "size of the system: " << mat_size
730  << messaget::eom;
731  instrumenter.message.statistics() << "# of constraints: "
732  << const_constraints_number << messaget::eom;
733  instrumenter.message.statistics() << "# of variables: "
734  << const_unique*fence_options << messaget::eom;
735 
736  ilp.set_size(mat_size);
737 
738 #ifdef DEBUG
739  print_vars();
740 #endif
741 
742  /* fills the constraints coeff */
743  /* tables read from 1 in glpk -- first row/column ignored */
744  mip_fill_matrix(ilp, i, const_constraints_number, const_unique);
745 
746  instrumenter.message.statistics() << "i: " << i << " mat_size: " << mat_size
747  << messaget::eom;
748  // assert(i-1==mat_size);
749 
750 #ifdef DEBUG
751  for(i=1; i<=mat_size; ++i)
752  instrumenter.message.debug() << i << "[" << ilp.imat[i] << ","
753  << ilp.jmat[i] << "]=" << ilp.vmat[i] << messaget::eom;
754 #endif
755 
756  /* solves MIP by branch-and-cut */
757  ilp.solve();
758 
759 #ifdef DEBUG
760  print_vars();
761 #endif
762 
763  /* checks optimality */
764  switch(glp_mip_status(ilp.lp))
765  {
766  case GLP_OPT:
767  instrumenter.message.result() << "Optimal solution found"
768  << messaget::eom;
769  break;
770  case GLP_UNDEF:
771  instrumenter.message.result() << "Solution undefined" << messaget::eom;
772  assert(0);
773  case GLP_FEAS:
774  instrumenter.message.result() << "Solution feasible, "
775  << "yet not proven optimal, "
776  << "due to early termination"
777  << messaget::eom;
778  break;
779  case GLP_NOFEAS:
781  << "No feasible solution, the system is UNSAT" << messaget::eom;
782  assert(0);
783  }
784 
786 
787  /* loads results (x_i) */
788  instrumenter.message.statistics() << "minimal cost: "
789  << glp_mip_obj_val(ilp.lp) << messaget::eom;
790  for(unsigned j=1; j<=const_unique*fence_options; ++j)
791  {
792  if(glp_mip_col_val(ilp.lp, j)>=1)
793  {
794  /* insert that fence */
795  assert(map_to_e.find(col_to_var(j))!=map_to_e.end());
796  const edget &delay=map_to_e.find(col_to_var(j))->second;
797  instrumenter.message.statistics() << delay.first << " -> "
798  << delay.second << " : " << to_string(col_to_fence(j))
799  << messaget::eom;
800  instrumenter.message.statistics() << "(between "
801  << egraph[delay.first].source_location << " and "
802  << egraph[delay.second].source_location << messaget::eom;
803  fenced_edges.insert(
804  std::pair<edget, fence_typet>(delay, col_to_fence(j)));
805  }
806  }
807 #else
808  throw "sorry, musketeer requires glpk; please recompile musketeer with glpk";
809 #endif
810 }
811 
813 {
814  /* TODO */
815 }
816 
818 {
819  /* removes redundant (due to several call to the same fenced function) */
820  std::set<std::string> non_redundant_display;
821  for(std::map<edget, fence_typet>::const_iterator it=fenced_edges.begin();
822  it!=fenced_edges.end();
823  ++it)
824  {
825  std::ostringstream s;
826  const abstract_eventt &first=instrumenter.egraph[it->first.first];
827 
828  s << to_string(it->second) << "|" << first.source_location.get_file()
829  << "|" << first.source_location.get_line() << "|"
830  << first.source_location.get_column() << '\n';
831  non_redundant_display.insert(s.str());
832  }
833 
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();
838  ++it)
839  results << *it;
840  results.close();
841 }
842 
843 /* prints final results */
845 {
846  /* removes redundant (due to several call to the same fenced function) */
847  std::set<std::string> non_redundant_display;
848  for(std::map<edget, fence_typet>::const_iterator it=fenced_edges.begin();
849  it!=fenced_edges.end();
850  ++it)
851  {
852  std::ostringstream s;
853  const abstract_eventt &first=instrumenter.egraph[it->first.first];
854  const abstract_eventt &second=instrumenter.egraph[it->first.second];
855 
856  s << to_string(it->second) << "|" << first.source_location.get_file()
857  << "|" << first.source_location.get_line() << "|"
858  << second.source_location.get_file()
859  << "|" << second.source_location.get_line() << '\n';
860  non_redundant_display.insert(s.str());
861  }
862 
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();
867  ++it)
868  results << *it;
869  results.close();
870 }
871 
872 /* prints final results */
874 {
875  /* removes redundant (due to several call to the same fenced function) */
876  std::set<std::string> non_redundant_display;
877  for(std::map<edget, fence_typet>::const_iterator it=fenced_edges.begin();
878  it!=fenced_edges.end();
879  ++it)
880  {
881  std::ostringstream s;
882  const abstract_eventt &first=instrumenter.egraph[it->first.first];
883  const abstract_eventt &second=instrumenter.egraph[it->first.second];
884 
885  try
886  {
887  s << to_string(it->second) << "|" << first.source_location.get_file()
888  << "|" << first.source_location.get_function() << "|"
889  << first.source_location.get_line() << "|" << first.variable << "|"
890  << second.source_location.get_file() << "|"
891  << second.source_location.get_function() << "|"
892  << second.source_location.get_line()
893  << "|" << second.variable << '\n';
894  non_redundant_display.insert(s.str());
895  }
896  catch(std::string s)
897  {
899  << "Couldn't retrieve symbols of variables " << first.variable
900  << " and " << second.variable << " due to " << s << messaget::eom;
901  }
902  }
903 
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();
908  ++it)
909  results << *it;
910  results.close();
911 }
912 
913 /* prints final results */
915 {
916  /* removes redundant (due to several call to the same fenced function) */
917  std::set<std::string> non_redundant_display;
918  for(std::map<edget, fence_typet>::const_iterator it=fenced_edges.begin();
919  it!=fenced_edges.end();
920  ++it)
921  {
922  std::ostringstream s;
923  const abstract_eventt &first=instrumenter.egraph[it->first.first];
924  const abstract_eventt &second=instrumenter.egraph[it->first.second];
925 
926  try
927  {
928  s << to_string(it->second) << "|" << first.source_location.get_file()
929  << "|" << first.source_location.get_function() << "|"
930  << first.source_location.get_line()
931  << "|" << first.variable << "|"
932  << get_type(first.variable).get("#c_type") << "|"
933  << second.source_location.get_file() << "|"
934  << second.source_location.get_function() << "|"
935  << second.source_location.get_line()
936  << "|" << second.variable << "|"
937  << get_type(second.variable).get("#c_type") << '\n';
938  non_redundant_display.insert(s.str());
939  }
940  catch (std::string s)
941  {
943  << "Couldn't retrieve types of variables " << first.variable
944  << " and " << second.variable << " due to " << s << messaget::eom;
945  }
946  }
947 
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();
952  ++it)
953  results << *it;
954  results.close();
955 }
956 
958 {
959  switch(f)
960  {
961  case Fence: return "fence";
962  case Lwfence: return "lwfence";
963  case Dp: return "dp";
964  case Branching: return "branching";
965  case Ctlfence: return "ctlfence";
966  }
967  assert(0);
968 }
969 
970 inline unsigned fence_insertert::col_to_var(unsigned u) const
971 {
972  return (u-u%fence_options)/fence_options+(u%fence_options!=0?1:0);
973 }
974 
976  const
977 {
978  switch(u%fence_options)
979  {
980  case 0: return Fence;
981  case 1: return Dp;
982  case 2: return Lwfence;
983  case 3: return Branching;
984  case 4: return Ctlfence;
985  }
986  assert(0);
987 }
988 
989 inline unsigned fence_insertert::var_fence_to_col(fence_typet f, unsigned var)
990  const
991 {
992  switch(f)
993  {
994  case Fence: return var*fence_options;
995  case Dp: return (var-1)*fence_options+1;
996  case Lwfence: return (var-1)*fence_options+2;
997  case Branching: return (var-1)*fence_options+3;
998  case Ctlfence: return (var-1)*fence_options+4;
999  }
1000  assert(0);
1001 }
1002 
1004 {
1005  switch(model)
1006  {
1007  case TSO:
1008  case PSO:
1009  case RMO:
1010  fence_options=1; // 2: f, br
1011  break;
1012  case Power:
1013  fence_options=3; // 5: f, lwf, dp, cf, br
1014  break;
1015  case Unknown: /* including ARM */
1016  fence_options=2; // 4: f, dp, cf, br
1017  break;
1018  }
1019 }
1020 
1022 {
1024  << "---- pos/pos+ (visible) variables ----" << messaget::eom;
1025  for(std::map<edget, unsigned>::const_iterator it=map_from_e.begin();
1026  it!=map_from_e.end(); ++it)
1027  instrumenter.message.statistics() << it->first.first << ","
1028  << it->first.second << messaget::eom;
1029  instrumenter.message.statistics() << "---- cmp (invisible) variables ----"
1030  << messaget::eom;
1031  for(std::map<edget, unsigned>::const_iterator it=
1032  invisible_var.map_from_e.begin();
1033  it!=invisible_var.map_from_e.end(); ++it)
1034  instrumenter.message.statistics() << it->first.first << ","
1035  << it->first.second << messaget::eom;
1036  instrumenter.message.statistics() << "-----------------------------------"
1037  << messaget::eom;
1038 }
1039 
1041 {
1042  std::string copy=id2string(id);
1043  /* if we picked an array, removes [] that rw_set added */
1044  if(copy.find("[]")!=std::string::npos)
1045  copy=copy.substr(0, copy.find_last_of("[]")-1);
1046  try
1047  {
1048  return instrumenter.ns.lookup(copy).type;
1049  }
1050  catch(...)
1051  {
1052  std::list<std::string> fields;
1053  std::string current;
1054 
1055  /* collects the consecutive fields */
1056  std::string::const_iterator it=copy.begin();
1057  std::string::const_iterator next=it;
1058  for(; it!=copy.end(); ++it)
1059  {
1060  next=it;
1061  ++next;
1062  if(!(*it=='.' || (next!=copy.end() && *it=='-' && *next=='>')))
1063  {
1064  current+=*it;
1065  instrumenter.message.debug() << current << messaget::eom;
1066  }
1067  else
1068  {
1069  fields.push_back(current);
1070  current.clear();
1071  if(*it!='.')
1072  ++it;
1073  /* safe as next!=copy.end() */
1074  assert(next!=copy.end());
1075  }
1076  }
1077 
1078  /* retrieves the type of the accessed field */
1079  typet field=type_component(fields.begin(), fields.end(),
1080  instrumenter.ns.lookup(fields.front()).type);
1081  return field;
1082  }
1083 }
1084 
1086  std::list<std::string>::const_iterator it,
1087  std::list<std::string>::const_iterator end,
1088  const typet &type)
1089 {
1090  if(it==end)
1091  return type;
1092 
1093  if(type.id()==ID_struct)
1094  {
1095  const struct_union_typet &str=to_struct_union_type(type);
1096  typet comp_type=str.component_type(*it);
1097  ++it;
1098  return type_component(it, end, comp_type);
1099  }
1100 
1101  if(type.id()==ID_symbol)
1102  {
1103  return type;
1104  }
1105 
1106  assert(0);
1107 }
std::map< unsigned, edget > & map_to_e
normal variables used almost every time
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
std::map< edget, unsigned > & map_from_e
mstreamt & result()
Definition: message.h:233
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Definition: ilp.h:78
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
messaget & message
Definition: goto2graph.h:280
std::string to_string(fence_typet f) const
void print_vars() const
mstreamt & status()
Definition: message.h:238
unsigned col_to_var(unsigned u) const
const bool with_freq
virtual void process_cycles_selection()
Definition: wmm.h:23
const irep_idt & get_function() const
std::list< std::set< event_idt > > powr_constraints
Definition: wmm.h:22
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void CT_not_powr(const edget &e, std::set< unsigned > &edges)
typet get_type(const irep_idt &id)
ILP structure.
namespacet ns
Definition: goto2graph.h:37
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.
Definition: std_types.h:277
unsigned fence_options
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
Definition: irep.h:189
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
Definition: irep.cpp:213
fence_typet col_to_fence(unsigned u) const
virtual unsigned fence_cost(fence_typet e) const
Definition: wmm.h:21
const float epsilon
virtual bool filter_cycles(unsigned cycle_id) const
typet component_type(const irep_idt &component_name) const
Definition: std_types.cpp:68
mstreamt & statistics()
Definition: message.h:243
std::set< event_idt > po
std::list< std::set< event_idt > > porr_constraints
A Template Class for Graphs.
mstreamt & debug()
Definition: message.h:253
unsigned & unique
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.
Definition: std_types.h:159
Definition: wmm.h:19
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
mip_vart invisible_var
Definition: wmm.h:20
event_grapht egraph
Definition: goto2graph.h:283
source_locationt source_location
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:289
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