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