src/mc/mc_visited.cpp

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