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 /**
 246  * \brief Checks whether a given state has already been visited by the algorithm.
 247  */
 248
 249 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 250 {
 251
 252   if (_sg_mc_visited == 0)
 253     return NULL;
 254
 255   int partial_comm = 0;
 256
 257   /* If comm determinism verification, we cannot stop the exploration if some
 258      communications are not finished (at least, data are transfered). These communications
 259      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 260   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 261     size_t current_process = 1;
 262     while (current_process < MC_smx_get_maxpid()) {
 263       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 264         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 265         partial_comm = 1;
 266         break;
 267       }
 268       current_process++;
 269     }
 270   }
 271
 272   mc_visited_state_t new_state = visited_state_new();
 273   graph_state->system_state = new_state->system_state;
 274   graph_state->in_visited_states = 1;
 275   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 276
 277   if (xbt_dynar_is_empty(visited_states)) {
 278
 279     xbt_dynar_push(visited_states, &new_state);
 280     return NULL;
 281
 282   } else {
 283
 284     int min = -1, max = -1, index;
 285     //int res;
 286     mc_visited_state_t state_test;
 287     int cursor;
 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          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         cursor = min;
 314         while (cursor <= max) {
 315           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       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       xbt_dynar_foreach(visited_states, cursor2, state_test){
 356         if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) {
 357           index2 = cursor2;
 358           min2 = state_test->num;
 359         }
 360       }
 361
 362       // and drop it:
 363       xbt_dynar_remove_at(visited_states, index2, NULL);
 364       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 365     }
 366
 367     return NULL;
 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   mc_visited_pair_t new_visited_pair = NULL;
 380
 381   if (visited_pair == NULL) {
 382     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 383   } else {
 384     new_visited_pair = visited_pair;
 385   }
 386
 387   if (xbt_dynar_is_empty(visited_pairs)) {
 388
 389     xbt_dynar_push(visited_pairs, &new_visited_pair);
 390
 391   } else {
 392
 393     int min = -1, max = -1, index;
 394     //int res;
 395     mc_visited_pair_t pair_test;
 396     int cursor;
 397
 398     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 399
 400     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 401       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 402          if(res != -1){
 403          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 404          if(pair_test->other_num == -1)
 405          pair->other_num = pair_test->num;
 406          else
 407          pair->other_num = pair_test->other_num;
 408          if(dot_output == NULL)
 409          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 410          else
 411          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 412          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 413          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 414          pair_test->visited_removed = 1;
 415          if(pair_test->stack_removed && pair_test->visited_removed){
 416          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 417          if(pair_test->acceptance_removed){
 418          MC_pair_delete(pair_test);
 419          }
 420          }else{
 421          MC_pair_delete(pair_test);
 422          }
 423          }
 424          return pair->other_num;
 425          } */
 426       cursor = min;
 427       while (cursor <= max) {
 428         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 429         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 430           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 431             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 432               if (pair_test->other_num == -1)
 433                 new_visited_pair->other_num = pair_test->num;
 434               else
 435                 new_visited_pair->other_num = pair_test->other_num;
 436               if (dot_output == NULL)
 437                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 438               else
 439                 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);
 440               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 441               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 442               pair_test->visited_removed = 1;
 443               if (pair_test->acceptance_pair) {
 444                 if (pair_test->acceptance_removed == 1)
 445                   MC_visited_pair_delete(pair_test);
 446               } else {
 447                 MC_visited_pair_delete(pair_test);
 448               }
 449               return new_visited_pair->other_num;
 450             }
 451           }
 452         }
 453         cursor++;
 454       }
 455       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 456     } else {
 457       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 458       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 459         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 460       } else {
 461         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 462           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 463         else
 464           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 465       }
 466     }
 467
 468     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 469       int min2 = mc_stats->expanded_pairs;
 470       unsigned int cursor2 = 0;
 471       unsigned int index2 = 0;
 472       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 473         if (!MC_important_snapshot(pair_test->graph_state->system_state)
 474             && pair_test->num < min2) {
 475           index2 = cursor2;
 476           min2 = pair_test->num;
 477         }
 478       }
 479       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 480       pair_test->visited_removed = 1;
 481       if (pair_test->acceptance_pair) {
 482         if (pair_test->acceptance_removed)
 483           MC_visited_pair_delete(pair_test);
 484       } else {
 485         MC_visited_pair_delete(pair_test);
 486       }
 487     }
 488
 489   }
 490   return -1;
 491 }
 492
 493 }