src/mc/mc_visited.c

   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 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
  18                                 "Logging specific to state equaity detection mechanisms");
  19
  20 xbt_dynar_t visited_pairs;
  21 xbt_dynar_t visited_states;
  22
  23 static int is_exploration_stack_state(mc_visited_state_t state){
  24   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
  25   while (item) {
  26     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
  27       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
  28       return 1;
  29     }
  30     item = xbt_fifo_get_next_item(item);
  31   }
  32   return 0;
  33 }
  34
  35 void visited_state_free(mc_visited_state_t state)
  36 {
  37   if (state) {
  38     if(!is_exploration_stack_state(state)){
  39       MC_free_snapshot(state->system_state);
  40     }
  41     xbt_free(state);
  42   }
  43 }
  44
  45 void visited_state_free_voidp(void *s)
  46 {
  47   visited_state_free((mc_visited_state_t) * (void **) s);
  48 }
  49
  50 /**
  51  * \brief Save the current state
  52  * \return Snapshot of the current state.
  53  */
  54 static mc_visited_state_t visited_state_new()
  55 {
  56   mc_process_t process = &(mc_model_checker->process);
  57   mc_visited_state_t new_state = NULL;
  58   new_state = xbt_new0(s_mc_visited_state_t, 1);
  59   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
  60     MC_process_get_heap(process)->heaplimit,
  61     MC_process_get_malloc_info(process));
  62
  63   if (MC_process_is_self(&mc_model_checker->process)) {
  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(mc_model_checker->process.smx_process_infos);
  68   }
  69
  70   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
  71   new_state->num = mc_stats->expanded_states;
  72   new_state->other_num = -1;
  73   return new_state;
  74 }
  75
  76 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)
  77 {
  78   mc_process_t process = &(mc_model_checker->process);
  79   mc_visited_pair_t pair = NULL;
  80   pair = xbt_new0(s_mc_visited_pair_t, 1);
  81   pair->graph_state = graph_state;
  82   if(pair->graph_state->system_state == NULL)
  83     pair->graph_state->system_state = MC_take_snapshot(pair_num);
  84   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
  85     MC_process_get_heap(process)->heaplimit,
  86     MC_process_get_malloc_info(process));
  87   pair->nb_processes = xbt_swag_size(simix_global->process_list);
  88   pair->automaton_state = automaton_state;
  89   pair->num = pair_num;
  90   pair->other_num = -1;
  91   pair->acceptance_removed = 0;
  92   pair->visited_removed = 0;
  93   pair->acceptance_pair = 0;
  94   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
  95   unsigned int cursor = 0;
  96   int value;
  97   xbt_dynar_foreach(atomic_propositions, cursor, value)
  98       xbt_dynar_push_as(pair->atomic_propositions, int, value);
  99   return pair;
 100 }
 101
 102 static int is_exploration_stack_pair(mc_visited_pair_t pair){
 103   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
 104   while (item) {
 105     if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
 106       ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
 107       return 1;
 108     }
 109     item = xbt_fifo_get_next_item(item);
 110   }
 111   return 0;
 112 }
 113
 114 void MC_visited_pair_delete(mc_visited_pair_t p)
 115 {
 116   p->automaton_state = NULL;
 117   if( !is_exploration_stack_pair(p))
 118     MC_state_delete(p->graph_state, 1);
 119   xbt_dynar_free(&(p->atomic_propositions));
 120   xbt_free(p);
 121   p = NULL;
 122 }
 123
 124 /**
 125  *  \brief Find a suitable subrange of candidate duplicates for a given state
 126  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
 127  *  \param ref current state/pair;
 128  *  \param min (output) index of the beginning of the the subrange
 129  *  \param max (output) index of the enf of the subrange
 130  *
 131  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
 132  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
 133  *  This function uses only fast discriminating criterions and does not use the
 134  *  full state/pair comparison algorithms.
 135  *
 136  *  The states/pairs in list MUST be ordered using a (given) weak order
 137  *  (based on nb_processes and heap_bytes_used).
 138  *  The subrange is the subrange of "equivalence" of the given state/pair.
 139  */
 140 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 141 {
 142
 143   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 144
 145   int cursor = 0, previous_cursor, next_cursor;
 146   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 147   void *ref_test;
 148
 149   if (_sg_mc_liveness) {
 150     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 151     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 152   } else {
 153     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 154     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 155   }
 156
 157   int start = 0;
 158   int end = xbt_dynar_length(list) - 1;
 159
 160   while (start <= end) {
 161     cursor = (start + end) / 2;
 162     if (_sg_mc_liveness) {
 163       ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 164       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 165       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 166     } else {
 167       ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
 168       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 169       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 170     }
 171     if (nb_processes_test < nb_processes) {
 172       start = cursor + 1;
 173     } else if (nb_processes_test > nb_processes) {
 174       end = cursor - 1;
 175     } else {
 176       if (heap_bytes_used_test < heap_bytes_used) {
 177         start = cursor + 1;
 178       } else if (heap_bytes_used_test > heap_bytes_used) {
 179         end = cursor - 1;
 180       } else {
 181         *min = *max = cursor;
 182         previous_cursor = cursor - 1;
 183         while (previous_cursor >= 0) {
 184           if (_sg_mc_liveness) {
 185             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
 186             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 187             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 188           } else {
 189             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
 190             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 191             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 192           }
 193           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 194             break;
 195           *min = previous_cursor;
 196           previous_cursor--;
 197         }
 198         next_cursor = cursor + 1;
 199         while (next_cursor < xbt_dynar_length(list)) {
 200           if (_sg_mc_liveness) {
 201             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
 202             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 203             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 204           } else {
 205             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
 206             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 207             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 208           }
 209           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 210             break;
 211           *max = next_cursor;
 212           next_cursor++;
 213         }
 214         mmalloc_set_current_heap(heap);
 215         return -1;
 216       }
 217     }
 218   }
 219
 220   mmalloc_set_current_heap(heap);
 221   return cursor;
 222 }
 223
 224
 225 /**
 226  * \brief Checks whether a given state has already been visited by the algorithm.
 227  */
 228
 229 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 230 {
 231
 232   if (_sg_mc_visited == 0)
 233     return NULL;
 234
 235   int partial_comm = 0;
 236
 237   /* If comm determinism verification, we cannot stop the exploration if some
 238      communications are not finished (at least, data are transfered). These communications
 239      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 240   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 241     int current_process = 1;
 242     while (current_process < MC_smx_get_maxpid()) {
 243       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 244         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 245         partial_comm = 1;
 246         break;
 247       }
 248       current_process++;
 249     }
 250   }
 251
 252   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 253
 254   mc_visited_state_t new_state = visited_state_new();
 255   graph_state->system_state = new_state->system_state;
 256   graph_state->in_visited_states = 1;
 257   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 258
 259   if (xbt_dynar_is_empty(visited_states)) {
 260
 261     xbt_dynar_push(visited_states, &new_state);
 262     mmalloc_set_current_heap(heap);
 263     return NULL;
 264
 265   } else {
 266
 267     int min = -1, max = -1, index;
 268     //int res;
 269     mc_visited_state_t state_test;
 270     int cursor;
 271
 272     index = get_search_interval(visited_states, new_state, &min, &max);
 273
 274     if (min != -1 && max != -1) {
 275
 276       // Parallell implementation
 277       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 278          if(res != -1){
 279          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 280          if(state_test->other_num == -1)
 281          new_state->other_num = state_test->num;
 282          else
 283          new_state->other_num = state_test->other_num;
 284          if(dot_output == NULL)
 285          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 286          else
 287          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);
 288          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 289          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 290          if(!raw_mem_set)
 291          MC_SET_STD_HEAP;
 292          return new_state->other_num;
 293          } */
 294
 295       if(!partial_comm && initial_global_state->initial_communications_pattern_done){
 296
 297         cursor = min;
 298         while (cursor <= max) {
 299           state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 300           if (snapshot_compare(state_test, new_state) == 0) {
 301             // The state has been visited:
 302
 303             if (state_test->other_num == -1)
 304               new_state->other_num = state_test->num;
 305             else
 306               new_state->other_num = state_test->other_num;
 307             if (dot_output == NULL)
 308               XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 309             else
 310               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);
 311
 312             /* Replace the old state with the new one (with a bigger num)
 313                (when the max number of visited states is reached,  the oldest
 314                one is removed according to its number (= with the min number) */
 315             xbt_dynar_remove_at(visited_states, cursor, NULL);
 316             xbt_dynar_insert_at(visited_states, cursor, &new_state);
 317             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 318
 319             mmalloc_set_current_heap(heap);
 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 (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     mmalloc_set_current_heap(heap);
 368     return NULL;
 369   }
 370 }
 371
 372 /**
 373  * \brief Checks whether a given pair has already been visited by the algorithm.
 374  */
 375 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 376
 377   if (_sg_mc_visited == 0)
 378     return -1;
 379
 380   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 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          if(!raw_mem_set)
 428          MC_SET_STD_HEAP;
 429          return pair->other_num;
 430          } */
 431       cursor = min;
 432       while (cursor <= max) {
 433         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 434         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 435           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 436             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 437               if (pair_test->other_num == -1)
 438                 new_visited_pair->other_num = pair_test->num;
 439               else
 440                 new_visited_pair->other_num = pair_test->other_num;
 441               if (dot_output == NULL)
 442                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 443               else
 444                 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);
 445               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 446               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 447               pair_test->visited_removed = 1;
 448               if (pair_test->acceptance_pair) {
 449                 if (pair_test->acceptance_removed == 1)
 450                   MC_visited_pair_delete(pair_test);
 451               } else {
 452                 MC_visited_pair_delete(pair_test);
 453               }
 454               mmalloc_set_current_heap(heap);
 455               return new_visited_pair->other_num;
 456             }
 457           }
 458         }
 459         cursor++;
 460       }
 461       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 462     } else {
 463       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 464       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 465         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 466       } else {
 467         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 468           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 469         else
 470           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 471       }
 472     }
 473
 474     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 475       int min2 = mc_stats->expanded_pairs;
 476       unsigned int cursor2 = 0;
 477       unsigned int index2 = 0;
 478       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 479         if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
 480           index2 = cursor2;
 481           min2 = pair_test->num;
 482         }
 483       }
 484       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 485       pair_test->visited_removed = 1;
 486       if (pair_test->acceptance_pair) {
 487         if (pair_test->acceptance_removed)
 488           MC_visited_pair_delete(pair_test);
 489       } else {
 490         MC_visited_pair_delete(pair_test);
 491       }
 492     }
 493
 494   }
 495
 496   mmalloc_set_current_heap(heap);
 497   return -1;
 498 }