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