CBMC
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 <fstream>
17 
18 #ifdef HAVE_GLPK
19 #include <glpk.h>
20 #include <cstdlib>
21 #endif
22 
24 {
25  var_to_instr.clear();
26  id2loc.clear();
27  id2cycloc.clear();
28 
29  if(!set_of_cycles.empty())
30  {
31  switch(strategy)
32  {
33  case all:
35  break;
38  break;
39  case min_interference:
41  break;
42  case read_first:
44  break;
45  case write_first:
47  break;
48  case my_events:
50  }
51  }
52  else if(num_sccs!=0)
53  {
54  for(std::size_t i=0; i<num_sccs; ++i)
55  {
56  switch(strategy)
57  {
58  case all:
60  break;
63  break;
64  case min_interference:
66  break;
67  case read_first:
69  break;
70  case write_first:
72  break;
73  case my_events:
75  }
76  }
77  }
78  else
79  message.debug() << "no cycles to instrument" << messaget::eom;
80 }
81 
83  const std::set<event_grapht::critical_cyclet> &subset_of_cycles)
84 {
85  for(std::set<event_grapht::critical_cyclet>::const_iterator it =
86  subset_of_cycles.begin();
87  it != subset_of_cycles.end();
88  ++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> &subset_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 it =
119  subset_of_cycles.begin();
120  it != subset_of_cycles.end();
121  ++it)
122  {
123  /* cycle with already a delayed pair? */
124  bool next=false;
125  for(std::set<event_grapht::critical_cyclet::delayt>::iterator
126  p_it=it->unsafe_pairs.begin();
127  p_it!=it->unsafe_pairs.end(); ++p_it)
128  {
129  if(delayed.find(*p_it)!=delayed.end())
130  {
131  next=true;
132  break;
133  }
134  }
135 
136  if(next)
137  continue;
138 
139  /* instruments the first pair */
140  if(!it->unsafe_pairs.empty())
141  {
142  std::set<event_grapht::critical_cyclet::delayt>::iterator
143  p_it=it->unsafe_pairs.begin();
144  delayed.insert(*p_it);
145  const abstract_eventt &first_ev=egraph[p_it->first];
146  var_to_instr.insert(first_ev.variable);
147  id2loc.insert(
148  std::pair<irep_idt, source_locationt>(
149  first_ev.variable, first_ev.source_location));
150  if(!p_it->is_po)
151  {
152  const abstract_eventt &second_ev=egraph[p_it->second];
153  var_to_instr.insert(second_ev.variable);
154  id2loc.insert(
155  std::pair<irep_idt, source_locationt>(
156  second_ev.variable, second_ev.source_location));
157  }
158  }
159  }
160 }
161 
163  const std::set<event_grapht::critical_cyclet> &)
164 {
165  /* TODO */
166  throw "read first strategy not implemented yet";
167 }
168 
170  const std::set<event_grapht::critical_cyclet> &)
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> &subset_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 C_j =
221  subset_of_cycles.begin();
222  C_j != subset_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()
241  << " cycles:" << subset_of_cycles.size() << 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, subset_of_cycles.size());
261  i=0;
262  for(std::set<event_grapht::critical_cyclet>::iterator C_j =
263  subset_of_cycles.begin();
264  C_j != subset_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 = subset_of_cycles.size() * edges.size();
274  message.debug() << "size of the system: " << mat_size
275  << messaget::eom;
276  std::vector<int> imat(mat_size+1);
277  std::vector<int> jmat(mat_size+1);
278  std::vector<double> vmat(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 C_j =
292  subset_of_cycles.begin();
293  C_j != subset_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 #else
348  (void)subset_of_cycles; // unused parameter
349  throw "sorry, minimum interference option requires glpk; "
350  "please recompile goto-instrument with glpk";
351 #endif
352 }
353 
355  const std::set<event_grapht::critical_cyclet> &set,
356  const std::set<event_idt> &my_events)
357 {
358  for(std::set<event_grapht::critical_cyclet>::const_iterator
359  it=set.begin();
360  it!=set.end(); ++it)
361  {
362  for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator
363  p_it=it->unsafe_pairs.begin();
364  p_it!=it->unsafe_pairs.end(); ++p_it)
365  {
366  if(my_events.find(p_it->first)!=my_events.end())
367  {
368  const abstract_eventt &first_ev=egraph[p_it->first];
369  var_to_instr.insert(first_ev.variable);
370  id2loc.insert(
371  std::pair<irep_idt, source_locationt>(
372  first_ev.variable, first_ev.source_location));
373  if(!p_it->is_po && my_events.find(p_it->second)!=my_events.end())
374  {
375  const abstract_eventt &second_ev=egraph[p_it->second];
376  var_to_instr.insert(second_ev.variable);
377  id2loc.insert(
378  std::pair<irep_idt, source_locationt>(second_ev.variable,
379  second_ev.source_location));
380  }
381  }
382  }
383  }
384 }
385 
387  const std::set<event_idt> &my_events)
388 {
389  var_to_instr.clear();
390  id2loc.clear();
391  id2cycloc.clear();
392 
393  if(!set_of_cycles.empty())
395  else if(num_sccs!=0)
396  {
397  for(std::size_t i=0; i<num_sccs; ++i)
399  }
400  else
401  message.debug() << "no cycles to instrument" << messaget::eom;
402 }
403 
404 std::set<event_idt> instrumentert::extract_my_events()
405 {
406  std::ifstream file;
407  file.open("inst.evt");
408  std::set<event_idt> this_set;
409 
410  std::size_t size;
411  file >> size;
412 
413  std::size_t tmp;
414 
415  for(std::size_t i=0; i<size; i++)
416  {
417  file >> tmp;
418  this_set.insert(tmp);
419  }
420 
421  file.close();
422 
423  return this_set;
424 }
source_locationt source_location
std::multimap< irep_idt, source_locationt > id2cycloc
Definition: goto2graph.h:355
void instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)
unsigned num_sccs
Definition: goto2graph.h:319
void instrument_my_events(const std::set< event_idt > &events)
void instrument_all_inserter(const set_of_cyclest &set)
event_grapht egraph
Definition: goto2graph.h:309
void instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:315
void instrument_with_strategy(instrumentation_strategyt strategy)
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:353
void instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:354
void instrument_my_events_inserter(const set_of_cyclest &set, const std::set< event_idt > &events)
void instrument_minimum_interference_inserter(const set_of_cyclest &set)
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:318
messaget & message
Definition: goto2graph.h:306
unsigned cost(const event_grapht::critical_cyclet::delayt &e)
cost function
static std::set< event_idt > extract_my_events()
mstreamt & statistics() const
Definition: message.h:419
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
Instrumenter.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
instrumentation_strategyt
Definition: wmm.h:27
@ my_events
Definition: wmm.h:32
@ one_event_per_cycle
Definition: wmm.h:33
@ min_interference
Definition: wmm.h:29
@ read_first
Definition: wmm.h:30
@ all
Definition: wmm.h:28
@ write_first
Definition: wmm.h:31