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