src/mc/mc_visited.cpp

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