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 = NULL;
  58   new_state = xbt_new0(s_mc_visited_state_t, 1);
  59   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
  60     MC_process_get_heap(process)->heaplimit,
  61     MC_process_get_malloc_info(process));
  62
  63   if (MC_process_is_self(&mc_model_checker->process)) {
  64     new_state->nb_processes = xbt_swag_size(simix_global->process_list);
  65   } else {
  66     MC_process_smx_refresh(&mc_model_checker->process);
  67     new_state->nb_processes = xbt_dynar_length(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   pair->nb_processes = xbt_swag_size(simix_global->process_list);
  88   pair->automaton_state = automaton_state;
  89   pair->num = pair_num;
  90   pair->other_num = -1;
  91   pair->acceptance_removed = 0;
  92   pair->visited_removed = 0;
  93   pair->acceptance_pair = 0;
  94   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
  95   unsigned int cursor = 0;
  96   int value;
  97   xbt_dynar_foreach(atomic_propositions, cursor, value)
  98       xbt_dynar_push_as(pair->atomic_propositions, int, value);
  99   return pair;
 100 }
 101
 102 static int is_exploration_stack_pair(mc_visited_pair_t pair){
 103   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
 104   while (item) {
 105     if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
 106       ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
 107       return 1;
 108     }
 109     item = xbt_fifo_get_next_item(item);
 110   }
 111   return 0;
 112 }
 113
 114 void MC_visited_pair_delete(mc_visited_pair_t p)
 115 {
 116   p->automaton_state = NULL;
 117   if( !is_exploration_stack_pair(p))
 118     MC_state_delete(p->graph_state, 1);
 119   xbt_dynar_free(&(p->atomic_propositions));
 120   xbt_free(p);
 121   p = NULL;
 122 }
 123
 124 /**
 125  *  \brief Find a suitable subrange of candidate duplicates for a given state
 126  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
 127  *  \param ref current state/pair;
 128  *  \param min (output) index of the beginning of the the subrange
 129  *  \param max (output) index of the enf of the subrange
 130  *
 131  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
 132  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
 133  *  This function uses only fast discriminating criterions and does not use the
 134  *  full state/pair comparison algorithms.
 135  *
 136  *  The states/pairs in list MUST be ordered using a (given) weak order
 137  *  (based on nb_processes and heap_bytes_used).
 138  *  The subrange is the subrange of "equivalence" of the given state/pair.
 139  */
 140 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 141 {
 142
 143   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 144
 145   int cursor = 0, previous_cursor, next_cursor;
 146   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 147   void *ref_test;
 148
 149   if (_sg_mc_liveness) {
 150     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 151     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 152   } else {
 153     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 154     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 155   }
 156
 157   int start = 0;
 158   int end = xbt_dynar_length(list) - 1;
 159
 160   while (start <= end) {
 161     cursor = (start + end) / 2;
 162     if (_sg_mc_liveness) {
 163       ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 164       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 165       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 166     } else {
 167       ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
 168       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 169       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 170     }
 171     if (nb_processes_test < nb_processes) {
 172       start = cursor + 1;
 173     } else if (nb_processes_test > nb_processes) {
 174       end = cursor - 1;
 175     } else {
 176       if (heap_bytes_used_test < heap_bytes_used) {
 177         start = cursor + 1;
 178       } else if (heap_bytes_used_test > heap_bytes_used) {
 179         end = cursor - 1;
 180       } else {
 181         *min = *max = cursor;
 182         previous_cursor = cursor - 1;
 183         while (previous_cursor >= 0) {
 184           if (_sg_mc_liveness) {
 185             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
 186             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 187             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 188           } else {
 189             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
 190             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 191             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 192           }
 193           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 194             break;
 195           *min = previous_cursor;
 196           previous_cursor--;
 197         }
 198         next_cursor = cursor + 1;
 199         while (next_cursor < xbt_dynar_length(list)) {
 200           if (_sg_mc_liveness) {
 201             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
 202             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 203             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 204           } else {
 205             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
 206             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 207             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 208           }
 209           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 210             break;
 211           *max = next_cursor;
 212           next_cursor++;
 213         }
 214         mmalloc_set_current_heap(heap);
 215         return -1;
 216       }
 217     }
 218   }
 219
 220   mmalloc_set_current_heap(heap);
 221   return cursor;
 222 }
 223
 224
 225 /**
 226  * \brief Checks whether a given state has already been visited by the algorithm.
 227  */
 228
 229 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 230 {
 231
 232   if (_sg_mc_visited == 0)
 233     return NULL;
 234
 235   int partial_comm = 0;
 236
 237   /* If comm determinism verification, we cannot stop the exploration if some
 238      communications are not finished (at least, data are transfered). These communications
 239      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 240   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 241     int current_process = 1;
 242     while (current_process < MC_smx_get_maxpid()) {
 243       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 244         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 245         partial_comm = 1;
 246         break;
 247       }
 248       current_process++;
 249     }
 250   }
 251
 252   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 253
 254   mc_visited_state_t new_state = visited_state_new();
 255   graph_state->system_state = new_state->system_state;
 256   graph_state->in_visited_states = 1;
 257   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 258
 259   if (xbt_dynar_is_empty(visited_states)) {
 260
 261     xbt_dynar_push(visited_states, &new_state);
 262     mmalloc_set_current_heap(heap);
 263     return NULL;
 264
 265   } else {
 266
 267     int min = -1, max = -1, index;
 268     //int res;
 269     mc_visited_state_t state_test;
 270     int cursor;
 271
 272     index = get_search_interval(visited_states, new_state, &min, &max);
 273
 274     if (min != -1 && max != -1) {
 275
 276       // Parallell implementation
 277       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 278          if(res != -1){
 279          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 280          if(state_test->other_num == -1)
 281          new_state->other_num = state_test->num;
 282          else
 283          new_state->other_num = state_test->other_num;
 284          if(dot_output == NULL)
 285          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 286          else
 287          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);
 288          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 289          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 290          if(!raw_mem_set)
 291          MC_SET_STD_HEAP;
 292          return new_state->other_num;
 293          } */
 294
 295       if (_sg_mc_safety || (!partial_comm
 296         && initial_global_state->initial_communications_pattern_done)) {
 297
 298         cursor = min;
 299         while (cursor <= max) {
 300           state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 301           if (snapshot_compare(state_test, new_state) == 0) {
 302             // The state has been visited:
 303
 304             if (state_test->other_num == -1)
 305               new_state->other_num = state_test->num;
 306             else
 307               new_state->other_num = state_test->other_num;
 308             if (dot_output == NULL)
 309               XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 310             else
 311               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);
 312
 313             /* Replace the old state with the new one (with a bigger num)
 314                (when the max number of visited states is reached,  the oldest
 315                one is removed according to its number (= with the min number) */
 316             xbt_dynar_remove_at(visited_states, cursor, NULL);
 317             xbt_dynar_insert_at(visited_states, cursor, &new_state);
 318             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 319
 320             mmalloc_set_current_heap(heap);
 321             return state_test;
 322           }
 323           cursor++;
 324         }
 325       }
 326
 327       xbt_dynar_insert_at(visited_states, min, &new_state);
 328       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 329
 330     } else {
 331
 332       // The state has not been visited: insert the state in the dynamic array.
 333       state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 334       if (state_test->nb_processes < new_state->nb_processes) {
 335         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 336       } else {
 337         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 338           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 339         else
 340           xbt_dynar_insert_at(visited_states, index, &new_state);
 341       }
 342
 343        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 344
 345     }
 346
 347     // We have reached the maximum number of stored states;
 348     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 349
 350       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 351
 352       // Find the (index of the) older state (with the smallest num):
 353       int min2 = mc_stats->expanded_states;
 354       unsigned int cursor2 = 0;
 355       unsigned int index2 = 0;
 356       xbt_dynar_foreach(visited_states, cursor2, state_test){
 357         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 358           index2 = cursor2;
 359           min2 = state_test->num;
 360         }
 361       }
 362
 363       // and drop it:
 364       xbt_dynar_remove_at(visited_states, index2, NULL);
 365       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 366     }
 367
 368     mmalloc_set_current_heap(heap);
 369     return NULL;
 370   }
 371 }
 372
 373 /**
 374  * \brief Checks whether a given pair has already been visited by the algorithm.
 375  */
 376 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 377
 378   if (_sg_mc_visited == 0)
 379     return -1;
 380
 381   xbt_mheap_t heap = mmalloc_set_current_heap(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               mmalloc_set_current_heap(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   mmalloc_set_current_heap(heap);
 498   return -1;
 499 }