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