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