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   /* If comm determinism verification, we cannot stop the exploration if some
 256      communications are not finished (at least, data are transfered). These communications
 257      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 258   int partial_comm = 0;
 259   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 260     for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 261       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 262         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 263         partial_comm = 1;
 264         break;
 265       }
 266     }
 267   }
 268
 269   mc_visited_state_t new_state = visited_state_new();
 270   graph_state->system_state = new_state->system_state;
 271   graph_state->in_visited_states = 1;
 272   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 273
 274   if (xbt_dynar_is_empty(visited_states)) {
 275
 276     xbt_dynar_push(visited_states, &new_state);
 277     return NULL;
 278
 279   } else {
 280
 281     int min = -1, max = -1, index;
 282
 283     index = get_search_interval(visited_states, new_state, &min, &max);
 284
 285     if (min != -1 && max != -1) {
 286
 287       // Parallell implementation
 288       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 289          if(res != -1){
 290          mc_visited_state_t state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 291          if(state_test->other_num == -1)
 292          new_state->other_num = state_test->num;
 293          else
 294          new_state->other_num = state_test->other_num;
 295          if(dot_output == NULL)
 296          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 297          else
 298          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);
 299          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 300          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 301          return new_state->other_num;
 302          } */
 303
 304       if (_sg_mc_safety || (!partial_comm
 305         && initial_global_state->initial_communications_pattern_done)) {
 306
 307         int cursor = min;
 308         while (cursor <= max) {
 309           mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 310           if (snapshot_compare(state_test, new_state) == 0) {
 311             // The state has been visited:
 312
 313             replace_state(state_test, new_state, cursor);
 314             return state_test;
 315           }
 316           cursor++;
 317         }
 318       }
 319
 320       xbt_dynar_insert_at(visited_states, min, &new_state);
 321       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 322
 323     } else {
 324
 325       // The state has not been visited: insert the state in the dynamic array.
 326       mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 327       if (state_test->nb_processes < new_state->nb_processes) {
 328         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 329       } else {
 330         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 331           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 332         else
 333           xbt_dynar_insert_at(visited_states, index, &new_state);
 334       }
 335
 336        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 337
 338     }
 339
 340     // We have reached the maximum number of stored states;
 341     if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
 342
 343       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 344
 345       // Find the (index of the) older state (with the smallest num):
 346       int min2 = mc_stats->expanded_states;
 347       unsigned int cursor2 = 0;
 348       unsigned int index2 = 0;
 349
 350       mc_visited_state_t state_test;
 351       xbt_dynar_foreach(visited_states, cursor2, state_test){
 352         if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) {
 353           index2 = cursor2;
 354           min2 = state_test->num;
 355         }
 356       }
 357
 358       // and drop it:
 359       xbt_dynar_remove_at(visited_states, index2, NULL);
 360       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 361     }
 362
 363     return NULL;
 364   }
 365 }
 366
 367 /**
 368  * \brief Checks whether a given pair has already been visited by the algorithm.
 369  */
 370 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 371
 372   if (_sg_mc_visited == 0)
 373     return -1;
 374
 375   mc_visited_pair_t new_visited_pair = NULL;
 376
 377   if (visited_pair == NULL) {
 378     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 379   } else {
 380     new_visited_pair = visited_pair;
 381   }
 382
 383   if (xbt_dynar_is_empty(visited_pairs)) {
 384
 385     xbt_dynar_push(visited_pairs, &new_visited_pair);
 386
 387   } else {
 388
 389     int min = -1, max = -1, index;
 390     //int res;
 391     mc_visited_pair_t pair_test;
 392     int cursor;
 393
 394     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 395
 396     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 397       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 398          if(res != -1){
 399          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 400          if(pair_test->other_num == -1)
 401          pair->other_num = pair_test->num;
 402          else
 403          pair->other_num = pair_test->other_num;
 404          if(dot_output == NULL)
 405          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 406          else
 407          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 408          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 409          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 410          pair_test->visited_removed = 1;
 411          if(pair_test->stack_removed && pair_test->visited_removed){
 412          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 413          if(pair_test->acceptance_removed){
 414          MC_pair_delete(pair_test);
 415          }
 416          }else{
 417          MC_pair_delete(pair_test);
 418          }
 419          }
 420          return pair->other_num;
 421          } */
 422       cursor = min;
 423       while (cursor <= max) {
 424         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 425         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 426           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 427             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 428               if (pair_test->other_num == -1)
 429                 new_visited_pair->other_num = pair_test->num;
 430               else
 431                 new_visited_pair->other_num = pair_test->other_num;
 432               if (dot_output == NULL)
 433                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 434               else
 435                 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);
 436               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 437               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 438               pair_test->visited_removed = 1;
 439               if (pair_test->acceptance_pair) {
 440                 if (pair_test->acceptance_removed == 1)
 441                   MC_visited_pair_delete(pair_test);
 442               } else {
 443                 MC_visited_pair_delete(pair_test);
 444               }
 445               return new_visited_pair->other_num;
 446             }
 447           }
 448         }
 449         cursor++;
 450       }
 451       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 452     } else {
 453       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 454       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 455         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 456       } else {
 457         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 458           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 459         else
 460           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 461       }
 462     }
 463
 464     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 465       int min2 = mc_stats->expanded_pairs;
 466       unsigned int cursor2 = 0;
 467       unsigned int index2 = 0;
 468       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 469         if (!MC_important_snapshot(pair_test->graph_state->system_state)
 470             && pair_test->num < min2) {
 471           index2 = cursor2;
 472           min2 = pair_test->num;
 473         }
 474       }
 475       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 476       pair_test->visited_removed = 1;
 477       if (pair_test->acceptance_pair) {
 478         if (pair_test->acceptance_removed)
 479           MC_visited_pair_delete(pair_test);
 480       } else {
 481         MC_visited_pair_delete(pair_test);
 482       }
 483     }
 484
 485   }
 486   return -1;
 487 }
 488
 489 }