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