cprover
instrumenter_strategies.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Strategies for picking the abstract events to instrument
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #include "goto2graph.h"
15 
16 #include <string>
17 #include <fstream>
18 
19 #ifdef HAVE_GLPK
20 #include <glpk.h>
21 #include <cstdlib>
22 #endif
23 
25 {
26  var_to_instr.clear();
27  id2loc.clear();
28  id2cycloc.clear();
29 
30  if(!set_of_cycles.empty())
31  {
32  switch(strategy)
33  {
34  case all:
36  break;
39  break;
40  case min_interference:
42  break;
43  case read_first:
45  break;
46  case write_first:
48  break;
49  case my_events:
50  assert(false);
51  }
52  }
53  else if(num_sccs!=0)
54  {
55  for(std::size_t i=0; i<num_sccs; ++i)
56  {
57  switch(strategy)
58  {
59  case all:
61  break;
64  break;
65  case min_interference:
67  break;
68  case read_first:
70  break;
71  case write_first:
73  break;
74  case my_events:
75  assert(false);
76  }
77  }
78  }
79  else
80  message.debug() << "no cycles to instrument" << messaget::eom;
81 }
82 
84  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
85 {
86  for(std::set<event_grapht::critical_cyclet>::const_iterator
87  it=(set_of_cycles).begin();
88  it!=(set_of_cycles).end(); ++it)
89  {
90  for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator
91  p_it=it->unsafe_pairs.begin();
92  p_it!=it->unsafe_pairs.end(); ++p_it)
93  {
94  const abstract_eventt &first_ev=egraph[p_it->first];
95  var_to_instr.insert(first_ev.variable);
96  id2loc.insert(
97  std::pair<irep_idt, source_locationt>(
98  first_ev.variable, first_ev.source_location));
99  if(!p_it->is_po)
100  {
101  const abstract_eventt &second_ev = egraph[p_it->second];
102  var_to_instr.insert(second_ev.variable);
103  id2loc.insert(
104  std::pair<irep_idt, source_locationt>(
105  second_ev.variable, second_ev.source_location));
106  }
107  }
108  }
109 }
110 
112  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
113 {
114  /* to keep track of the delayed pair, and to avoid the instrumentation
115  of two pairs in a same cycle */
116  std::set<event_grapht::critical_cyclet::delayt> delayed;
117 
118  for(std::set<event_grapht::critical_cyclet>::iterator
119  it=set_of_cycles.begin();
120  it!=set_of_cycles.end(); ++it)
121  {
122  /* cycle with already a delayed pair? */
123  bool next=false;
124  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
125  p_it=it->unsafe_pairs.begin();
126  p_it!=it->unsafe_pairs.end(); ++p_it)
127  {
128  if(delayed.find(*p_it)!=delayed.end())
129  {
130  next=true;
131  break;
132  }
133  }
134 
135  if(next)
136  continue;
137 
138  /* instruments the first pair */
139  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
140  p_it=it->unsafe_pairs.begin();
141  p_it!=it->unsafe_pairs.end(); ++p_it)
142  {
143  delayed.insert(*p_it);
144  const abstract_eventt &first_ev=egraph[p_it->first];
145  var_to_instr.insert(first_ev.variable);
146  id2loc.insert(
147  std::pair<irep_idt, source_locationt>(
148  first_ev.variable, first_ev.source_location));
149  if(!p_it->is_po)
150  {
151  const abstract_eventt &second_ev=egraph[p_it->second];
152  var_to_instr.insert(second_ev.variable);
153  id2loc.insert(
154  std::pair<irep_idt, source_locationt>(
155  second_ev.variable, second_ev.source_location));
156  }
157  break;
158  }
159  }
160 }
161 
163  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
164 {
165  /* TODO */
166  throw "read first strategy not implemented yet";
167 }
168 
170  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
171 {
172  /* TODO */
173  throw "write first strategy not implemented yet";
174 }
175 
177 unsigned inline instrumentert::cost(
179 {
180  /* cost(poW*)=1
181  cost(poRW)=cost(rfe)=2
182  cost(poRR)=3 */
184  return 1;
185  else if(egraph[e.second].operation==abstract_eventt::operationt::Write
186  || !e.is_po)
187  return 2;
188  else
189  return 3;
190 }
191 
193  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
194 {
195  /* Idea:
196  We solve this by a linear programming approach,
197  using for instance glpk lib.
198 
199  Input: the edges to instrument E, the cycles C_j
200  Pb: min sum_{e_i in E} d(e_i).x_i
201  s.t. for all j, sum_{e_i in C_j} >= 1,
202  where e_i is a pair to potentially instrument,
203  x_i is a Boolean stating whether we instrument
204  e_i, and d() is the cost of an instrumentation.
205  Output: the x_i, saying which pairs to instrument
206 
207  For this instrumentation, we propose:
208  d(poW*)=1
209  d(poRW)=d(rfe)=2
210  d(poRR)=3
211 
212  This function can be refined with the actual times
213  we get in experimenting the different pairs in a
214  single IRIW.
215  */
216 
217 #ifdef HAVE_GLPK
218  /* first, identify all the unsafe pairs */
219  std::set<event_grapht::critical_cyclet::delayt> edges;
220  for(std::set<event_grapht::critical_cyclet>::iterator
221  C_j=set_of_cycles.begin();
222  C_j!=set_of_cycles.end();
223  ++C_j)
224  for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator e_i=
225  C_j->unsafe_pairs.begin();
226  e_i!=C_j->unsafe_pairs.end();
227  ++e_i)
228  edges.insert(*e_i);
229 
230  glp_prob *lp;
231  glp_iocp parm;
232  glp_init_iocp(&parm);
233  parm.msg_lev=GLP_MSG_OFF;
234  parm.presolve=GLP_ON;
235 
236  lp=glp_create_prob();
237  glp_set_prob_name(lp, "instrumentation optimisation");
238  glp_set_obj_dir(lp, GLP_MIN);
239 
240  message.debug() << "edges: "<<edges.size()<<" cycles:"<<set_of_cycles.size()
241  << messaget::eom;
242 
243  /* sets the variables and coefficients */
244  glp_add_cols(lp, edges.size());
245  std::size_t i=0;
246  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
247  e_i=edges.begin();
248  e_i!=edges.end();
249  ++e_i)
250  {
251  ++i;
252  std::string name="e_"+std::to_string(i);
253  glp_set_col_name(lp, i, name.c_str());
254  glp_set_col_bnds(lp, i, GLP_LO, 0.0, 0.0);
255  glp_set_obj_coef(lp, i, cost(*e_i));
256  glp_set_col_kind(lp, i, GLP_BV);
257  }
258 
259  /* sets the constraints (soundness): one per cycle */
260  glp_add_rows(lp, set_of_cycles.size());
261  i=0;
262  for(std::set<event_grapht::critical_cyclet>::iterator
263  C_j=set_of_cycles.begin();
264  C_j!=set_of_cycles.end();
265  ++C_j)
266  {
267  ++i;
268  std::string name="C_"+std::to_string(i);
269  glp_set_row_name(lp, i, name.c_str());
270  glp_set_row_bnds(lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/
271  }
272 
273  const std::size_t mat_size=set_of_cycles.size()*edges.size();
274  message.debug() << "size of the system: " << mat_size
275  << messaget::eom;
276  int *imat=new int[mat_size+1];
277  int *jmat=new int[mat_size+1];
278  double *vmat=new double[mat_size+1];
279 
280  /* fills the constraints coeff */
281  /* tables read from 1 in glpk -- first row/column ignored */
282  std::size_t col=1;
283  std::size_t row=1;
284  i=1;
285  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
286  e_i=edges.begin();
287  e_i!=edges.end();
288  ++e_i)
289  {
290  row=1;
291  for(std::set<event_grapht::critical_cyclet>::iterator
292  C_j=set_of_cycles.begin();
293  C_j!=set_of_cycles.end();
294  ++C_j)
295  {
296  imat[i]=row;
297  jmat[i]=col;
298  if(C_j->unsafe_pairs.find(*e_i)!=C_j->unsafe_pairs.end())
299  vmat[i]=1.0;
300  else
301  vmat[i]=0.0;
302  ++i;
303  ++row;
304  }
305  ++col;
306  }
307 
308 #ifdef DEBUG
309  for(i=1; i<=mat_size; ++i)
310  message.statistics() <<i<<"["<<imat[i]<<","<<jmat[i]<<"]="<<vmat[i]
311  << messaget::eom;
312 #endif
313 
314  /* solves MIP by branch-and-cut */
315  glp_load_matrix(lp, mat_size, imat, jmat, vmat);
316  glp_intopt(lp, &parm);
317 
318  /* loads results (x_i) */
319  message.statistics() << "minimal cost: " << glp_mip_obj_val(lp)
320  << messaget::eom;
321  i=0;
322  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
323  e_i=edges.begin();
324  e_i!=edges.end();
325  ++e_i)
326  {
327  ++i;
328  if(glp_mip_col_val(lp, i)>=1)
329  {
330  const abstract_eventt &first_ev=egraph[e_i->first];
331  var_to_instr.insert(first_ev.variable);
332  id2loc.insert(
333  std::pair<irep_idt, source_locationt>(
334  first_ev.variable, first_ev.source_location));
335  if(!e_i->is_po)
336  {
337  const abstract_eventt &second_ev=egraph[e_i->second];
338  var_to_instr.insert(second_ev.variable);
339  id2loc.insert(
340  std::pair<irep_idt, source_locationt>(
341  second_ev.variable, second_ev.source_location));
342  }
343  }
344  }
345 
346  glp_delete_prob(lp);
347  delete[] imat;
348  delete[] jmat;
349  delete[] vmat;
350 #else
351  throw "sorry, minimum interference option requires glpk; "
352  "please recompile goto-instrument with glpk";
353 #endif
354 }
355 
357  const std::set<event_grapht::critical_cyclet> &set,
358  const std::set<event_idt> &my_events)
359 {
360  for(std::set<event_grapht::critical_cyclet>::const_iterator
361  it=set.begin();
362  it!=set.end(); ++it)
363  {
364  for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator
365  p_it=it->unsafe_pairs.begin();
366  p_it!=it->unsafe_pairs.end(); ++p_it)
367  {
368  if(my_events.find(p_it->first)!=my_events.end())
369  {
370  const abstract_eventt &first_ev=egraph[p_it->first];
371  var_to_instr.insert(first_ev.variable);
372  id2loc.insert(
373  std::pair<irep_idt, source_locationt>(
374  first_ev.variable, first_ev.source_location));
375  if(!p_it->is_po && my_events.find(p_it->second)!=my_events.end())
376  {
377  const abstract_eventt &second_ev=egraph[p_it->second];
378  var_to_instr.insert(second_ev.variable);
379  id2loc.insert(
380  std::pair<irep_idt, source_locationt>(second_ev.variable,
381  second_ev.source_location));
382  }
383  }
384  }
385  }
386 }
387 
389  const std::set<event_idt> &my_events)
390 {
391  var_to_instr.clear();
392  id2loc.clear();
393  id2cycloc.clear();
394 
395  if(!set_of_cycles.empty())
397  else if(num_sccs!=0)
398  {
399  for(std::size_t i=0; i<num_sccs; ++i)
401  }
402  else
403  message.debug() << "no cycles to instrument" << messaget::eom;
404 }
405 
406 std::set<event_idt> instrumentert::extract_my_events()
407 {
408  std::ifstream file;
409  file.open("inst.evt");
410  std::set<event_idt> this_set;
411 
412  std::size_t size;
413  file >> size;
414 
415  std::size_t tmp;
416 
417  for(std::size_t i=0; i<size; i++)
418  {
419  file >> tmp;
420  this_set.insert(tmp);
421  }
422 
423  file.close();
424 
425  return this_set;
426 }
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:327
instrumentation_strategyt
Definition: wmm.h:26
messaget & message
Definition: goto2graph.h:280
unsigned cost(const event_grapht::critical_cyclet::delayt &e)
cost function
void instrument_my_events_inserter(const set_of_cyclest &set, const std::set< event_idt > &events)
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
Definition: wmm.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void instrument_my_events(const std::set< event_idt > &events)
unsigned num_sccs
Definition: goto2graph.h:293
Instrumenter.
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:328
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:329
void instrument_with_strategy(instrumentation_strategyt strategy)
mstreamt & statistics()
Definition: message.h:243
void instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)
Definition: wmm.h:32
mstreamt & debug()
Definition: message.h:253
void instrument_all_inserter(const set_of_cyclest &set)
static std::set< event_idt > extract_my_events()
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
event_grapht egraph
Definition: goto2graph.h:283
source_locationt source_location
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:289
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:292
Definition: wmm.h:28
Definition: kdev_t.h:19