src/mc/mc_dpor.c

   1 /* Copyright (c) 2008-2013. 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 "mc_private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /********** Global variables **********/
  13
  14 xbt_dynar_t visited_states;
  15 xbt_dict_t first_enabled_state;
  16
  17 /********** Static functions ***********/
  18
  19 static void visited_state_free(mc_visited_state_t state){
  20   if(state){
  21     MC_free_snapshot(state->system_state);
  22     xbt_free(state);
  23   }
  24 }
  25
  26 static void visited_state_free_voidp(void *s){
  27   visited_state_free((mc_visited_state_t) * (void **) s);
  28 }
  29
  30 static mc_visited_state_t visited_state_new(){
  31
  32   mc_visited_state_t new_state = NULL;
  33   new_state = xbt_new0(s_mc_visited_state_t, 1);
  34   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
  35   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
  36   new_state->system_state = MC_take_snapshot();
  37   new_state->num = mc_stats->expanded_states;
  38   new_state->other_num = -1;
  39
  40   return new_state;
  41
  42 }
  43
  44 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
  45
  46   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  47
  48   MC_SET_RAW_MEM;
  49
  50   int cursor = 0, previous_cursor, next_cursor;
  51   mc_visited_state_t state_test;
  52   int start = 0;
  53   int end = xbt_dynar_length(all_states) - 1;
  54
  55   while(start <= end){
  56     cursor = (start + end) / 2;
  57     state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
  58     if(state_test->nb_processes < state->nb_processes){
  59       start = cursor + 1;
  60     }else if(state_test->nb_processes > state->nb_processes){
  61       end = cursor - 1;
  62     }else{
  63       if(state_test->heap_bytes_used < state->heap_bytes_used){
  64         start = cursor +1;
  65       }else if(state_test->heap_bytes_used > state->heap_bytes_used){
  66         end = cursor - 1;
  67       }else{
  68         *min = *max = cursor;
  69         previous_cursor = cursor - 1;
  70         while(previous_cursor >= 0){
  71           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
  72           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
  73             break;
  74           *min = previous_cursor;
  75           previous_cursor--;
  76         }
  77         next_cursor = cursor + 1;
  78         while(next_cursor < xbt_dynar_length(all_states)){
  79           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
  80           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
  81             break;
  82           *max = next_cursor;
  83           next_cursor++;
  84         }
  85         if(!raw_mem_set)
  86           MC_UNSET_RAW_MEM;
  87         return -1;
  88       }
  89      }
  90   }
  91
  92   if(!raw_mem_set)
  93     MC_UNSET_RAW_MEM;
  94
  95   return cursor;
  96 }
  97
  98 static int is_visited_state(){
  99
 100   if(_sg_mc_visited == 0)
 101     return -1;
 102
 103   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 104
 105   MC_SET_RAW_MEM;
 106
 107   mc_visited_state_t new_state = visited_state_new();
 108
 109   if(xbt_dynar_is_empty(visited_states)){
 110
 111     xbt_dynar_push(visited_states, &new_state);
 112
 113     if(!raw_mem_set)
 114       MC_UNSET_RAW_MEM;
 115
 116     return -1;
 117
 118   }else{
 119
 120     int min = -1, max = -1, index;
 121     //int res;
 122     mc_visited_state_t state_test;
 123     int cursor;
 124
 125     index = get_search_interval(visited_states, new_state, &min, &max);
 126
 127     if(min != -1 && max != -1){
 128       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 129       if(res != -1){
 130         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 131         if(state_test->other_num == -1)
 132           new_state->other_num = state_test->num;
 133         else
 134           new_state->other_num = state_test->other_num;
 135         if(dot_output == NULL)
 136           XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 137         else
 138           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);
 139         xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 140         xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 141         if(!raw_mem_set)
 142           MC_UNSET_RAW_MEM;
 143         return new_state->other_num;
 144         }*/
 145       cursor = min;
 146       while(cursor <= max){
 147         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 148         if(snapshot_compare(state_test, new_state) == 0){
 149           if(state_test->other_num == -1)
 150             new_state->other_num = state_test->num;
 151           else
 152             new_state->other_num = state_test->other_num;
 153           if(dot_output == NULL)
 154             XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 155           else
 156             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);
 157           xbt_dynar_remove_at(visited_states, cursor, NULL);
 158           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 159           if(!raw_mem_set)
 160             MC_UNSET_RAW_MEM;
 161           return new_state->other_num;
 162         }
 163         cursor++;
 164       }
 165       xbt_dynar_insert_at(visited_states, min, &new_state);
 166     }else{
 167       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 168       if(state_test->nb_processes < new_state->nb_processes){
 169         xbt_dynar_insert_at(visited_states, index+1, &new_state);
 170       }else{
 171         if(state_test->heap_bytes_used < new_state->heap_bytes_used)
 172           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 173         else
 174           xbt_dynar_insert_at(visited_states, index, &new_state);
 175       }
 176     }
 177
 178     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
 179       int min2 = mc_stats->expanded_states;
 180       unsigned int cursor2 = 0;
 181       unsigned int index2 = 0;
 182       xbt_dynar_foreach(visited_states, cursor2, state_test){
 183         if(state_test->num < min2){
 184           index2 = cursor2;
 185           min2 = state_test->num;
 186         }
 187       }
 188       xbt_dynar_remove_at(visited_states, index2, NULL);
 189     }
 190
 191     if(!raw_mem_set)
 192       MC_UNSET_RAW_MEM;
 193
 194     return -1;
 195
 196   }
 197 }
 198
 199 /**
 200  *  \brief Initialize the DPOR exploration algorithm
 201  */
 202 void MC_dpor_init()
 203 {
 204
 205   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 206
 207   mc_state_t initial_state = NULL;
 208   smx_process_t process;
 209
 210   /* Create the initial state and push it into the exploration stack */
 211   MC_SET_RAW_MEM;
 212
 213   initial_state = MC_state_new();
 214   if(_sg_mc_visited > 0)
 215     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 216
 217   first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
 218
 219   MC_UNSET_RAW_MEM;
 220
 221   XBT_DEBUG("**************************************************");
 222   XBT_DEBUG("Initial state");
 223
 224   /* Wait for requests (schedules processes) */
 225   MC_wait_for_requests();
 226
 227   MC_SET_RAW_MEM;
 228
 229   /* Get an enabled process and insert it in the interleave set of the initial state */
 230   xbt_swag_foreach(process, simix_global->process_list){
 231     if(MC_process_is_enabled(process)){
 232       MC_state_interleave_process(initial_state, process);
 233       if(mc_reduce_kind != e_mc_reduce_none)
 234         break;
 235     }
 236   }
 237
 238   xbt_fifo_unshift(mc_stack_safety, initial_state);
 239
 240   /* To ensure the soundness of DPOR, we have to keep a list of
 241      processes which are still enabled at each step of the exploration.
 242      If max depth is reached, we interleave them in the state in which they have
 243      been enabled for the first time. */
 244   xbt_swag_foreach(process, simix_global->process_list){
 245     if(MC_process_is_enabled(process)){
 246       char *key = bprintf("%lu", process->pid);
 247       char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 248       xbt_dict_set(first_enabled_state, key, data, NULL);
 249       xbt_free(key);
 250     }
 251   }
 252
 253   MC_UNSET_RAW_MEM;
 254
 255   if(raw_mem_set)
 256     MC_SET_RAW_MEM;
 257   else
 258     MC_UNSET_RAW_MEM;
 259
 260 }
 261
 262
 263 /**
 264  *   \brief Perform the model-checking operation using a depth-first search exploration
 265  *         with Dynamic Partial Order Reductions
 266  */
 267 void MC_dpor(void)
 268 {
 269
 270   char *req_str = NULL;
 271   int value;
 272   smx_simcall_t req = NULL, prev_req = NULL;
 273   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
 274   smx_process_t process = NULL;
 275   xbt_fifo_item_t item = NULL;
 276   int pos;
 277   int visited_state = -1;
 278   int enabled = 0;
 279
 280   while (xbt_fifo_size(mc_stack_safety) > 0) {
 281
 282     /* Get current state */
 283     state = (mc_state_t)
 284       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 285
 286     XBT_DEBUG("**************************************************");
 287     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
 288               xbt_fifo_size(mc_stack_safety), state, state->num,
 289               MC_state_interleave_size(state), user_max_depth_reached);
 290
 291     /* Update statistics */
 292     mc_stats->visited_states++;
 293
 294     /* If there are processes to interleave and the maximum depth has not been reached
 295        then perform one step of the exploration algorithm */
 296     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
 297         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 298
 299       /* Debug information */
 300       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 301         req_str = MC_request_to_string(req, value);
 302         XBT_DEBUG("Execute: %s", req_str);
 303         xbt_free(req_str);
 304       }
 305
 306       MC_SET_RAW_MEM;
 307       if(dot_output != NULL)
 308         req_str = MC_request_get_dot_output(req, value);
 309       MC_UNSET_RAW_MEM;
 310
 311       MC_state_set_executed_request(state, req, value);
 312       mc_stats->executed_transitions++;
 313
 314       MC_SET_RAW_MEM;
 315       char *key = bprintf("%lu", req->issuer->pid);
 316       xbt_dict_remove(first_enabled_state, key);
 317       xbt_free(key);
 318       MC_UNSET_RAW_MEM;
 319
 320       /* Answer the request */
 321       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 322
 323       /* Wait for requests (schedules processes) */
 324       MC_wait_for_requests();
 325
 326       /* Create the new expanded state */
 327       MC_SET_RAW_MEM;
 328
 329       next_state = MC_state_new();
 330
 331       if((visited_state = is_visited_state()) == -1){
 332
 333         /* Get an enabled process and insert it in the interleave set of the next state */
 334         xbt_swag_foreach(process, simix_global->process_list){
 335           if(MC_process_is_enabled(process)){
 336             MC_state_interleave_process(next_state, process);
 337             if(mc_reduce_kind != e_mc_reduce_none)
 338               break;
 339           }
 340         }
 341
 342         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 343           next_state->system_state = MC_take_snapshot();
 344         }
 345
 346         if(dot_output != NULL)
 347           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 348
 349       }else{
 350
 351         if(dot_output != NULL)
 352           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
 353
 354       }
 355
 356       xbt_fifo_unshift(mc_stack_safety, next_state);
 357
 358       /* Insert in dict all enabled processes, if not included yet */
 359       xbt_swag_foreach(process, simix_global->process_list){
 360         if(MC_process_is_enabled(process)){
 361           char *key = bprintf("%lu", process->pid);
 362           if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
 363             char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 364             xbt_dict_set(first_enabled_state, key, data, NULL);
 365           }
 366           xbt_free(key);
 367         }
 368       }
 369
 370       if(dot_output != NULL)
 371         xbt_free(req_str);
 372
 373       MC_UNSET_RAW_MEM;
 374
 375       /* Let's loop again */
 376
 377       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 378     } else {
 379
 380       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
 381
 382         if(user_max_depth_reached && visited_state == -1)
 383           XBT_DEBUG("User max depth reached !");
 384         else if(visited_state == -1)
 385           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 386
 387         visited_state = -1;
 388
 389         /* Interleave enabled processes in the state in which they have been enabled for the first time */
 390         xbt_swag_foreach(process, simix_global->process_list){
 391           if(MC_process_is_enabled(process)){
 392             char *key = bprintf("%lu", process->pid);
 393             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 394             xbt_free(key);
 395             mc_state_t state_test = NULL;
 396             xbt_fifo_item_t item = NULL;
 397             int cursor = xbt_fifo_size(mc_stack_safety);
 398             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 399               if(cursor-- == enabled){
 400                 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
 401                   XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
 402                   MC_state_interleave_process(state_test, process);
 403                   break;
 404                 }
 405               }
 406             }
 407           }
 408         }
 409
 410       }else{
 411
 412         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 413
 414       }
 415
 416       /* Trash the current state, no longer needed */
 417       MC_SET_RAW_MEM;
 418       xbt_fifo_shift(mc_stack_safety);
 419       MC_state_delete(state);
 420       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 421       MC_UNSET_RAW_MEM;
 422
 423       /* Check for deadlocks */
 424       if(MC_deadlock_check()){
 425         MC_show_deadlock(NULL);
 426         return;
 427       }
 428
 429       MC_SET_RAW_MEM;
 430       /* Traverse the stack backwards until a state with a non empty interleave
 431          set is found, deleting all the states that have it empty in the way.
 432          For each deleted state, check if the request that has generated it
 433          (from it's predecesor state), depends on any other previous request
 434          executed before it. If it does then add it to the interleave set of the
 435          state that executed that previous request. */
 436
 437       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 438         if(mc_reduce_kind != e_mc_reduce_none){
 439           req = MC_state_get_internal_request(state);
 440           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 441             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 442               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 443                 XBT_DEBUG("Dependent Transitions:");
 444                 prev_req = MC_state_get_executed_request(prev_state, &value);
 445                 req_str = MC_request_to_string(prev_req, value);
 446                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 447                 xbt_free(req_str);
 448                 prev_req = MC_state_get_executed_request(state, &value);
 449                 req_str = MC_request_to_string(prev_req, value);
 450                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 451                 xbt_free(req_str);
 452               }
 453
 454               if(!MC_state_process_is_done(prev_state, req->issuer))
 455                 MC_state_interleave_process(prev_state, req->issuer);
 456               else
 457                 XBT_DEBUG("Process %p is in done set", req->issuer);
 458
 459               break;
 460
 461             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 462
 463               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 464               break;
 465
 466             }else{
 467
 468               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
 469
 470             }
 471           }
 472         }
 473
 474         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 475           /* We found a back-tracking point, let's loop */
 476           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 477           if(_sg_mc_checkpoint){
 478             if(state->system_state != NULL){
 479               MC_restore_snapshot(state->system_state);
 480               xbt_fifo_unshift(mc_stack_safety, state);
 481               MC_UNSET_RAW_MEM;
 482             }else{
 483               pos = xbt_fifo_size(mc_stack_safety);
 484               item = xbt_fifo_get_first_item(mc_stack_safety);
 485               while(pos>0){
 486                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 487                 if(restore_state->system_state != NULL){
 488                   break;
 489                 }else{
 490                   item = xbt_fifo_get_next_item(item);
 491                   pos--;
 492                 }
 493               }
 494               MC_restore_snapshot(restore_state->system_state);
 495               xbt_fifo_unshift(mc_stack_safety, state);
 496               MC_UNSET_RAW_MEM;
 497               MC_replay(mc_stack_safety, pos);
 498             }
 499           }else{
 500             xbt_fifo_unshift(mc_stack_safety, state);
 501             MC_UNSET_RAW_MEM;
 502             MC_replay(mc_stack_safety, -1);
 503           }
 504           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
 505           break;
 506         } else {
 507           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 508           MC_state_delete(state);
 509         }
 510       }
 511       MC_UNSET_RAW_MEM;
 512     }
 513   }
 514   MC_print_statistics(mc_stats);
 515   MC_UNSET_RAW_MEM;
 516
 517   return;
 518 }
 519
 520
 521
 522