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