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(mc_stats->expanded_states);
  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_ignore_heap(simix_global->process_to_run->data, 0);
 228   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 229
 230   MC_SET_RAW_MEM;
 231
 232   /* Get an enabled process and insert it in the interleave set of the initial state */
 233   xbt_swag_foreach(process, simix_global->process_list){
 234     if(MC_process_is_enabled(process)){
 235       MC_state_interleave_process(initial_state, process);
 236       if(mc_reduce_kind != e_mc_reduce_none)
 237         break;
 238     }
 239   }
 240
 241   xbt_fifo_unshift(mc_stack_safety, initial_state);
 242
 243   /* To ensure the soundness of DPOR, we have to keep a list of
 244      processes which are still enabled at each step of the exploration.
 245      If max depth is reached, we interleave them in the state in which they have
 246      been enabled for the first time. */
 247   xbt_swag_foreach(process, simix_global->process_list){
 248     if(MC_process_is_enabled(process)){
 249       char *key = bprintf("%lu", process->pid);
 250       char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 251       xbt_dict_set(first_enabled_state, key, data, NULL);
 252       xbt_free(key);
 253     }
 254   }
 255
 256   MC_UNSET_RAW_MEM;
 257
 258   if(raw_mem_set)
 259     MC_SET_RAW_MEM;
 260   else
 261     MC_UNSET_RAW_MEM;
 262
 263 }
 264
 265
 266 /**
 267  *   \brief Perform the model-checking operation using a depth-first search exploration
 268  *         with Dynamic Partial Order Reductions
 269  */
 270 void MC_dpor(void)
 271 {
 272
 273   char *req_str = NULL;
 274   int value;
 275   smx_simcall_t req = NULL, prev_req = NULL;
 276   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
 277   smx_process_t process = NULL;
 278   xbt_fifo_item_t item = NULL;
 279   mc_state_t state_test = NULL;
 280   int pos;
 281   int visited_state = -1;
 282   int enabled = 0;
 283
 284   while (xbt_fifo_size(mc_stack_safety) > 0) {
 285
 286     /* Get current state */
 287     state = (mc_state_t)
 288       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 289
 290     XBT_DEBUG("**************************************************");
 291     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
 292               xbt_fifo_size(mc_stack_safety), state, state->num,
 293               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
 294
 295     /* Update statistics */
 296     mc_stats->visited_states++;
 297
 298     /* If there are processes to interleave and the maximum depth has not been reached
 299        then perform one step of the exploration algorithm */
 300     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
 301         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 302
 303       /* Debug information */
 304       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 305         req_str = MC_request_to_string(req, value);
 306         XBT_DEBUG("Execute: %s", req_str);
 307         xbt_free(req_str);
 308       }
 309
 310       MC_SET_RAW_MEM;
 311       if(dot_output != NULL)
 312         req_str = MC_request_get_dot_output(req, value);
 313       MC_UNSET_RAW_MEM;
 314
 315       MC_state_set_executed_request(state, req, value);
 316       mc_stats->executed_transitions++;
 317
 318       MC_SET_RAW_MEM;
 319       char *key = bprintf("%lu", req->issuer->pid);
 320       xbt_dict_remove(first_enabled_state, key);
 321       xbt_free(key);
 322       MC_UNSET_RAW_MEM;
 323
 324       /* Answer the request */
 325       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 326
 327       /* Wait for requests (schedules processes) */
 328       MC_wait_for_requests();
 329
 330       /* Create the new expanded state */
 331       MC_SET_RAW_MEM;
 332
 333       next_state = MC_state_new();
 334
 335       if((visited_state = is_visited_state()) == -1){
 336
 337         /* Get an enabled process and insert it in the interleave set of the next state */
 338         xbt_swag_foreach(process, simix_global->process_list){
 339           if(MC_process_is_enabled(process)){
 340             MC_state_interleave_process(next_state, process);
 341             if(mc_reduce_kind != e_mc_reduce_none)
 342               break;
 343           }
 344         }
 345
 346         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 347           next_state->system_state = MC_take_snapshot(next_state->num);
 348         }
 349
 350         if(dot_output != NULL)
 351           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 352
 353       }else{
 354
 355         if(dot_output != NULL)
 356           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
 357
 358       }
 359
 360       xbt_fifo_unshift(mc_stack_safety, next_state);
 361
 362       /* Insert in dict all enabled processes, if not included yet */
 363       xbt_swag_foreach(process, simix_global->process_list){
 364         if(MC_process_is_enabled(process)){
 365           char *key = bprintf("%lu", process->pid);
 366           if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
 367             char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 368             xbt_dict_set(first_enabled_state, key, data, NULL);
 369           }
 370           xbt_free(key);
 371         }
 372       }
 373
 374       if(dot_output != NULL)
 375         xbt_free(req_str);
 376
 377       MC_UNSET_RAW_MEM;
 378
 379       /* Let's loop again */
 380
 381       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 382     } else {
 383
 384       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
 385
 386         if(user_max_depth_reached && visited_state == -1)
 387           XBT_DEBUG("User max depth reached !");
 388         else if(visited_state == -1)
 389           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 390
 391         visited_state = -1;
 392
 393         /* Interleave enabled processes in the state in which they have been enabled for the first time */
 394         xbt_swag_foreach(process, simix_global->process_list){
 395           if(MC_process_is_enabled(process)){
 396             char *key = bprintf("%lu", process->pid);
 397             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 398             xbt_free(key);
 399             int cursor = xbt_fifo_size(mc_stack_safety);
 400             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 401               if(cursor-- == enabled){
 402                 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
 403                   XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
 404                   MC_state_interleave_process(state_test, process);
 405                   break;
 406                 }
 407               }
 408             }
 409           }
 410         }
 411
 412       }else{
 413
 414         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 415
 416       }
 417
 418       /* Trash the current state, no longer needed */
 419       MC_SET_RAW_MEM;
 420       xbt_fifo_shift(mc_stack_safety);
 421       MC_state_delete(state);
 422       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 423       MC_UNSET_RAW_MEM;
 424
 425       /* Check for deadlocks */
 426       if(MC_deadlock_check()){
 427         MC_show_deadlock(NULL);
 428         return;
 429       }
 430
 431       MC_SET_RAW_MEM;
 432       /* Traverse the stack backwards until a state with a non empty interleave
 433          set is found, deleting all the states that have it empty in the way.
 434          For each deleted state, check if the request that has generated it
 435          (from it's predecesor state), depends on any other previous request
 436          executed before it. If it does then add it to the interleave set of the
 437          state that executed that previous request. */
 438
 439       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 440         if(mc_reduce_kind != e_mc_reduce_none){
 441           req = MC_state_get_internal_request(state);
 442           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 443             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 444               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 445                 XBT_DEBUG("Dependent Transitions:");
 446                 prev_req = MC_state_get_executed_request(prev_state, &value);
 447                 req_str = MC_request_to_string(prev_req, value);
 448                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 449                 xbt_free(req_str);
 450                 prev_req = MC_state_get_executed_request(state, &value);
 451                 req_str = MC_request_to_string(prev_req, value);
 452                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 453                 xbt_free(req_str);
 454               }
 455
 456               if(!MC_state_process_is_done(prev_state, req->issuer))
 457                 MC_state_interleave_process(prev_state, req->issuer);
 458               else
 459                 XBT_DEBUG("Process %p is in done set", req->issuer);
 460
 461               break;
 462
 463             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 464
 465               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 466               break;
 467
 468             }else{
 469
 470               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);
 471
 472             }
 473           }
 474         }
 475
 476         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 477           /* We found a back-tracking point, let's loop */
 478           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 479           if(_sg_mc_checkpoint){
 480             if(state->system_state != NULL){
 481               MC_restore_snapshot(state->system_state);
 482               xbt_fifo_unshift(mc_stack_safety, state);
 483               MC_UNSET_RAW_MEM;
 484             }else{
 485               pos = xbt_fifo_size(mc_stack_safety);
 486               item = xbt_fifo_get_first_item(mc_stack_safety);
 487               while(pos>0){
 488                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 489                 if(restore_state->system_state != NULL){
 490                   break;
 491                 }else{
 492                   item = xbt_fifo_get_next_item(item);
 493                   pos--;
 494                 }
 495               }
 496               MC_restore_snapshot(restore_state->system_state);
 497               xbt_fifo_unshift(mc_stack_safety, state);
 498               MC_UNSET_RAW_MEM;
 499               MC_replay(mc_stack_safety, pos);
 500             }
 501           }else{
 502             xbt_fifo_unshift(mc_stack_safety, state);
 503             MC_UNSET_RAW_MEM;
 504             MC_replay(mc_stack_safety, -1);
 505           }
 506           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
 507           break;
 508         } else {
 509           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 510           MC_state_delete(state);
 511         }
 512       }
 513       MC_UNSET_RAW_MEM;
 514     }
 515   }
 516   MC_print_statistics(mc_stats);
 517   MC_UNSET_RAW_MEM;
 518
 519   return;
 520 }
 521
 522
 523
 524