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