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