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 = 0;
 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)",
 261               xbt_fifo_size(mc_stack_safety), state, state->num,
 262               MC_state_interleave_size(state));
 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 &&
 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){
 354
 355         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 356
 357         /* Interleave enabled processes in the state in which they have been enabled for the first time */
 358         xbt_swag_foreach(process, simix_global->process_list){
 359           if(MC_process_is_enabled(process)){
 360             char *key = bprintf("%lu", process->pid);
 361             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 362             xbt_free(key);
 363             mc_state_t state_test = NULL;
 364             xbt_fifo_item_t item = NULL;
 365             int cursor = xbt_fifo_size(mc_stack_safety);
 366             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 367               if(cursor-- == enabled){
 368                 if(!MC_state_process_is_done(state_test, process)){
 369                   MC_state_interleave_process(state_test, process);
 370                   break;
 371                 }
 372               }
 373             }
 374           }
 375         }
 376
 377         if(MC_state_interleave_size(state) > 0){
 378           max_depth_reached = 1;
 379         }else{
 380           /* Trash the current state, no longer needed */
 381           MC_SET_RAW_MEM;
 382           xbt_fifo_shift(mc_stack_safety);
 383           MC_state_delete(state);
 384           MC_UNSET_RAW_MEM;
 385
 386           max_depth_reached = 0;
 387         }
 388
 389
 390       }else{
 391
 392         XBT_DEBUG("There are no more processes to interleave.");
 393
 394         /* Trash the current state, no longer needed */
 395         MC_SET_RAW_MEM;
 396         xbt_fifo_shift(mc_stack_safety);
 397         MC_state_delete(state);
 398         XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 399         MC_UNSET_RAW_MEM;
 400
 401         max_depth_reached = 0;
 402       }
 403
 404       /* Check for deadlocks */
 405       if(MC_deadlock_check()){
 406         MC_show_deadlock(NULL);
 407         return;
 408       }
 409
 410       MC_SET_RAW_MEM;
 411       /* Traverse the stack backwards until a state with a non empty interleave
 412          set is found, deleting all the states that have it empty in the way.
 413          For each deleted state, check if the request that has generated it
 414          (from it's predecesor state), depends on any other previous request
 415          executed before it. If it does then add it to the interleave set of the
 416          state that executed that previous request. */
 417
 418       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 419         if(mc_reduce_kind != e_mc_reduce_none){
 420           if((xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth) && max_depth_reached){
 421             req = MC_state_get_request(state, &value);
 422             MC_state_set_executed_request(state, req, value);
 423           }
 424           req = MC_state_get_internal_request(state);
 425           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 426             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 427               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 428                 XBT_DEBUG("Dependent Transitions:");
 429                 prev_req = MC_state_get_executed_request(prev_state, &value);
 430                 req_str = MC_request_to_string(prev_req, value);
 431                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 432                 xbt_free(req_str);
 433                 prev_req = MC_state_get_executed_request(state, &value);
 434                 req_str = MC_request_to_string(prev_req, value);
 435                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 436                 xbt_free(req_str);
 437               }
 438
 439               if(!MC_state_process_is_done(prev_state, req->issuer))
 440                 MC_state_interleave_process(prev_state, req->issuer);
 441               else
 442                 XBT_DEBUG("Process %p is in done set", req->issuer);
 443
 444               break;
 445
 446             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 447
 448               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 449               break;
 450
 451             }else{
 452
 453               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);
 454
 455             }
 456           }
 457         }
 458
 459         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 460           /* We found a back-tracking point, let's loop */
 461           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 462           if(_sg_mc_checkpoint){
 463             if(state->system_state != NULL){
 464               MC_restore_snapshot(state->system_state);
 465               xbt_fifo_unshift(mc_stack_safety, state);
 466               MC_UNSET_RAW_MEM;
 467             }else{
 468               pos = xbt_fifo_size(mc_stack_safety);
 469               item = xbt_fifo_get_first_item(mc_stack_safety);
 470               while(pos>0){
 471                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 472                 if(restore_state->system_state != NULL){
 473                   break;
 474                 }else{
 475                   item = xbt_fifo_get_next_item(item);
 476                   pos--;
 477                 }
 478               }
 479               MC_restore_snapshot(restore_state->system_state);
 480               xbt_fifo_unshift(mc_stack_safety, state);
 481               MC_UNSET_RAW_MEM;
 482               MC_replay(mc_stack_safety, pos);
 483             }
 484           }else{
 485             xbt_fifo_unshift(mc_stack_safety, state);
 486             MC_UNSET_RAW_MEM;
 487             MC_replay(mc_stack_safety, -1);
 488           }
 489           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
 490           break;
 491         } else {
 492           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 493           MC_state_delete(state);
 494         }
 495       }
 496       MC_UNSET_RAW_MEM;
 497     }
 498   }
 499   MC_print_statistics(mc_stats);
 500   MC_UNSET_RAW_MEM;
 501
 502   return;
 503 }
 504
 505
 506
 507