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