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  if(!it->unsafe_pairs.empty())
140  {
141  std::set<event_grapht::critical_cyclet::delayt>::iterator
142  p_it=it->unsafe_pairs.begin();
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  }
158  }
159 }
160 
162  const std::set<event_grapht::critical_cyclet> &)
163 {
164  /* TODO */
165  throw "read first strategy not implemented yet";
166 }
167 
169  const std::set<event_grapht::critical_cyclet> &)
170 {
171  /* TODO */
172  throw "write first strategy not implemented yet";
173 }
174 
176 unsigned inline instrumentert::cost(
178 {
179  /* cost(poW*)=1
180  cost(poRW)=cost(rfe)=2
181  cost(poRR)=3 */
183  return 1;
184  else if(egraph[e.second].operation==abstract_eventt::operationt::Write
185  || !e.is_po)
186  return 2;
187  else
188  return 3;
189 }
190 
192  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
193 {
194  /* Idea:
195  We solve this by a linear programming approach,
196  using for instance glpk lib.
197 
198  Input: the edges to instrument E, the cycles C_j
199  Pb: min sum_{e_i in E} d(e_i).x_i
200  s.t. for all j, sum_{e_i in C_j} >= 1,
201  where e_i is a pair to potentially instrument,
202  x_i is a Boolean stating whether we instrument
203  e_i, and d() is the cost of an instrumentation.
204  Output: the x_i, saying which pairs to instrument
205 
206  For this instrumentation, we propose:
207  d(poW*)=1
208  d(poRW)=d(rfe)=2
209  d(poRR)=3
210 
211  This function can be refined with the actual times
212  we get in experimenting the different pairs in a
213  single IRIW.
214  */
215 
216 #ifdef HAVE_GLPK
217  /* first, identify all the unsafe pairs */
218  std::set<event_grapht::critical_cyclet::delayt> edges;
219  for(std::set<event_grapht::critical_cyclet>::iterator
220  C_j=set_of_cycles.begin();
221  C_j!=set_of_cycles.end();
222  ++C_j)
223  for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator e_i=
224  C_j->unsafe_pairs.begin();
225  e_i!=C_j->unsafe_pairs.end();
226  ++e_i)
227  edges.insert(*e_i);
228 
229  glp_prob *lp;
230  glp_iocp parm;
231  glp_init_iocp(&parm);
232  parm.msg_lev=GLP_MSG_OFF;
233  parm.presolve=GLP_ON;
234 
235  lp=glp_create_prob();
236  glp_set_prob_name(lp, "instrumentation optimisation");
237  glp_set_obj_dir(lp, GLP_MIN);
238 
239  message.debug() << "edges: "<<edges.size()<<" cycles:"<<set_of_cycles.size()
240  << messaget::eom;
241 
242  /* sets the variables and coefficients */
243  glp_add_cols(lp, edges.size());
244  std::size_t i=0;
245  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
246  e_i=edges.begin();
247  e_i!=edges.end();
248  ++e_i)
249  {
250  ++i;
251  std::string name="e_"+std::to_string(i);
252  glp_set_col_name(lp, i, name.c_str());
253  glp_set_col_bnds(lp, i, GLP_LO, 0.0, 0.0);
254  glp_set_obj_coef(lp, i, cost(*e_i));
255  glp_set_col_kind(lp, i, GLP_BV);
256  }
257 
258  /* sets the constraints (soundness): one per cycle */
259  glp_add_rows(lp, set_of_cycles.size());
260  i=0;
261  for(std::set<event_grapht::critical_cyclet>::iterator
262  C_j=set_of_cycles.begin();
263  C_j!=set_of_cycles.end();
264  ++C_j)
265  {
266  ++i;
267  std::string name="C_"+std::to_string(i);
268  glp_set_row_name(lp, i, name.c_str());
269  glp_set_row_bnds(lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/
270  }
271 
272  const std::size_t mat_size=set_of_cycles.size()*edges.size();
273  message.debug() << "size of the system: " << mat_size
274  << messaget::eom;
275  std::vector<int> imat(mat_size+1);
276  std::vector<int> jmat(mat_size+1);
277  std::vector<double> vmat(mat_size+1);
278 
279  /* fills the constraints coeff */
280  /* tables read from 1 in glpk -- first row/column ignored */
281  std::size_t col=1;
282  std::size_t row=1;
283  i=1;
284  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
285  e_i=edges.begin();
286  e_i!=edges.end();
287  ++e_i)
288  {
289  row=1;
290  for(std::set<event_grapht::critical_cyclet>::iterator
291  C_j=set_of_cycles.begin();
292  C_j!=set_of_cycles.end();
293  ++C_j)
294  {
295  imat[i]=row;
296  jmat[i]=col;
297  if(C_j->unsafe_pairs.find(*e_i)!=C_j->unsafe_pairs.end())
298  vmat[i]=1.0;
299  else
300  vmat[i]=0.0;
301  ++i;
302  ++row;
303  }
304  ++col;
305  }
306 
307 #ifdef DEBUG
308  for(i=1; i<=mat_size; ++i)
309  message.statistics() <<i<<"["<<imat[i]<<","<<jmat[i]<<"]="<<vmat[i]
310  << messaget::eom;
311 #endif
312 
313  /* solves MIP by branch-and-cut */
314  glp_load_matrix(lp, mat_size, imat.data(), jmat.data(), vmat.data());
315  glp_intopt(lp, &parm);
316 
317  /* loads results (x_i) */
318  message.statistics() << "minimal cost: " << glp_mip_obj_val(lp)
319  << messaget::eom;
320  i=0;
321  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
322  e_i=edges.begin();
323  e_i!=edges.end();
324  ++e_i)
325  {
326  ++i;
327  if(glp_mip_col_val(lp, i)>=1)
328  {
329  const abstract_eventt &first_ev=egraph[e_i->first];
330  var_to_instr.insert(first_ev.variable);
331  id2loc.insert(
332  std::pair<irep_idt, source_locationt>(
333  first_ev.variable, first_ev.source_location));
334  if(!e_i->is_po)
335  {
336  const abstract_eventt &second_ev=egraph[e_i->second];
337  var_to_instr.insert(second_ev.variable);
338  id2loc.insert(
339  std::pair<irep_idt, source_locationt>(
340  second_ev.variable, second_ev.source_location));
341  }
342  }
343  }
344 
345  glp_delete_prob(lp);
346 #else
347  throw "sorry, minimum interference option requires glpk; "
348  "please recompile goto-instrument with glpk";
349 #endif
350 }
351 
353  const std::set<event_grapht::critical_cyclet> &set,
354  const std::set<event_idt> &my_events)
355 {
356  for(std::set<event_grapht::critical_cyclet>::const_iterator
357  it=set.begin();
358  it!=set.end(); ++it)
359  {
360  for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator
361  p_it=it->unsafe_pairs.begin();
362  p_it!=it->unsafe_pairs.end(); ++p_it)
363  {
364  if(my_events.find(p_it->first)!=my_events.end())
365  {
366  const abstract_eventt &first_ev=egraph[p_it->first];
367  var_to_instr.insert(first_ev.variable);
368  id2loc.insert(
369  std::pair<irep_idt, source_locationt>(
370  first_ev.variable, first_ev.source_location));
371  if(!p_it->is_po && my_events.find(p_it->second)!=my_events.end())
372  {
373  const abstract_eventt &second_ev=egraph[p_it->second];
374  var_to_instr.insert(second_ev.variable);
375  id2loc.insert(
376  std::pair<irep_idt, source_locationt>(second_ev.variable,
377  second_ev.source_location));
378  }
379  }
380  }
381  }
382 }
383 
385  const std::set<event_idt> &my_events)
386 {
387  var_to_instr.clear();
388  id2loc.clear();
389  id2cycloc.clear();
390 
391  if(!set_of_cycles.empty())
393  else if(num_sccs!=0)
394  {
395  for(std::size_t i=0; i<num_sccs; ++i)
397  }
398  else
399  message.debug() << "no cycles to instrument" << messaget::eom;
400 }
401 
402 std::set<event_idt> instrumentert::extract_my_events()
403 {
404  std::ifstream file;
405  file.open("inst.evt");
406  std::set<event_idt> this_set;
407 
408  std::size_t size;
409  file >> size;
410 
411  std::size_t tmp;
412 
413  for(std::size_t i=0; i<size; i++)
414  {
415  file >> tmp;
416  this_set.insert(tmp);
417  }
418 
419  file.close();
420 
421  return this_set;
422 }
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:323
instrumentation_strategyt
Definition: wmm.h:26
messaget & message
Definition: goto2graph.h:276
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:272
void instrument_my_events(const std::set< event_idt > &events)
unsigned num_sccs
Definition: goto2graph.h:289
Instrumenter.
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:324
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:325
void instrument_with_strategy(instrumentation_strategyt strategy)
void instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)
Definition: wmm.h:32
void instrument_all_inserter(const set_of_cyclest &set)
static std::set< event_idt > extract_my_events()
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
event_grapht egraph
Definition: goto2graph.h:279
source_locationt source_location
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:285
mstreamt & debug() const
Definition: message.h:332
mstreamt & statistics() const
Definition: message.h:322
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:288
Definition: wmm.h:28
Definition: kdev_t.h:19