src/mc/mc_visited.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 <unistd.h>
   8 #include <sys/wait.h>
   9
  10 #include "mc_comm_pattern.h"
  11 #include "mc_safety.h"
  12 #include "mc_liveness.h"
  13 #include "mc_private.h"
  14
  15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
  16                                 "Logging specific to state equaity detection mechanisms");
  17
  18 xbt_dynar_t visited_pairs;
  19 xbt_dynar_t visited_states;
  20
  21 static int is_exploration_stack_state(mc_visited_state_t state){
  22   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
  23   while (item) {
  24     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
  25       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
  26       return 1;
  27     }
  28     item = xbt_fifo_get_next_item(item);
  29   }
  30   return 0;
  31 }
  32
  33 void visited_state_free(mc_visited_state_t state)
  34 {
  35   if (state) {
  36     if(!is_exploration_stack_state(state)){
  37       MC_free_snapshot(state->system_state);
  38     }
  39     xbt_free(state);
  40   }
  41 }
  42
  43 void visited_state_free_voidp(void *s)
  44 {
  45   visited_state_free((mc_visited_state_t) * (void **) s);
  46 }
  47
  48 /**
  49  * \brief Save the current state
  50  * \return Snapshot of the current state.
  51  */
  52 static mc_visited_state_t visited_state_new()
  53 {
  54   mc_process_t process = &(mc_model_checker->process);
  55   mc_visited_state_t new_state = NULL;
  56   new_state = xbt_new0(s_mc_visited_state_t, 1);
  57   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
  58     MC_process_get_heap(process)->heaplimit,
  59     MC_process_get_malloc_info(process));
  60   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
  61   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
  62   new_state->num = mc_stats->expanded_states;
  63   new_state->other_num = -1;
  64   return new_state;
  65 }
  66
  67 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
  68 {
  69   mc_process_t process = &(mc_model_checker->process);
  70   mc_visited_pair_t pair = NULL;
  71   pair = xbt_new0(s_mc_visited_pair_t, 1);
  72   pair->graph_state = graph_state;
  73   if(pair->graph_state->system_state == NULL)
  74     pair->graph_state->system_state = MC_take_snapshot(pair_num);
  75   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
  76     MC_process_get_heap(process)->heaplimit,
  77     MC_process_get_malloc_info(process));
  78   pair->nb_processes = xbt_swag_size(simix_global->process_list);
  79   pair->automaton_state = automaton_state;
  80   pair->num = pair_num;
  81   pair->other_num = -1;
  82   pair->acceptance_removed = 0;
  83   pair->visited_removed = 0;
  84   pair->acceptance_pair = 0;
  85   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
  86   unsigned int cursor = 0;
  87   int value;
  88   xbt_dynar_foreach(atomic_propositions, cursor, value)
  89       xbt_dynar_push_as(pair->atomic_propositions, int, value);
  90   return pair;
  91 }
  92
  93 static int is_exploration_stack_pair(mc_visited_pair_t pair){
  94   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
  95   while (item) {
  96     if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
  97       ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
  98       return 1;
  99     }
 100     item = xbt_fifo_get_next_item(item);
 101   }
 102   return 0;
 103 }
 104
 105 void MC_visited_pair_delete(mc_visited_pair_t p)
 106 {
 107   p->automaton_state = NULL;
 108   if( !is_exploration_stack_pair(p))
 109     MC_state_delete(p->graph_state, 1);
 110   xbt_dynar_free(&(p->atomic_propositions));
 111   xbt_free(p);
 112   p = NULL;
 113 }
 114
 115 /**
 116  *  \brief Find a suitable subrange of candidate duplicates for a given state
 117  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
 118  *  \param ref current state/pair;
 119  *  \param min (output) index of the beginning of the the subrange
 120  *  \param max (output) index of the enf of the subrange
 121  *
 122  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
 123  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
 124  *  This function uses only fast discriminating criterions and does not use the
 125  *  full state/pair comparison algorithms.
 126  *
 127  *  The states/pairs in list MUST be ordered using a (given) weak order
 128  *  (based on nb_processes and heap_bytes_used).
 129  *  The subrange is the subrange of "equivalence" of the given state/pair.
 130  */
 131 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 132 {
 133
 134   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 135
 136   int cursor = 0, previous_cursor, next_cursor;
 137   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 138   void *ref_test;
 139
 140   if (_sg_mc_liveness) {
 141     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 142     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 143   } else {
 144     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 145     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 146   }
 147
 148   int start = 0;
 149   int end = xbt_dynar_length(list) - 1;
 150
 151   while (start <= end) {
 152     cursor = (start + end) / 2;
 153     if (_sg_mc_liveness) {
 154       ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 155       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 156       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 157     } else {
 158       ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
 159       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 160       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 161     }
 162     if (nb_processes_test < nb_processes) {
 163       start = cursor + 1;
 164     } else if (nb_processes_test > nb_processes) {
 165       end = cursor - 1;
 166     } else {
 167       if (heap_bytes_used_test < heap_bytes_used) {
 168         start = cursor + 1;
 169       } else if (heap_bytes_used_test > heap_bytes_used) {
 170         end = cursor - 1;
 171       } else {
 172         *min = *max = cursor;
 173         previous_cursor = cursor - 1;
 174         while (previous_cursor >= 0) {
 175           if (_sg_mc_liveness) {
 176             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
 177             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 178             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 179           } else {
 180             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
 181             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 182             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 183           }
 184           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 185             break;
 186           *min = previous_cursor;
 187           previous_cursor--;
 188         }
 189         next_cursor = cursor + 1;
 190         while (next_cursor < xbt_dynar_length(list)) {
 191           if (_sg_mc_liveness) {
 192             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
 193             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 194             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 195           } else {
 196             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
 197             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 198             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 199           }
 200           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 201             break;
 202           *max = next_cursor;
 203           next_cursor++;
 204         }
 205         mmalloc_set_current_heap(heap);
 206         return -1;
 207       }
 208     }
 209   }
 210
 211   mmalloc_set_current_heap(heap);
 212   return cursor;
 213 }
 214
 215
 216 /**
 217  * \brief Checks whether a given state has already been visited by the algorithm.
 218  */
 219
 220 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 221 {
 222
 223   if (_sg_mc_visited == 0)
 224     return NULL;
 225
 226   int partial_comm = 0;
 227
 228   /* If comm determinism verification, we cannot stop the exploration if some
 229      communications are not finished (at least, data are transfered). These communications
 230      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 231   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 232     int current_process = 1;
 233     while (current_process < MC_smx_get_maxpid()) {
 234       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 235         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 236         partial_comm = 1;
 237         break;
 238       }
 239       current_process++;
 240     }
 241   }
 242
 243   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 244
 245   mc_visited_state_t new_state = visited_state_new();
 246   graph_state->system_state = new_state->system_state;
 247   graph_state->in_visited_states = 1;
 248   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 249
 250   if (xbt_dynar_is_empty(visited_states)) {
 251
 252     xbt_dynar_push(visited_states, &new_state);
 253     mmalloc_set_current_heap(heap);
 254     return NULL;
 255
 256   } else {
 257
 258     int min = -1, max = -1, index;
 259     //int res;
 260     mc_visited_state_t state_test;
 261     int cursor;
 262
 263     index = get_search_interval(visited_states, new_state, &min, &max);
 264
 265     if (min != -1 && max != -1) {
 266
 267       // Parallell implementation
 268       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 269          if(res != -1){
 270          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 271          if(state_test->other_num == -1)
 272          new_state->other_num = state_test->num;
 273          else
 274          new_state->other_num = state_test->other_num;
 275          if(dot_output == NULL)
 276          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 277          else
 278          XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
 279          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 280          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 281          if(!raw_mem_set)
 282          MC_SET_STD_HEAP;
 283          return new_state->other_num;
 284          } */
 285
 286       if(!partial_comm && initial_global_state->initial_communications_pattern_done){
 287
 288         cursor = min;
 289         while (cursor <= max) {
 290           state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 291           if (snapshot_compare(state_test, new_state) == 0) {
 292             // The state has been visited:
 293
 294             if (state_test->other_num == -1)
 295               new_state->other_num = state_test->num;
 296             else
 297               new_state->other_num = state_test->other_num;
 298             if (dot_output == NULL)
 299               XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 300             else
 301               XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
 302
 303             /* Replace the old state with the new one (with a bigger num)
 304                (when the max number of visited states is reached,  the oldest
 305                one is removed according to its number (= with the min number) */
 306             xbt_dynar_remove_at(visited_states, cursor, NULL);
 307             xbt_dynar_insert_at(visited_states, cursor, &new_state);
 308             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 309
 310             mmalloc_set_current_heap(heap);
 311             return state_test;
 312           }
 313           cursor++;
 314         }
 315       }
 316
 317       xbt_dynar_insert_at(visited_states, min, &new_state);
 318       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 319
 320     } else {
 321
 322       // The state has not been visited: insert the state in the dynamic array.
 323       state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 324       if (state_test->nb_processes < new_state->nb_processes) {
 325         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 326       } else {
 327         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 328           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 329         else
 330           xbt_dynar_insert_at(visited_states, index, &new_state);
 331       }
 332
 333        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 334
 335     }
 336
 337     // We have reached the maximum number of stored states;
 338     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 339
 340       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 341
 342       // Find the (index of the) older state (with the smallest num):
 343       int min2 = mc_stats->expanded_states;
 344       unsigned int cursor2 = 0;
 345       unsigned int index2 = 0;
 346       xbt_dynar_foreach(visited_states, cursor2, state_test){
 347         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 348           index2 = cursor2;
 349           min2 = state_test->num;
 350         }
 351       }
 352
 353       // and drop it:
 354       xbt_dynar_remove_at(visited_states, index2, NULL);
 355       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 356     }
 357
 358     mmalloc_set_current_heap(heap);
 359     return NULL;
 360   }
 361 }
 362
 363 /**
 364  * \brief Checks whether a given pair has already been visited by the algorithm.
 365  */
 366 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 367
 368   if (_sg_mc_visited == 0)
 369     return -1;
 370
 371   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 372
 373   mc_visited_pair_t new_visited_pair = NULL;
 374
 375   if (visited_pair == NULL) {
 376     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 377   } else {
 378     new_visited_pair = visited_pair;
 379   }
 380
 381   if (xbt_dynar_is_empty(visited_pairs)) {
 382
 383     xbt_dynar_push(visited_pairs, &new_visited_pair);
 384
 385   } else {
 386
 387     int min = -1, max = -1, index;
 388     //int res;
 389     mc_visited_pair_t pair_test;
 390     int cursor;
 391
 392     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 393
 394     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 395       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 396          if(res != -1){
 397          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 398          if(pair_test->other_num == -1)
 399          pair->other_num = pair_test->num;
 400          else
 401          pair->other_num = pair_test->other_num;
 402          if(dot_output == NULL)
 403          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 404          else
 405          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 406          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 407          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 408          pair_test->visited_removed = 1;
 409          if(pair_test->stack_removed && pair_test->visited_removed){
 410          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 411          if(pair_test->acceptance_removed){
 412          MC_pair_delete(pair_test);
 413          }
 414          }else{
 415          MC_pair_delete(pair_test);
 416          }
 417          }
 418          if(!raw_mem_set)
 419          MC_SET_STD_HEAP;
 420          return pair->other_num;
 421          } */
 422       cursor = min;
 423       while (cursor <= max) {
 424         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 425         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 426           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 427             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 428               if (pair_test->other_num == -1)
 429                 new_visited_pair->other_num = pair_test->num;
 430               else
 431                 new_visited_pair->other_num = pair_test->other_num;
 432               if (dot_output == NULL)
 433                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 434               else
 435                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
 436               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 437               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 438               pair_test->visited_removed = 1;
 439               if (pair_test->acceptance_pair) {
 440                 if (pair_test->acceptance_removed == 1)
 441                   MC_visited_pair_delete(pair_test);
 442               } else {
 443                 MC_visited_pair_delete(pair_test);
 444               }
 445               mmalloc_set_current_heap(heap);
 446               return new_visited_pair->other_num;
 447             }
 448           }
 449         }
 450         cursor++;
 451       }
 452       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 453     } else {
 454       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 455       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 456         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 457       } else {
 458         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 459           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 460         else
 461           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 462       }
 463     }
 464
 465     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 466       int min2 = mc_stats->expanded_pairs;
 467       unsigned int cursor2 = 0;
 468       unsigned int index2 = 0;
 469       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 470         if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
 471           index2 = cursor2;
 472           min2 = pair_test->num;
 473         }
 474       }
 475       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 476       pair_test->visited_removed = 1;
 477       if (pair_test->acceptance_pair) {
 478         if (pair_test->acceptance_removed)
 479           MC_visited_pair_delete(pair_test);
 480       } else {
 481         MC_visited_pair_delete(pair_test);
 482       }
 483     }
 484
 485   }
 486
 487   mmalloc_set_current_heap(heap);
 488   return -1;
 489 }