Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
aaac6e5b3afb1a0f53e2e161a33dd1cc469add38
[simgrid.git] / src / mc / mc_global.c
1 #include <unistd.h>
2 #include <sys/types.h>
3 #include <sys/wait.h>
4
5 #include "../surf/surf_private.h"
6 #include "../simix/private.h"
7 #include "xbt/fifo.h"
8 #include "private.h"
9
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
12                                 "Logging specific to MC (global)");
13
14 /* MC global data structures */
15 mc_snapshot_t initial_snapshot = NULL;
16 xbt_fifo_t mc_stack = NULL;
17 mc_stats_t mc_stats = NULL;
18 mc_stats_pair_t mc_stats_pair = NULL;
19 mc_state_t mc_current_state = NULL;
20 char mc_replay_mode = FALSE;
21 double *mc_time = NULL;
22 xbt_fifo_t mc_snapshot_stack = NULL;
23
24 /**
25  *  \brief Initialize the model-checker data structures
26  */
27 void MC_init(void)
28 {
29   /* Check if MC is already initialized */
30   if (initial_snapshot)
31     return;
32
33   mc_time = xbt_new0(double, simix_process_maxpid);
34
35   /* Initialize the data structures that must be persistent across every
36      iteration of the model-checker (in RAW memory) */
37   MC_SET_RAW_MEM;
38
39   /* Initialize statistics */
40   mc_stats = xbt_new0(s_mc_stats_t, 1);
41   mc_stats->state_size = 1;
42
43   /* Create exploration stack */
44   mc_stack = xbt_fifo_new();
45
46   MC_UNSET_RAW_MEM;
47
48   MC_dpor_init();
49
50   MC_SET_RAW_MEM;
51   /* Save the initial state */
52   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
53   MC_take_snapshot(initial_snapshot);
54   MC_UNSET_RAW_MEM;
55 }
56
57 void MC_init_stateful(void){
58   
59    /* Check if MC is already initialized */
60   if (initial_snapshot)
61     return;
62
63   mc_time = xbt_new0(double, simix_process_maxpid);
64
65   /* Initialize the data structures that must be persistent across every
66      iteration of the model-checker (in RAW memory) */
67   MC_SET_RAW_MEM;
68
69   /* Initialize statistics */
70   mc_stats = xbt_new0(s_mc_stats_t, 1);
71   mc_stats->state_size = 1;
72
73   /* Create exploration stack */
74   mc_snapshot_stack = xbt_fifo_new();
75
76   MC_UNSET_RAW_MEM;
77
78   MC_dpor_stateful_init();
79
80
81 }
82
83 void MC_init_with_automaton(xbt_automaton_t a){
84
85   XBT_DEBUG("Start init mc");
86   
87   mc_time = xbt_new0(double, simix_process_maxpid);
88
89   /* Initialize the data structures that must be persistent across every
90      iteration of the model-checker (in RAW memory) */
91
92   MC_SET_RAW_MEM;
93
94   /* Initialize statistics */
95   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
96   mc_stats = xbt_new0(s_mc_stats_t, 1);
97   //mc_stats_pair->pair_size = 1;
98
99   XBT_DEBUG("Creating snapshot_stack");
100
101  /* Create exploration stack */
102   mc_snapshot_stack = xbt_fifo_new();
103
104
105   MC_UNSET_RAW_MEM;
106
107   //MC_vddfs_with_restore_snapshot_init(a);
108   //MC_ddfs_with_restore_snapshot_init(a);
109   MC_dpor2_init(a);
110   //MC_dpor3_init(a);
111 }
112
113
114 void MC_modelcheck(void)
115 {
116   MC_init();
117   MC_dpor();
118   MC_exit();
119 }
120
121 void MC_modelcheck_stateful(void)
122 {
123   MC_init_stateful();
124   MC_dpor_stateful();
125   MC_exit();
126 }
127
128 void MC_modelcheck_with_automaton(xbt_automaton_t a){
129   MC_init_with_automaton(a);
130   MC_exit_with_automaton();
131 }
132
133 void MC_exit_with_automaton(void)
134 {
135   MC_print_statistics_pairs(mc_stats_pair);
136   xbt_free(mc_time);
137   MC_memory_exit();
138 }
139
140 void MC_exit(void)
141 {
142   MC_print_statistics(mc_stats);
143   xbt_free(mc_time);
144   MC_memory_exit();
145 }
146
147
148 int MC_random(int min, int max)
149 {
150   /*FIXME: return mc_current_state->executed_transition->random.value;*/
151   return 0;
152 }
153
154 /**
155  * \brief Schedules all the process that are ready to run
156  */
157 void MC_wait_for_requests(void)
158 {
159   smx_process_t process;
160   smx_req_t req;
161   unsigned int iter;
162
163   while (xbt_dynar_length(simix_global->process_to_run)) {
164     SIMIX_process_runall();
165     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
166       req = &process->request;
167       if (req->call != REQ_NO_REQ && !MC_request_is_visible(req))
168           SIMIX_request_pre(req, 0);
169     }
170   }
171 }
172
173 int MC_deadlock_check()
174 {
175   int deadlock = FALSE;
176   smx_process_t process;
177   if(xbt_swag_size(simix_global->process_list)){
178     deadlock = TRUE;
179     xbt_swag_foreach(process, simix_global->process_list){
180       if(process->request.call != REQ_NO_REQ
181          && MC_request_is_enabled(&process->request)){
182         deadlock = FALSE;
183         break;
184       }
185     }
186   }
187   return deadlock;
188 }
189
190 /**
191  * \brief Re-executes from the initial state all the transitions indicated by
192  *        a given model-checker stack.
193  * \param stack The stack with the transitions to execute.
194 */
195 void MC_replay(xbt_fifo_t stack)
196 {
197   int value;
198   char *req_str;
199   smx_req_t req = NULL, saved_req = NULL;
200   xbt_fifo_item_t item;
201   mc_state_t state;
202
203   XBT_DEBUG("**** Begin Replay ****");
204
205   /* Restore the initial state */
206   MC_restore_snapshot(initial_snapshot);
207   /* At the moment of taking the snapshot the raw heap was set, so restoring
208    * it will set it back again, we have to unset it to continue  */
209   MC_UNSET_RAW_MEM;
210
211   /* Traverse the stack from the initial state and re-execute the transitions */
212   for (item = xbt_fifo_get_last_item(stack);
213        item != xbt_fifo_get_first_item(stack);
214        item = xbt_fifo_get_prev_item(item)) {
215
216     state = (mc_state_t) xbt_fifo_get_item_content(item);
217     saved_req = MC_state_get_executed_request(state, &value);
218    
219     if(saved_req){
220       /* because we got a copy of the executed request, we have to fetch the  
221          real one, pointed by the request field of the issuer process */
222       req = &saved_req->issuer->request;
223
224       /* Debug information */
225       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
226         req_str = MC_request_to_string(req, value);
227         XBT_DEBUG("Replay: %s (%p)", req_str, state);
228         xbt_free(req_str);
229       }
230     }
231          
232     SIMIX_request_pre(req, value);
233     MC_wait_for_requests();
234          
235     /* Update statistics */
236     mc_stats->visited_states++;
237     mc_stats->executed_transitions++;
238   }
239   XBT_DEBUG("**** End Replay ****");
240 }
241
242 /**
243  * \brief Dumps the contents of a model-checker's stack and shows the actual
244  *        execution trace
245  * \param stack The stack to dump
246 */
247 void MC_dump_stack(xbt_fifo_t stack)
248 {
249   mc_state_t state;
250
251   MC_show_stack(stack);
252
253   MC_SET_RAW_MEM;
254   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
255     MC_state_delete(state);
256   MC_UNSET_RAW_MEM;
257 }
258
259
260 void MC_show_stack(xbt_fifo_t stack)
261 {
262   int value;
263   mc_state_t state;
264   xbt_fifo_item_t item;
265   smx_req_t req;
266   char *req_str = NULL;
267   
268   for (item = xbt_fifo_get_last_item(stack);
269        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
270         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
271     req = MC_state_get_executed_request(state, &value);
272     if(req){
273       req_str = MC_request_to_string(req, value);
274       XBT_INFO("%s", req_str);
275       xbt_free(req_str);
276     }
277   }
278 }
279
280 void MC_show_deadlock(smx_req_t req)
281 {
282   /*char *req_str = NULL;*/
283   XBT_INFO("**************************");
284   XBT_INFO("*** DEAD-LOCK DETECTED ***");
285   XBT_INFO("**************************");
286   XBT_INFO("Locked request:");
287   /*req_str = MC_request_to_string(req);
288   XBT_INFO("%s", req_str);
289   xbt_free(req_str);*/
290   XBT_INFO("Counter-example execution trace:");
291   MC_dump_stack(mc_stack);
292 }
293
294 void MC_show_deadlock_stateful(smx_req_t req)
295 {
296   /*char *req_str = NULL;*/
297   XBT_INFO("**************************");
298   XBT_INFO("*** DEAD-LOCK DETECTED ***");
299   XBT_INFO("**************************");
300   XBT_INFO("Locked request:");
301   /*req_str = MC_request_to_string(req);
302   XBT_INFO("%s", req_str);
303   xbt_free(req_str);*/
304   XBT_INFO("Counter-example execution trace:");
305   MC_show_stack_stateful(mc_snapshot_stack);
306 }
307
308 void MC_dump_stack_stateful(xbt_fifo_t stack)
309 {
310   //mc_state_ws_t state;
311
312   MC_show_stack_stateful(stack);
313
314   /*MC_SET_RAW_MEM;
315   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
316     MC_state_delete(state);
317     MC_UNSET_RAW_MEM;*/
318 }
319
320
321 void MC_show_stack_stateful(xbt_fifo_t stack)
322 {
323   int value;
324   mc_state_ws_t state;
325   xbt_fifo_item_t item;
326   smx_req_t req;
327   char *req_str = NULL;
328   
329   for (item = xbt_fifo_get_last_item(stack);
330        (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
331         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
332     req = MC_state_get_executed_request(state->graph_state, &value);
333     if(req){
334       req_str = MC_request_to_string(req, value);
335       XBT_INFO("%s", req_str);
336       xbt_free(req_str);
337     }
338   }
339 }
340
341 void MC_print_statistics(mc_stats_t stats)
342 {
343   XBT_INFO("State space size ~= %lu", stats->state_size);
344   XBT_INFO("Expanded states = %lu", stats->expanded_states);
345   XBT_INFO("Visited states = %lu", stats->visited_states);
346   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
347   XBT_INFO("Expanded / Visited = %lf",
348         (double) stats->visited_states / stats->expanded_states);
349   /*XBT_INFO("Exploration coverage = %lf",
350      (double)stats->expanded_states / stats->state_size); */
351 }
352
353 void MC_print_statistics_pairs(mc_stats_pair_t stats)
354 {
355   XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
356   XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
357   //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
358   XBT_INFO("Expanded / Visited = %lf",
359         (double) stats->visited_pairs / stats->expanded_pairs);
360   /*XBT_INFO("Exploration coverage = %lf",
361      (double)stats->expanded_states / stats->state_size); */
362 }
363
364 void MC_assert(int prop)
365 {
366   if (MC_IS_ENABLED && !prop) {
367     XBT_INFO("**************************");
368     XBT_INFO("*** PROPERTY NOT VALID ***");
369     XBT_INFO("**************************");
370     XBT_INFO("Counter-example execution trace:");
371     MC_dump_stack(mc_stack);
372     MC_print_statistics(mc_stats);
373     xbt_abort();
374   }
375 }
376
377 void MC_assert_stateful(int prop)
378 {
379   if (MC_IS_ENABLED && !prop) {
380     XBT_INFO("**************************");
381     XBT_INFO("*** PROPERTY NOT VALID ***");
382     XBT_INFO("**************************");
383     XBT_INFO("Counter-example execution trace:");
384     MC_dump_stack_stateful(mc_snapshot_stack);
385     MC_print_statistics(mc_stats);
386     xbt_abort();
387   }
388 }
389
390 void MC_assert_pair(int prop){
391   if (MC_IS_ENABLED && !prop) {
392     XBT_INFO("**************************");
393     XBT_INFO("*** PROPERTY NOT VALID ***");
394     XBT_INFO("**************************");
395     //XBT_INFO("Counter-example execution trace:");
396     MC_show_snapshot_stack(mc_snapshot_stack);
397     //MC_dump_snapshot_stack(mc_snapshot_stack);
398     MC_print_statistics_pairs(mc_stats_pair);
399     xbt_abort();
400   }
401 }
402
403 void MC_process_clock_add(smx_process_t process, double amount)
404 {
405   mc_time[process->pid] += amount;
406 }
407
408 double MC_process_clock_get(smx_process_t process)
409 {
410   if(mc_time)
411     return mc_time[process->pid];
412   else
413     return 0;
414 }