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_model_checker->is_important_snapshot(*state_test->system_state)
 359             && state_test->num < min2) {
 360           index2 = cursor2;
 361           min2 = state_test->num;
 362         }
 363       }
 364
 365       // and drop it:
 366       xbt_dynar_remove_at(visited_states, index2, NULL);
 367       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 368     }
 369
 370     return NULL;
 371   }
 372 }
 373
 374 /**
 375  * \brief Checks whether a given pair has already been visited by the algorithm.
 376  */
 377 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 378
 379   if (_sg_mc_visited == 0)
 380     return -1;
 381
 382   mc_visited_pair_t new_visited_pair = NULL;
 383
 384   if (visited_pair == NULL) {
 385     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 386   } else {
 387     new_visited_pair = visited_pair;
 388   }
 389
 390   if (xbt_dynar_is_empty(visited_pairs)) {
 391
 392     xbt_dynar_push(visited_pairs, &new_visited_pair);
 393
 394   } else {
 395
 396     int min = -1, max = -1, index;
 397     //int res;
 398     mc_visited_pair_t pair_test;
 399     int cursor;
 400
 401     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 402
 403     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 404       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 405          if(res != -1){
 406          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 407          if(pair_test->other_num == -1)
 408          pair->other_num = pair_test->num;
 409          else
 410          pair->other_num = pair_test->other_num;
 411          if(dot_output == NULL)
 412          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 413          else
 414          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 415          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 416          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 417          pair_test->visited_removed = 1;
 418          if(pair_test->stack_removed && pair_test->visited_removed){
 419          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 420          if(pair_test->acceptance_removed){
 421          MC_pair_delete(pair_test);
 422          }
 423          }else{
 424          MC_pair_delete(pair_test);
 425          }
 426          }
 427          return pair->other_num;
 428          } */
 429       cursor = min;
 430       while (cursor <= max) {
 431         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 432         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 433           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 434             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 435               if (pair_test->other_num == -1)
 436                 new_visited_pair->other_num = pair_test->num;
 437               else
 438                 new_visited_pair->other_num = pair_test->other_num;
 439               if (dot_output == NULL)
 440                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 441               else
 442                 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);
 443               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 444               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 445               pair_test->visited_removed = 1;
 446               if (pair_test->acceptance_pair) {
 447                 if (pair_test->acceptance_removed == 1)
 448                   MC_visited_pair_delete(pair_test);
 449               } else {
 450                 MC_visited_pair_delete(pair_test);
 451               }
 452               return new_visited_pair->other_num;
 453             }
 454           }
 455         }
 456         cursor++;
 457       }
 458       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 459     } else {
 460       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 461       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 462         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 463       } else {
 464         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 465           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 466         else
 467           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 468       }
 469     }
 470
 471     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 472       int min2 = mc_stats->expanded_pairs;
 473       unsigned int cursor2 = 0;
 474       unsigned int index2 = 0;
 475       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 476         if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
 477             && pair_test->num < min2) {
 478           index2 = cursor2;
 479           min2 = pair_test->num;
 480         }
 481       }
 482       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 483       pair_test->visited_removed = 1;
 484       if (pair_test->acceptance_pair) {
 485         if (pair_test->acceptance_removed)
 486           MC_visited_pair_delete(pair_test);
 487       } else {
 488         MC_visited_pair_delete(pair_test);
 489       }
 490     }
 491
 492   }
 493   return -1;
 494 }
 495
 496 }