src/mc/mc_dpor.c

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