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_print_statistics(mc_stats);
 177   MC_UNSET_RAW_MEM;
 178   return;
 179 }
 180
 181
 182 /********************* DPOR stateful *********************/
 183
 184 mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
 185   mc_state_ws_t sws = NULL;
 186   sws = xbt_new0(s_mc_state_ws_t, 1);
 187   sws->system_state = s;
 188   sws->graph_state = gs;
 189   return sws;
 190 }
 191
 192 void MC_dpor_stateful_init(){
 193
 194   XBT_DEBUG("**************************************************");
 195   XBT_DEBUG("DPOR (stateful) init");
 196   XBT_DEBUG("**************************************************");
 197
 198   mc_state_t initial_graph_state;
 199   smx_process_t process;
 200   mc_snapshot_t initial_system_snapshot;
 201   mc_state_ws_t initial_state ;
 202
 203   MC_wait_for_requests();
 204
 205   MC_SET_RAW_MEM;
 206
 207   initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 208
 209   initial_graph_state = MC_state_new();
 210   xbt_swag_foreach(process, simix_global->process_list){
 211     if(MC_process_is_enabled(process)){
 212       MC_state_interleave_process(initial_graph_state, process);
 213       break;
 214     }
 215   }
 216
 217   MC_take_snapshot(initial_system_snapshot);
 218
 219   initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
 220   xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
 221
 222   MC_UNSET_RAW_MEM;
 223
 224 }
 225
 226 void MC_dpor_stateful(){
 227
 228   smx_process_t process = NULL;
 229
 230   if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
 231     return;
 232
 233   int value;
 234   mc_state_t next_graph_state = NULL;
 235   smx_simcall_t req = NULL, prev_req = NULL;
 236   char *req_str;
 237   xbt_fifo_item_t item = NULL;
 238
 239   mc_snapshot_t next_snapshot;
 240   mc_state_ws_t current_state;
 241   mc_state_ws_t prev_state;
 242   mc_state_ws_t next_state;
 243
 244   while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
 245
 246     current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
 247
 248
 249     XBT_DEBUG("**************************************************");
 250     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));
 251
 252     mc_stats->visited_states++;
 253     if(mc_stats->expanded_states>1100)
 254       exit(0);
 255     //sleep(1);
 256
 257     if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
 258
 259       /* Debug information */
 260       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 261   req_str = MC_request_to_string(req, value);
 262   //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
 263   XBT_DEBUG("Execute: %s",req_str);
 264   xbt_free(req_str);
 265       }
 266
 267       MC_state_set_executed_request(current_state->graph_state, req, value);
 268       mc_stats->executed_transitions++;
 269
 270       /* Answer the request */
 271       SIMIX_simcall_pre(req, value);
 272
 273       /* Wait for requests (schedules processes) */
 274       MC_wait_for_requests();
 275
 276       /* Create the new expanded graph_state */
 277       MC_SET_RAW_MEM;
 278
 279       next_graph_state = MC_state_new();
 280
 281       /* Get an enabled process and insert it in the interleave set of the next graph_state */
 282       xbt_swag_foreach(process, simix_global->process_list){
 283   if(MC_process_is_enabled(process)){
 284     MC_state_interleave_process(next_graph_state, process);
 285     break;
 286   }
 287       }
 288
 289       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 290       MC_take_snapshot(next_snapshot);
 291
 292       next_state = new_state_ws(next_snapshot, next_graph_state);
 293       xbt_fifo_unshift(mc_stack_safety_stateful, next_state);
 294
 295       MC_UNSET_RAW_MEM;
 296
 297     }else{
 298       XBT_DEBUG("There are no more processes to interleave.");
 299
 300       /* Trash the current state, no longer needed */
 301       MC_SET_RAW_MEM;
 302       xbt_fifo_shift(mc_stack_safety_stateful);
 303       MC_UNSET_RAW_MEM;
 304
 305       /* Check for deadlocks */
 306       if(MC_deadlock_check()){
 307         MC_show_deadlock_stateful(NULL);
 308         return;
 309       }
 310
 311       MC_SET_RAW_MEM;
 312       while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
 313   req = MC_state_get_internal_request(current_state->graph_state);
 314   xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
 315           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
 316             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 317               XBT_DEBUG("Dependent Transitions:");
 318               prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
 319               req_str = MC_request_to_string(prev_req, value);
 320               XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
 321               xbt_free(req_str);
 322               prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
 323               req_str = MC_request_to_string(prev_req, value);
 324               XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
 325               xbt_free(req_str);
 326             }
 327
 328             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
 329               MC_state_interleave_process(prev_state->graph_state, req->issuer);
 330
 331       } else {
 332               XBT_DEBUG("Process %p is in done set", req->issuer);
 333       }
 334
 335             break;
 336           }
 337         }
 338
 339   if(MC_state_interleave_size(current_state->graph_state)){
 340     MC_restore_snapshot(current_state->system_state);
 341     xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
 342     XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
 343     MC_UNSET_RAW_MEM;
 344     break;
 345   }
 346       }
 347
 348       MC_UNSET_RAW_MEM;
 349
 350     }
 351   }
 352   MC_UNSET_RAW_MEM;
 353   return;
 354 }
 355
 356
 357