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 /**
  12  *  \brief Initialize the DPOR exploration algorithm
  13  */
  14 void MC_dpor_init()
  15 {
  16   mc_state_t initial_state = NULL;
  17   smx_process_t process;
  18
  19   /* Create the initial state and push it into the exploration stack */
  20   MC_SET_RAW_MEM;
  21   initial_state = MC_state_new();
  22   MC_UNSET_RAW_MEM;
  23
  24   XBT_DEBUG("**************************************************");
  25   XBT_DEBUG("Initial state");
  26
  27   /* Wait for requests (schedules processes) */
  28   MC_wait_for_requests();
  29
  30   MC_SET_RAW_MEM;
  31   /* Get an enabled process and insert it in the interleave set of the initial state */
  32   xbt_swag_foreach(process, simix_global->process_list){
  33     if(MC_process_is_enabled(process)){
  34       MC_state_interleave_process(initial_state, process);
  35       break;
  36     }
  37   }
  38
  39   initial_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
  40   MC_take_snapshot(initial_state->system_state);
  41
  42   xbt_fifo_unshift(mc_stack_safety, initial_state);
  43
  44   MC_UNSET_RAW_MEM;
  45
  46   /* FIXME: Update Statistics
  47      mc_stats->state_size +=
  48      xbt_setset_set_size(initial_state->enabled_transitions); */
  49 }
  50
  51
  52 /**
  53  *   \brief Perform the model-checking operation using a depth-first search exploration
  54  *         with Dynamic Partial Order Reductions
  55  */
  56 void MC_dpor(void)
  57 {
  58   char *req_str;
  59   int value;
  60   smx_simcall_t req = NULL, prev_req = NULL;
  61   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
  62   smx_process_t process = NULL;
  63   xbt_fifo_item_t item = NULL;
  64   int pos;
  65
  66   while (xbt_fifo_size(mc_stack_safety) > 0) {
  67
  68     /* Get current state */
  69     state = (mc_state_t)
  70       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
  71
  72     XBT_DEBUG("**************************************************");
  73     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
  74               xbt_fifo_size(mc_stack_safety), state,
  75               MC_state_interleave_size(state));
  76
  77     /* Update statistics */
  78     mc_stats->visited_states++;
  79
  80     /* If there are processes to interleave and the maximum depth has not been reached
  81        then perform one step of the exploration algorithm */
  82     if (xbt_fifo_size(mc_stack_safety) < MAX_DEPTH &&
  83         (req = MC_state_get_request(state, &value))) {
  84
  85       /* Debug information */
  86       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  87         req_str = MC_request_to_string(req, value);
  88         XBT_DEBUG("Execute: %s", req_str);
  89         xbt_free(req_str);
  90       }
  91
  92       MC_state_set_executed_request(state, req, value);
  93       mc_stats->executed_transitions++;
  94
  95       /* Answer the request */
  96       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
  97
  98       /* Wait for requests (schedules processes) */
  99       MC_wait_for_requests();
 100
 101       /* Create the new expanded state */
 102       MC_SET_RAW_MEM;
 103
 104       next_state = MC_state_new();
 105
 106       /* Get an enabled process and insert it in the interleave set of the next state */
 107       xbt_swag_foreach(process, simix_global->process_list){
 108         if(MC_process_is_enabled(process)){
 109           MC_state_interleave_process(next_state, process);
 110           break;
 111         }
 112       }
 113
 114       if(_surf_do_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_do_mc_checkpoint == 0)){
 115         next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
 116         MC_take_snapshot(next_state->system_state);
 117       }
 118
 119       xbt_fifo_unshift(mc_stack_safety, next_state);
 120       MC_UNSET_RAW_MEM;
 121
 122       /* FIXME: Update Statistics
 123          mc_stats->state_size +=
 124          xbt_setset_set_size(next_state->enabled_transitions);*/
 125
 126       /* Let's loop again */
 127
 128       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 129     } else {
 130       XBT_DEBUG("There are no more processes to interleave.");
 131
 132       /* Trash the current state, no longer needed */
 133       MC_SET_RAW_MEM;
 134       xbt_fifo_shift(mc_stack_safety);
 135       MC_state_delete(state);
 136       MC_UNSET_RAW_MEM;
 137
 138       /* Check for deadlocks */
 139       if(MC_deadlock_check()){
 140         MC_show_deadlock(NULL);
 141         return;
 142       }
 143
 144       MC_SET_RAW_MEM;
 145       /* Traverse the stack backwards until a state with a non empty interleave
 146          set is found, deleting all the states that have it empty in the way.
 147          For each deleted state, check if the request that has generated it
 148          (from it's predecesor state), depends on any other previous request
 149          executed before it. If it does then add it to the interleave set of the
 150          state that executed that previous request. */
 151       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 152         req = MC_state_get_internal_request(state);
 153         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 154           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 155             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 156               XBT_DEBUG("Dependent Transitions:");
 157               prev_req = MC_state_get_executed_request(prev_state, &value);
 158               req_str = MC_request_to_string(prev_req, value);
 159               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 160               xbt_free(req_str);
 161               prev_req = MC_state_get_executed_request(state, &value);
 162               req_str = MC_request_to_string(prev_req, value);
 163               XBT_DEBUG("%s (state=%p)", req_str, state);
 164               xbt_free(req_str);
 165             }
 166
 167             if(!MC_state_process_is_done(prev_state, req->issuer))
 168               MC_state_interleave_process(prev_state, req->issuer);
 169             else
 170               XBT_DEBUG("Process %p is in done set", req->issuer);
 171
 172             break;
 173           }
 174         }
 175         if (MC_state_interleave_size(state)) {
 176           /* We found a back-tracking point, let's loop */
 177           if(_surf_do_mc_checkpoint){
 178             if(state->system_state != NULL){
 179               MC_restore_snapshot(state->system_state);
 180               xbt_fifo_unshift(mc_stack_safety, state);
 181               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 182               MC_UNSET_RAW_MEM;
 183             }else{
 184               pos = xbt_fifo_size(mc_stack_safety);
 185               item = xbt_fifo_get_first_item(mc_stack_safety);
 186               while(pos>0){
 187                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 188                 if(restore_state->system_state != NULL){
 189                   break;
 190                 }else{
 191                   item = xbt_fifo_get_next_item(item);
 192                   pos--;
 193                 }
 194               }
 195               MC_restore_snapshot(restore_state->system_state);
 196               xbt_fifo_unshift(mc_stack_safety, state);
 197               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 198               MC_UNSET_RAW_MEM;
 199               MC_replay(mc_stack_safety, pos);
 200             }
 201           }else{
 202             xbt_fifo_unshift(mc_stack_safety, state);
 203             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 204             MC_UNSET_RAW_MEM;
 205             MC_replay(mc_stack_safety, -1);
 206           }
 207           break;
 208         } else {
 209           MC_state_delete(state);
 210         }
 211       }
 212       MC_UNSET_RAW_MEM;
 213     }
 214   }
 215   MC_print_statistics(mc_stats);
 216   MC_UNSET_RAW_MEM;
 217   return;
 218 }
 219
 220
 221
 222