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         MC_UNSET_RAW_MEM;
 399
 400         max_depth_reached = 0;
 401       }
 402
 403       /* Check for deadlocks */
 404       if(MC_deadlock_check()){
 405         MC_show_deadlock(NULL);
 406         return;
 407       }
 408
 409       MC_SET_RAW_MEM;
 410       /* Traverse the stack backwards until a state with a non empty interleave
 411          set is found, deleting all the states that have it empty in the way.
 412          For each deleted state, check if the request that has generated it
 413          (from it's predecesor state), depends on any other previous request
 414          executed before it. If it does then add it to the interleave set of the
 415          state that executed that previous request. */
 416
 417       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 418         if(mc_reduce_kind != e_mc_reduce_none){
 419           if((xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth) && max_depth_reached){
 420             req = MC_state_get_request(state, &value);
 421             MC_state_set_executed_request(state, req, value);
 422           }
 423           req = MC_state_get_internal_request(state);
 424           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 425             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 426               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 427                 XBT_DEBUG("Dependent Transitions:");
 428                 prev_req = MC_state_get_executed_request(prev_state, &value);
 429                 req_str = MC_request_to_string(prev_req, value);
 430                 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 431                 xbt_free(req_str);
 432                 prev_req = MC_state_get_executed_request(state, &value);
 433                 req_str = MC_request_to_string(prev_req, value);
 434                 XBT_DEBUG("%s (state=%p)", req_str, state);
 435                 xbt_free(req_str);
 436               }
 437
 438               if(!MC_state_process_is_done(prev_state, req->issuer))
 439                 MC_state_interleave_process(prev_state, req->issuer);
 440               else
 441                 XBT_DEBUG("Process %p is in done set", req->issuer);
 442
 443               break;
 444
 445             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 446
 447               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 448               break;
 449
 450             }
 451           }
 452         }
 453
 454         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 455           /* We found a back-tracking point, let's loop */
 456           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety) + 1);
 457           if(_sg_mc_checkpoint){
 458             if(state->system_state != NULL){
 459               MC_restore_snapshot(state->system_state);
 460               xbt_fifo_unshift(mc_stack_safety, state);
 461               MC_UNSET_RAW_MEM;
 462             }else{
 463               pos = xbt_fifo_size(mc_stack_safety);
 464               item = xbt_fifo_get_first_item(mc_stack_safety);
 465               while(pos>0){
 466                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 467                 if(restore_state->system_state != NULL){
 468                   break;
 469                 }else{
 470                   item = xbt_fifo_get_next_item(item);
 471                   pos--;
 472                 }
 473               }
 474               MC_restore_snapshot(restore_state->system_state);
 475               xbt_fifo_unshift(mc_stack_safety, state);
 476               MC_UNSET_RAW_MEM;
 477               MC_replay(mc_stack_safety, pos);
 478             }
 479           }else{
 480             xbt_fifo_unshift(mc_stack_safety, state);
 481             MC_UNSET_RAW_MEM;
 482             MC_replay(mc_stack_safety, -1);
 483           }
 484           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 485           break;
 486         } else {
 487           XBT_DEBUG("Delete state at depth %d",xbt_fifo_size(mc_stack_safety) + 1);
 488           MC_state_delete(state);
 489         }
 490       }
 491       MC_UNSET_RAW_MEM;
 492     }
 493   }
 494   MC_print_statistics(mc_stats);
 495   MC_UNSET_RAW_MEM;
 496
 497   return;
 498 }
 499
 500
 501
 502