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