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(
  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     MC_process_get_heap(process)->heaplimit,
  87     MC_process_get_malloc_info(process));
  88   if (MC_process_is_self(&mc_model_checker->process)) {
  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
 150   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 151
 152   int cursor = 0, previous_cursor, next_cursor;
 153   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 154   void *ref_test;
 155
 156   if (_sg_mc_liveness) {
 157     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 158     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 159   } else {
 160     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 161     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 162   }
 163
 164   int start = 0;
 165   int end = xbt_dynar_length(list) - 1;
 166
 167   while (start <= end) {
 168     cursor = (start + end) / 2;
 169     if (_sg_mc_liveness) {
 170       ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 171       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 172       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 173     } else {
 174       ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
 175       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 176       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 177     }
 178     if (nb_processes_test < nb_processes) {
 179       start = cursor + 1;
 180     } else if (nb_processes_test > nb_processes) {
 181       end = cursor - 1;
 182     } else {
 183       if (heap_bytes_used_test < heap_bytes_used) {
 184         start = cursor + 1;
 185       } else if (heap_bytes_used_test > heap_bytes_used) {
 186         end = cursor - 1;
 187       } else {
 188         *min = *max = cursor;
 189         previous_cursor = cursor - 1;
 190         while (previous_cursor >= 0) {
 191           if (_sg_mc_liveness) {
 192             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
 193             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 194             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 195           } else {
 196             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
 197             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 198             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 199           }
 200           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 201             break;
 202           *min = previous_cursor;
 203           previous_cursor--;
 204         }
 205         next_cursor = cursor + 1;
 206         while (next_cursor < xbt_dynar_length(list)) {
 207           if (_sg_mc_liveness) {
 208             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
 209             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 210             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 211           } else {
 212             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
 213             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 214             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 215           }
 216           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 217             break;
 218           *max = next_cursor;
 219           next_cursor++;
 220         }
 221         mmalloc_set_current_heap(heap);
 222         return -1;
 223       }
 224     }
 225   }
 226
 227   mmalloc_set_current_heap(heap);
 228   return cursor;
 229 }
 230
 231
 232 /**
 233  * \brief Checks whether a given state has already been visited by the algorithm.
 234  */
 235
 236 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 237 {
 238
 239   if (_sg_mc_visited == 0)
 240     return NULL;
 241
 242   int partial_comm = 0;
 243
 244   /* If comm determinism verification, we cannot stop the exploration if some
 245      communications are not finished (at least, data are transfered). These communications
 246      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 247   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 248     int current_process = 1;
 249     while (current_process < MC_smx_get_maxpid()) {
 250       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 251         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 252         partial_comm = 1;
 253         break;
 254       }
 255       current_process++;
 256     }
 257   }
 258
 259   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 260
 261   mc_visited_state_t new_state = visited_state_new();
 262   graph_state->system_state = new_state->system_state;
 263   graph_state->in_visited_states = 1;
 264   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 265
 266   if (xbt_dynar_is_empty(visited_states)) {
 267
 268     xbt_dynar_push(visited_states, &new_state);
 269     mmalloc_set_current_heap(heap);
 270     return NULL;
 271
 272   } else {
 273
 274     int min = -1, max = -1, index;
 275     //int res;
 276     mc_visited_state_t state_test;
 277     int cursor;
 278
 279     index = get_search_interval(visited_states, new_state, &min, &max);
 280
 281     if (min != -1 && max != -1) {
 282
 283       // Parallell implementation
 284       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 285          if(res != -1){
 286          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 287          if(state_test->other_num == -1)
 288          new_state->other_num = state_test->num;
 289          else
 290          new_state->other_num = state_test->other_num;
 291          if(dot_output == NULL)
 292          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 293          else
 294          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);
 295          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 296          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 297          if(!raw_mem_set)
 298          MC_SET_STD_HEAP;
 299          return new_state->other_num;
 300          } */
 301
 302       if (_sg_mc_safety || (!partial_comm
 303         && initial_global_state->initial_communications_pattern_done)) {
 304
 305         cursor = min;
 306         while (cursor <= max) {
 307           state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 308           if (snapshot_compare(state_test, new_state) == 0) {
 309             // The state has been visited:
 310
 311             if (state_test->other_num == -1)
 312               new_state->other_num = state_test->num;
 313             else
 314               new_state->other_num = state_test->other_num;
 315             if (dot_output == NULL)
 316               XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 317             else
 318               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);
 319
 320             /* Replace the old state with the new one (with a bigger num)
 321                (when the max number of visited states is reached,  the oldest
 322                one is removed according to its number (= with the min number) */
 323             xbt_dynar_remove_at(visited_states, cursor, NULL);
 324             xbt_dynar_insert_at(visited_states, cursor, &new_state);
 325             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 326
 327             mmalloc_set_current_heap(heap);
 328             return state_test;
 329           }
 330           cursor++;
 331         }
 332       }
 333
 334       xbt_dynar_insert_at(visited_states, min, &new_state);
 335       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 336
 337     } else {
 338
 339       // The state has not been visited: insert the state in the dynamic array.
 340       state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 341       if (state_test->nb_processes < new_state->nb_processes) {
 342         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 343       } else {
 344         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 345           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 346         else
 347           xbt_dynar_insert_at(visited_states, index, &new_state);
 348       }
 349
 350        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 351
 352     }
 353
 354     // We have reached the maximum number of stored states;
 355     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 356
 357       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 358
 359       // Find the (index of the) older state (with the smallest num):
 360       int min2 = mc_stats->expanded_states;
 361       unsigned int cursor2 = 0;
 362       unsigned int index2 = 0;
 363       xbt_dynar_foreach(visited_states, cursor2, state_test){
 364         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 365           index2 = cursor2;
 366           min2 = state_test->num;
 367         }
 368       }
 369
 370       // and drop it:
 371       xbt_dynar_remove_at(visited_states, index2, NULL);
 372       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 373     }
 374
 375     mmalloc_set_current_heap(heap);
 376     return NULL;
 377   }
 378 }
 379
 380 /**
 381  * \brief Checks whether a given pair has already been visited by the algorithm.
 382  */
 383 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 384
 385   if (_sg_mc_visited == 0)
 386     return -1;
 387
 388   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 389
 390   mc_visited_pair_t new_visited_pair = NULL;
 391
 392   if (visited_pair == NULL) {
 393     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 394   } else {
 395     new_visited_pair = visited_pair;
 396   }
 397
 398   if (xbt_dynar_is_empty(visited_pairs)) {
 399
 400     xbt_dynar_push(visited_pairs, &new_visited_pair);
 401
 402   } else {
 403
 404     int min = -1, max = -1, index;
 405     //int res;
 406     mc_visited_pair_t pair_test;
 407     int cursor;
 408
 409     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 410
 411     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 412       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 413          if(res != -1){
 414          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 415          if(pair_test->other_num == -1)
 416          pair->other_num = pair_test->num;
 417          else
 418          pair->other_num = pair_test->other_num;
 419          if(dot_output == NULL)
 420          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 421          else
 422          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 423          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 424          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 425          pair_test->visited_removed = 1;
 426          if(pair_test->stack_removed && pair_test->visited_removed){
 427          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 428          if(pair_test->acceptance_removed){
 429          MC_pair_delete(pair_test);
 430          }
 431          }else{
 432          MC_pair_delete(pair_test);
 433          }
 434          }
 435          if(!raw_mem_set)
 436          MC_SET_STD_HEAP;
 437          return pair->other_num;
 438          } */
 439       cursor = min;
 440       while (cursor <= max) {
 441         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 442         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 443           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 444             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 445               if (pair_test->other_num == -1)
 446                 new_visited_pair->other_num = pair_test->num;
 447               else
 448                 new_visited_pair->other_num = pair_test->other_num;
 449               if (dot_output == NULL)
 450                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 451               else
 452                 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);
 453               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 454               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 455               pair_test->visited_removed = 1;
 456               if (pair_test->acceptance_pair) {
 457                 if (pair_test->acceptance_removed == 1)
 458                   MC_visited_pair_delete(pair_test);
 459               } else {
 460                 MC_visited_pair_delete(pair_test);
 461               }
 462               mmalloc_set_current_heap(heap);
 463               return new_visited_pair->other_num;
 464             }
 465           }
 466         }
 467         cursor++;
 468       }
 469       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 470     } else {
 471       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 472       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 473         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 474       } else {
 475         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 476           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 477         else
 478           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 479       }
 480     }
 481
 482     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 483       int min2 = mc_stats->expanded_pairs;
 484       unsigned int cursor2 = 0;
 485       unsigned int index2 = 0;
 486       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 487         if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
 488           index2 = cursor2;
 489           min2 = pair_test->num;
 490         }
 491       }
 492       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 493       pair_test->visited_removed = 1;
 494       if (pair_test->acceptance_pair) {
 495         if (pair_test->acceptance_removed)
 496           MC_visited_pair_delete(pair_test);
 497       } else {
 498         MC_visited_pair_delete(pair_test);
 499       }
 500     }
 501
 502   }
 503
 504   mmalloc_set_current_heap(heap);
 505   return -1;
 506 }