src/mc/mc_dpor.c

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