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