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