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