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 <xbt/automaton.h>
  11 #include <xbt/log.h>
  12 #include <xbt/sysdep.h>
  13 #include <xbt/dynar.h>
  14 #include <xbt/fifo.h>
  15
  16 #include "src/mc/mc_comm_pattern.h"
  17 #include "src/mc/mc_safety.h"
  18 #include "src/mc/mc_liveness.h"
  19 #include "src/mc/mc_private.h"
  20 #include "src/mc/Process.hpp"
  21 #include "src/mc/mc_smx.h"
  22
  23 extern "C" {
  24
  25 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
  26                                 "Logging specific to state equaity detection mechanisms");
  27
  28 xbt_dynar_t visited_pairs;
  29 xbt_dynar_t visited_states;
  30
  31 static int is_exploration_stack_state(mc_visited_state_t state){
  32   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
  33   while (item) {
  34     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
  35       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
  36       return 1;
  37     }
  38     item = xbt_fifo_get_next_item(item);
  39   }
  40   return 0;
  41 }
  42
  43 void visited_state_free(mc_visited_state_t state)
  44 {
  45   if (!state)
  46     return;
  47   if(!is_exploration_stack_state(state))
  48     delete state->system_state;
  49   xbt_free(state);
  50 }
  51
  52 void visited_state_free_voidp(void *s)
  53 {
  54   visited_state_free((mc_visited_state_t) * (void **) s);
  55 }
  56
  57 /**
  58  * \brief Save the current state
  59  * \return Snapshot of the current state.
  60  */
  61 static mc_visited_state_t visited_state_new()
  62 {
  63   simgrid::mc::Process* process = &(mc_model_checker->process());
  64   mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
  65   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
  66     process->get_heap()->heaplimit,
  67     process->get_malloc_info());
  68
  69   MC_process_smx_refresh(&mc_model_checker->process());
  70   new_state->nb_processes =
  71     mc_model_checker->process().smx_process_infos.size();
  72
  73   new_state->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states);
  74   new_state->num = mc_stats->expanded_states;
  75   new_state->other_num = -1;
  76   return new_state;
  77 }
  78
  79 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)
  80 {
  81   simgrid::mc::Process* process = &(mc_model_checker->process());
  82   mc_visited_pair_t pair = nullptr;
  83   pair = xbt_new0(s_mc_visited_pair_t, 1);
  84   pair->graph_state = graph_state;
  85   if(pair->graph_state->system_state == nullptr)
  86     pair->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
  87   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
  88     process->get_heap()->heaplimit,
  89     process->get_malloc_info());
  90
  91   MC_process_smx_refresh(&mc_model_checker->process());
  92   pair->nb_processes =
  93     mc_model_checker->process().smx_process_infos.size();
  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), nullptr);
 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 = nullptr;
 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 = nullptr;
 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 if (heap_bytes_used_test < heap_bytes_used)
 180       start = cursor + 1;
 181     else if (heap_bytes_used_test > heap_bytes_used)
 182       end = cursor - 1;
 183     else {
 184         *min = *max = cursor;
 185         previous_cursor = cursor - 1;
 186         while (previous_cursor >= 0) {
 187           if (_sg_mc_liveness) {
 188             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
 189             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 190             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 191           } else {
 192             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
 193             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 194             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 195           }
 196           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 197             break;
 198           *min = previous_cursor;
 199           previous_cursor--;
 200         }
 201         size_t next_cursor = cursor + 1;
 202         while (next_cursor < xbt_dynar_length(list)) {
 203           if (_sg_mc_liveness) {
 204             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
 205             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 206             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 207           } else {
 208             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
 209             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 210             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 211           }
 212           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 213             break;
 214           *max = next_cursor;
 215           next_cursor++;
 216         }
 217         return -1;
 218     }
 219   }
 220   return cursor;
 221 }
 222
 223 static
 224 void replace_state(
 225   mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor)
 226 {
 227   if (state_test->other_num == -1)
 228     new_state->other_num = state_test->num;
 229   else
 230     new_state->other_num = state_test->other_num;
 231
 232   if (dot_output == nullptr)
 233     XBT_DEBUG("State %d already visited ! (equal to state %d)",
 234       new_state->num, state_test->num);
 235   else
 236     XBT_DEBUG(
 237       "State %d already visited ! (equal to state %d (state %d in dot_output))",
 238       new_state->num, state_test->num, new_state->other_num);
 239
 240   /* Replace the old state with the new one (with a bigger num)
 241      (when the max number of visited states is reached,  the oldest
 242      one is removed according to its number (= with the min number) */
 243   xbt_dynar_remove_at(visited_states, cursor, nullptr);
 244   xbt_dynar_insert_at(visited_states, cursor, &new_state);
 245   XBT_DEBUG("Replace visited state %d with the new visited state %d",
 246     state_test->num, new_state->num);
 247 }
 248
 249 static
 250 bool some_dommunications_are_not_finished()
 251 {
 252   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 253     xbt_dynar_t pattern = xbt_dynar_get_as(
 254       incomplete_communications_pattern, current_process, xbt_dynar_t);
 255     if (!xbt_dynar_is_empty(pattern)) {
 256       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 257       return true;
 258     }
 259   }
 260   return false;
 261 }
 262
 263 /**
 264  * \brief Checks whether a given state has already been visited by the algorithm.
 265  */
 266
 267 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 268 {
 269   if (_sg_mc_visited == 0)
 270     return nullptr;
 271
 272   /* If comm determinism verification, we cannot stop the exploration if some
 273      communications are not finished (at least, data are transfered). These communications
 274      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 275   int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
 276     some_dommunications_are_not_finished();
 277
 278   mc_visited_state_t new_state = visited_state_new();
 279   graph_state->system_state = new_state->system_state;
 280   graph_state->in_visited_states = 1;
 281   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 282
 283   if (xbt_dynar_is_empty(visited_states)) {
 284     xbt_dynar_push(visited_states, &new_state);
 285     return nullptr;
 286   }
 287
 288     int min = -1, max = -1, index;
 289
 290     index = get_search_interval(visited_states, new_state, &min, &max);
 291
 292     if (min != -1 && max != -1) {
 293
 294       // Parallell implementation
 295       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 296          if(res != -1){
 297          mc_visited_state_t state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 298          if(state_test->other_num == -1)
 299          new_state->other_num = state_test->num;
 300          else
 301          new_state->other_num = state_test->other_num;
 302          if(dot_output == nullptr)
 303          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 304          else
 305          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);
 306          xbt_dynar_remove_at(visited_states, (min + res) - 1, nullptr);
 307          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 308          return new_state->other_num;
 309          } */
 310
 311       if (_sg_mc_safety || (!partial_comm
 312         && initial_global_state->initial_communications_pattern_done)) {
 313
 314         int cursor = min;
 315         while (cursor <= max) {
 316           mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 317           if (snapshot_compare(state_test, new_state) == 0) {
 318             // The state has been visited:
 319
 320             replace_state(state_test, new_state, cursor);
 321             return state_test;
 322           }
 323           cursor++;
 324         }
 325       }
 326
 327       xbt_dynar_insert_at(visited_states, min, &new_state);
 328       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 329
 330     } else {
 331
 332       // The state has not been visited: insert the state in the dynamic array.
 333       mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 334       if (state_test->nb_processes < new_state->nb_processes)
 335         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 336       else 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        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 342
 343     }
 344
 345   if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
 346     return nullptr;
 347
 348   // We have reached the maximum number of stored states;
 349
 350       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 351
 352       // Find the (index of the) older state (with the smallest num):
 353       int min2 = mc_stats->expanded_states;
 354       unsigned int cursor2 = 0;
 355       unsigned int index2 = 0;
 356
 357       mc_visited_state_t state_test;
 358       xbt_dynar_foreach(visited_states, cursor2, state_test)
 359         if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
 360             && state_test->num < min2) {
 361           index2 = cursor2;
 362           min2 = state_test->num;
 363         }
 364
 365       // and drop it:
 366       xbt_dynar_remove_at(visited_states, index2, nullptr);
 367       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 368
 369     return nullptr;
 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   mc_visited_pair_t new_visited_pair = nullptr;
 381   if (visited_pair == nullptr)
 382     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 383   else
 384     new_visited_pair = visited_pair;
 385
 386   if (xbt_dynar_is_empty(visited_pairs)) {
 387     xbt_dynar_push(visited_pairs, &new_visited_pair);
 388     return -1;
 389   }
 390
 391     int min = -1, max = -1, index;
 392     //int res;
 393     mc_visited_pair_t pair_test;
 394     int cursor;
 395
 396     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 397
 398     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 399       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 400          if(res != -1){
 401          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 402          if(pair_test->other_num == -1)
 403          pair->other_num = pair_test->num;
 404          else
 405          pair->other_num = pair_test->other_num;
 406          if(dot_output == nullptr)
 407          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 408          else
 409          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 410          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, nullptr);
 411          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 412          pair_test->visited_removed = 1;
 413          if(pair_test->stack_removed && pair_test->visited_removed){
 414          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 415          if(pair_test->acceptance_removed){
 416          MC_pair_delete(pair_test);
 417          }
 418          }else{
 419          MC_pair_delete(pair_test);
 420          }
 421          }
 422          return pair->other_num;
 423          } */
 424       cursor = min;
 425       while (cursor <= max) {
 426         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 427         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 428           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 429             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 430               if (pair_test->other_num == -1)
 431                 new_visited_pair->other_num = pair_test->num;
 432               else
 433                 new_visited_pair->other_num = pair_test->other_num;
 434               if (dot_output == nullptr)
 435                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 436               else
 437                 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);
 438               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 439               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 440               pair_test->visited_removed = 1;
 441               if (!pair_test->acceptance_pair
 442                   || pair_test->acceptance_removed == 1)
 443                 MC_visited_pair_delete(pair_test);
 444               return new_visited_pair->other_num;
 445             }
 446           }
 447         }
 448         cursor++;
 449       }
 450       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 451     } else {
 452       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 453       if (pair_test->nb_processes < new_visited_pair->nb_processes)
 454         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 455       else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 456         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 457       else
 458         xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 459     }
 460
 461     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 462       int min2 = mc_stats->expanded_pairs;
 463       unsigned int cursor2 = 0;
 464       unsigned int index2 = 0;
 465       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 466         if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
 467             && pair_test->num < min2) {
 468           index2 = cursor2;
 469           min2 = pair_test->num;
 470         }
 471       }
 472       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 473       pair_test->visited_removed = 1;
 474       if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
 475         MC_visited_pair_delete(pair_test);
 476     }
 477   return -1;
 478 }
 479
 480 }