Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
add a (unused) fortran datatype for compilation of recent bigdft
[simgrid.git] / src / mc / mc_liveness.c
1 /* Copyright (c) 2011-2014. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #include "mc_private.h"
8 #include <unistd.h>
9 #include <sys/wait.h>
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
12                                 "Logging specific to algorithms for liveness properties verification");
13
14 /********* Global variables *********/
15
16 xbt_dynar_t acceptance_pairs;
17 xbt_dynar_t successors;
18 xbt_parmap_t parmap;
19
20 /********* Static functions *********/
21
22 static xbt_dynar_t get_atomic_propositions_values()
23 {
24   int res;
25   int_f_void_t f;
26   unsigned int cursor = 0;
27   xbt_automaton_propositional_symbol_t ps = NULL;
28   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
29
30   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) {
31     f = (int_f_void_t) ps->function;
32     res = f();
33     xbt_dynar_push_as(values, int, res);
34   }
35
36   return values;
37 }
38
39
40 static mc_visited_pair_t is_reached_acceptance_pair(int pair_num,
41                                                     xbt_automaton_state_t
42                                                     automaton_state,
43                                                     xbt_dynar_t
44                                                     atomic_propositions)
45 {
46
47   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
48
49   MC_SET_MC_HEAP;
50
51   mc_visited_pair_t pair = NULL;
52   pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
53   pair->acceptance_pair = 1;
54
55   if (xbt_dynar_is_empty(acceptance_pairs)) {
56
57     xbt_dynar_push(acceptance_pairs, &pair);
58
59   } else {
60
61     int min = -1, max = -1, index;
62     //int res;
63     mc_visited_pair_t pair_test;
64     int cursor;
65
66     index = get_search_interval(acceptance_pairs, pair, &min, &max);
67
68     if (min != -1 && max != -1) {       // Acceptance pair with same number of processes and same heap bytes used exists
69
70       // Parallell implementation
71       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
72          if(res != -1){
73          if(!raw_mem_set)
74          MC_SET_STD_HEAP;
75          return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
76          } */
77
78       cursor = min;
79       while (cursor <= max) {
80         pair_test =
81             (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor,
82                                                  mc_visited_pair_t);
83         if (xbt_automaton_state_compare
84             (pair_test->automaton_state, pair->automaton_state) == 0) {
85           if (xbt_automaton_propositional_symbols_compare_value
86               (pair_test->atomic_propositions,
87                pair->atomic_propositions) == 0) {
88             if (snapshot_compare(pair_test, pair) == 0) {
89               XBT_INFO("Pair %d already reached (equal to pair %d) !",
90                        pair->num, pair_test->num);
91
92               xbt_fifo_shift(mc_stack);
93               if (dot_output != NULL)
94                 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
95                         initial_global_state->prev_pair, pair_test->num,
96                         initial_global_state->prev_req);
97
98               if (!raw_mem_set)
99                 MC_SET_STD_HEAP;
100
101               return NULL;
102             }
103           }
104         }
105         cursor++;
106       }
107       xbt_dynar_insert_at(acceptance_pairs, min, &pair);
108     } else {
109       pair_test =
110           (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index,
111                                                mc_visited_pair_t);
112       if (pair_test->nb_processes < pair->nb_processes) {
113         xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
114       } else {
115         if (pair_test->heap_bytes_used < pair->heap_bytes_used)
116           xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
117         else
118           xbt_dynar_insert_at(acceptance_pairs, index, &pair);
119       }
120     }
121
122   }
123
124   if (!raw_mem_set)
125     MC_SET_STD_HEAP;
126
127   return pair;
128
129 }
130
131 static void remove_acceptance_pair(int pair_num)
132 {
133
134   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
135
136   MC_SET_MC_HEAP;
137
138   unsigned int cursor = 0;
139   mc_visited_pair_t pair_test = NULL;
140
141   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
142     if (pair_test->num == pair_num) {
143       break;
144     }
145   }
146
147   xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
148
149   pair_test->acceptance_removed = 1;
150
151   if (_sg_mc_visited == 0) {
152     MC_visited_pair_delete(pair_test);
153   } else if (pair_test->visited_removed == 1) {
154     MC_visited_pair_delete(pair_test);
155   }
156
157   if (!raw_mem_set)
158     MC_SET_STD_HEAP;
159 }
160
161
162 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
163                                        xbt_dynar_t atomic_propositions_values)
164 {
165
166   switch (l->type) {
167   case 0:{
168       int left_res =
169           MC_automaton_evaluate_label(l->u.or_and.left_exp,
170                                       atomic_propositions_values);
171       int right_res =
172           MC_automaton_evaluate_label(l->u.or_and.right_exp,
173                                       atomic_propositions_values);
174       return (left_res || right_res);
175     }
176   case 1:{
177       int left_res =
178           MC_automaton_evaluate_label(l->u.or_and.left_exp,
179                                       atomic_propositions_values);
180       int right_res =
181           MC_automaton_evaluate_label(l->u.or_and.right_exp,
182                                       atomic_propositions_values);
183       return (left_res && right_res);
184     }
185   case 2:{
186       int res =
187           MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
188       return (!res);
189     }
190   case 3:{
191       unsigned int cursor = 0;
192       xbt_automaton_propositional_symbol_t p = NULL;
193       xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor,
194                         p) {
195         if (strcmp(p->pred, l->u.predicat) == 0)
196           return (int) xbt_dynar_get_as(atomic_propositions_values, cursor,
197                                         int);
198       }
199       return -1;
200     }
201   case 4:{
202       return 2;
203     }
204   default:
205     return -1;
206   }
207 }
208
209 void MC_pre_modelcheck_liveness(void)
210 {
211
212   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
213
214   mc_pair_t initial_pair = NULL;
215   smx_process_t process;
216
217   MC_wait_for_requests();
218
219   MC_SET_MC_HEAP;
220
221   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
222   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
223   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
224
225   initial_global_state->snapshot = MC_take_snapshot(0);
226   initial_global_state->prev_pair = 0;
227
228   MC_SET_STD_HEAP;
229
230   unsigned int cursor = 0;
231   xbt_automaton_state_t automaton_state;
232
233   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state) {
234     if (automaton_state->type == -1) {  /* Initial automaton state */
235
236       MC_SET_MC_HEAP;
237
238       initial_pair = MC_pair_new();
239       initial_pair->automaton_state = automaton_state;
240       initial_pair->graph_state = MC_state_new();
241       initial_pair->atomic_propositions = get_atomic_propositions_values();
242
243       /* Get enabled processes and insert them in the interleave set of the graph_state */
244       xbt_swag_foreach(process, simix_global->process_list) {
245         if (MC_process_is_enabled(process)) {
246           MC_state_interleave_process(initial_pair->graph_state, process);
247         }
248       }
249
250       initial_pair->requests =
251           MC_state_interleave_size(initial_pair->graph_state);
252       initial_pair->search_cycle = 0;
253
254       xbt_fifo_unshift(mc_stack, initial_pair);
255
256       MC_SET_STD_HEAP;
257
258       MC_modelcheck_liveness();
259
260       if (cursor != 0) {
261         MC_restore_snapshot(initial_global_state->snapshot);
262         MC_SET_STD_HEAP;
263       }
264     }
265   }
266
267   if (initial_global_state->raw_mem_set)
268     MC_SET_MC_HEAP;
269   else
270     MC_SET_STD_HEAP;
271
272
273 }
274
275
276 void MC_modelcheck_liveness()
277 {
278
279   smx_process_t process;
280   mc_pair_t current_pair = NULL;
281
282   if (xbt_fifo_size(mc_stack) == 0)
283     return;
284
285   /* Get current pair */
286   current_pair =
287       (mc_pair_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
288
289   /* Update current state in buchi automaton */
290   _mc_property_automaton->current_state = current_pair->automaton_state;
291
292   XBT_DEBUG
293       ("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)",
294        xbt_fifo_size(mc_stack), current_pair->search_cycle,
295        MC_state_interleave_size(current_pair->graph_state), current_pair->num);
296
297   mc_stats->visited_pairs++;
298
299   int value;
300   smx_simcall_t req = NULL;
301   char *req_str;
302
303   xbt_automaton_transition_t transition_succ;
304   unsigned int cursor = 0;
305   int res;
306   int visited_num;
307
308   mc_pair_t next_pair = NULL;
309   xbt_dynar_t prop_values = NULL;
310   mc_visited_pair_t reached_pair = NULL;
311   int counter_example_depth = 0;
312
313   if (xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
314
315     if (current_pair->requests > 0) {
316
317       if (current_pair->search_cycle) {
318
319         if ((current_pair->automaton_state->type == 1)
320             || (current_pair->automaton_state->type == 2)) {
321           if ((reached_pair =
322                is_reached_acceptance_pair(current_pair->num,
323                                           current_pair->automaton_state,
324                                           current_pair->atomic_propositions)) ==
325               NULL) {
326
327             counter_example_depth = xbt_fifo_size(mc_stack);
328             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
329             XBT_INFO("|             ACCEPTANCE CYCLE            |");
330             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
331             XBT_INFO("Counter-example that violates formula :");
332             MC_show_stack_liveness(mc_stack);
333             MC_dump_stack_liveness(mc_stack);
334             MC_print_statistics(mc_stats);
335             XBT_INFO("Counter-example depth : %d", counter_example_depth);
336             xbt_abort();
337
338           }
339         }
340       }
341
342       if ((visited_num =
343            is_visited_pair(reached_pair, current_pair->num,
344                            current_pair->automaton_state,
345                            current_pair->atomic_propositions)) != -1) {
346
347         MC_SET_MC_HEAP;
348         if (dot_output != NULL)
349           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
350                   initial_global_state->prev_pair, visited_num,
351                   initial_global_state->prev_req);
352         MC_SET_STD_HEAP;
353
354       } else {
355
356         while ((req =
357                 MC_state_get_request(current_pair->graph_state,
358                                      &value)) != NULL) {
359
360           MC_SET_MC_HEAP;
361           if (dot_output != NULL) {
362             if (initial_global_state->prev_pair != 0
363                 && initial_global_state->prev_pair != current_pair->num) {
364               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
365                       initial_global_state->prev_pair, current_pair->num,
366                       initial_global_state->prev_req);
367               xbt_free(initial_global_state->prev_req);
368             }
369             initial_global_state->prev_pair = current_pair->num;
370           }
371           MC_SET_STD_HEAP;
372
373           /* Debug information */
374           if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
375             req_str = MC_request_to_string(req, value);
376             XBT_DEBUG("Execute: %s", req_str);
377             xbt_free(req_str);
378           }
379
380           MC_SET_MC_HEAP;
381           if (dot_output != NULL) {
382             initial_global_state->prev_req =
383                 MC_request_get_dot_output(req, value);
384             if (current_pair->search_cycle)
385               fprintf(dot_output, "%d [shape=doublecircle];\n",
386                       current_pair->num);
387           }
388           MC_SET_STD_HEAP;
389
390           MC_state_set_executed_request(current_pair->graph_state, req, value);
391           mc_stats->executed_transitions++;
392
393           /* Answer the request */
394           SIMIX_simcall_enter(req, value);
395
396           /* Wait for requests (schedules processes) */
397           MC_wait_for_requests();
398
399           MC_SET_MC_HEAP;
400           prop_values = get_atomic_propositions_values();
401           MC_SET_STD_HEAP;
402
403           int new_pair = 0;
404
405           /* Evaluate enabled transition according to atomic propositions values */
406           cursor = 0;
407           xbt_dynar_foreach(current_pair->automaton_state->out, cursor,
408                             transition_succ) {
409
410             res =
411                 MC_automaton_evaluate_label(transition_succ->label,
412                                             prop_values);
413
414             if (res == 1) {     // enabled transition in automaton
415
416               if (new_pair)
417                 MC_replay_liveness(mc_stack, 1);
418
419               MC_SET_MC_HEAP;
420
421               next_pair = MC_pair_new();
422               next_pair->graph_state = MC_state_new();
423               next_pair->automaton_state = transition_succ->dst;
424               next_pair->atomic_propositions = get_atomic_propositions_values();
425
426               /* Get enabled processes and insert them in the interleave set of the next graph_state */
427               xbt_swag_foreach(process, simix_global->process_list) {
428                 if (MC_process_is_enabled(process)) {
429                   MC_state_interleave_process(next_pair->graph_state, process);
430                 }
431               }
432
433               next_pair->requests =
434                   MC_state_interleave_size(next_pair->graph_state);
435
436               if (next_pair->automaton_state->type == 1
437                   || next_pair->automaton_state->type == 2
438                   || current_pair->search_cycle)
439                 next_pair->search_cycle = 1;
440
441               xbt_fifo_unshift(mc_stack, next_pair);
442
443               if (mc_stats->expanded_pairs % 1000000 == 0)
444                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
445
446               MC_SET_STD_HEAP;
447
448               new_pair = 1;
449
450               MC_modelcheck_liveness();
451
452             }
453
454           }
455
456           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
457           cursor = 0;
458           xbt_dynar_foreach(current_pair->automaton_state->out, cursor,
459                             transition_succ) {
460
461             res =
462                 MC_automaton_evaluate_label(transition_succ->label,
463                                             prop_values);
464
465             if (res == 2) {     // true transition in automaton
466
467               if (new_pair)
468                 MC_replay_liveness(mc_stack, 1);
469
470               MC_SET_MC_HEAP;
471
472               next_pair = MC_pair_new();
473               next_pair->graph_state = MC_state_new();
474               next_pair->automaton_state = transition_succ->dst;
475               next_pair->atomic_propositions = get_atomic_propositions_values();
476
477               /* Get enabled process and insert it in the interleave set of the next graph_state */
478               xbt_swag_foreach(process, simix_global->process_list) {
479                 if (MC_process_is_enabled(process)) {
480                   MC_state_interleave_process(next_pair->graph_state, process);
481                 }
482               }
483
484               next_pair->requests =
485                   MC_state_interleave_size(next_pair->graph_state);
486
487               if (next_pair->automaton_state->type == 1
488                   || next_pair->automaton_state->type == 2
489                   || current_pair->search_cycle)
490                 next_pair->search_cycle = 1;
491
492               xbt_fifo_unshift(mc_stack, next_pair);
493
494               if (mc_stats->expanded_pairs % 1000000 == 0)
495                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
496
497               MC_SET_STD_HEAP;
498
499               new_pair = 1;
500
501               MC_modelcheck_liveness();
502
503             }
504
505           }
506
507           if (MC_state_interleave_size(current_pair->graph_state) > 0) {
508             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack));
509             MC_replay_liveness(mc_stack, 0);
510           }
511
512         }
513
514       }
515
516     }
517
518   } else {
519
520     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
521     if (MC_state_interleave_size(current_pair->graph_state) > 0) {
522       XBT_WARN
523           ("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
524       if (_sg_mc_max_depth == 1000)
525         XBT_WARN
526             ("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
527     }
528
529   }
530
531   if (xbt_fifo_size(mc_stack) == _sg_mc_max_depth) {
532     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached",
533               current_pair->num, xbt_fifo_size(mc_stack));
534   } else {
535     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num,
536               xbt_fifo_size(mc_stack));
537   }
538
539
540   MC_SET_MC_HEAP;
541   xbt_dynar_free(&prop_values);
542   current_pair = xbt_fifo_shift(mc_stack);
543   if (xbt_fifo_size(mc_stack) != _sg_mc_max_depth - 1
544       && current_pair->requests > 0 && current_pair->search_cycle) {
545     remove_acceptance_pair(current_pair->num);
546   }
547   MC_pair_delete(current_pair);
548
549   MC_SET_STD_HEAP;
550
551 }