CBMC
Loading...
Searching...
No Matches
instrumenter_strategies.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Strategies for picking the abstract events to instrument
4
5Author: Vincent Nimal
6
7Date: 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
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
177unsigned inline instrumentert::cost(
179{
180 /* cost(poW*)=1
181 cost(poRW)=cost(rfe)=2
182 cost(poRR)=3 */
184 return 1;
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;
233 parm.msg_lev=GLP_MSG_OFF;
234 parm.presolve=GLP_ON;
235
237 glp_set_prob_name(lp, "instrumentation optimisation");
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);
257 }
258
259 /* sets the constraints (soundness): one per cycle */
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 */
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
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{
390 id2loc.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
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}
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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 & debug() const
Definition message.h:421
mstreamt & statistics() const
Definition message.h:411
static eomt eom
Definition message.h:289
Instrumenter.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
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