src/mc/mc_dpor.c

   1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
   2    All rights reserved.                                          */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /**
  13  *  \brief Initialize the DPOR exploration algorithm
  14  */
  15 void MC_dpor_init()
  16 {
  17   mc_state_t initial_state = NULL;
  18   smx_process_t process;
  19
  20   /* Create the initial state and push it into the exploration stack */
  21   MC_SET_RAW_MEM;
  22   initial_state = MC_state_new();
  23   xbt_fifo_unshift(mc_stack, initial_state);
  24   MC_UNSET_RAW_MEM;
  25
  26   DEBUG0("**************************************************");
  27   DEBUG0("Initial state");
  28
  29   /* Wait for requests (schedules processes) */
  30   MC_wait_for_requests();
  31
  32   MC_SET_RAW_MEM;
  33   /* Get an enabled process and insert it in the interleave set of the initial state */
  34   xbt_swag_foreach(process, simix_global->process_list){
  35     if(SIMIX_process_is_enabled(process)){
  36       xbt_setset_set_insert(initial_state->interleave, process);
  37       break;
  38     }
  39   }
  40   MC_UNSET_RAW_MEM;
  41
  42   /* FIXME: Update Statistics
  43   mc_stats->state_size +=
  44       xbt_setset_set_size(initial_state->enabled_transitions); */
  45 }
  46
  47
  48 /**
  49  *      \brief Perform the model-checking operation using a depth-first search exploration
  50  *         with Dynamic Partial Order Reductions
  51  */
  52 void MC_dpor(void)
  53 {
  54   char *req_str, deadlock;
  55   smx_req_t 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) > 0) {
  61
  62     DEBUG0("**************************************************");
  63
  64     /* Get current state */
  65     state = (mc_state_t)
  66       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  67
  68     /* If there are processes to interleave and the maximun depth has not been reached
  69        then perform one step of the exploration algorithm */
  70     if (xbt_setset_set_size(state->interleave) > 0
  71         && xbt_fifo_size(mc_stack) < MAX_DEPTH) {
  72
  73       DEBUG3("Exploration detph=%d (state=%p)(%d interleave)",
  74              xbt_fifo_size(mc_stack), state,
  75              xbt_setset_set_size(state->interleave));
  76
  77       /* Update statistics */
  78       mc_stats->visited_states++;
  79       mc_stats->executed_transitions++;
  80
  81       MC_SET_RAW_MEM;
  82       /* Choose a request to execute from the the current state */
  83       req = MC_state_get_request(state);
  84       MC_UNSET_RAW_MEM;
  85
  86       if(req){
  87         /* Answer the request */
  88         /* Debug information */
  89         if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  90           req_str = MC_request_to_string(req);
  91           DEBUG1("Execute: %s", req_str);
  92           xbt_free(req_str);
  93         }
  94
  95         MC_state_set_executed_request(state, req);
  96
  97         SIMIX_request_pre(req); /* After this call req is no longer usefull */
  98
  99         /* Wait for requests (schedules processes) */
 100         MC_wait_for_requests();
 101
 102         /* Create the new expanded state */
 103         MC_SET_RAW_MEM;
 104         next_state = MC_state_new();
 105         xbt_fifo_unshift(mc_stack, next_state);
 106
 107
 108         /* Get an enabled process and insert it in the interleave set of the next state */
 109         xbt_swag_foreach(process, simix_global->process_list){
 110           if(SIMIX_process_is_enabled(process)){
 111             xbt_setset_set_insert(next_state->interleave, process);
 112             break;
 113           }
 114         }
 115         MC_UNSET_RAW_MEM;
 116
 117         /* FIXME: Update Statistics
 118         mc_stats->state_size +=
 119             xbt_setset_set_size(next_state->enabled_transitions);*/
 120       }
 121       /* Let's loop again */
 122
 123       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 124     } else {
 125       DEBUG0("There are no more processes to interleave.");
 126
 127       /* Check for deadlocks */
 128       if(xbt_swag_size(simix_global->process_list)){
 129         deadlock = TRUE;
 130         xbt_swag_foreach(process, simix_global->process_list){
 131           if(process->request.call != REQ_NO_REQ
 132              && SIMIX_request_is_enabled(&process->request)){
 133             deadlock = FALSE;
 134             break;
 135           }
 136         }
 137
 138         if(deadlock){
 139           MC_show_deadlock(&process->request);
 140           return;
 141         }
 142       }
 143
 144       /*
 145       INFO0("*********************************");
 146       MC_show_stack(mc_stack); */
 147
 148       /* Trash the current state, no longer needed */
 149       MC_SET_RAW_MEM;
 150       xbt_fifo_shift(mc_stack);
 151       MC_state_delete(state);
 152
 153       /* Traverse the stack backwards until a state with a non empty interleave
 154          set is found, deleting all the states that have it empty in the way.
 155          For each deleted state, check if the request that has generated it
 156          (from it's predecesor state), depends on any other previous request
 157          executed before it. If it does then add it to the interleave set of the
 158          state that executed that previous request. */
 159       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 160         req = MC_state_get_executed_request(state);
 161         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 162           if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){
 163             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 164               DEBUG0("Dependent Transitions:");
 165               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state));
 166               DEBUG2("%s (state=%p)", req_str, prev_state);
 167               xbt_free(req_str);
 168               req_str = MC_request_to_string(req);
 169               DEBUG2("%s (state=%p)", req_str, state);
 170               xbt_free(req_str);
 171             }
 172
 173             if(!xbt_setset_set_belongs(prev_state->done, req->issuer))
 174               xbt_setset_set_insert(prev_state->interleave, req->issuer);
 175             else
 176               DEBUG1("Process %p is in done set", req->issuer);
 177
 178             break;
 179           }
 180         }
 181         if (xbt_setset_set_size(state->interleave) > 0) {
 182           /* We found a back-tracking point, let's loop */
 183           xbt_fifo_unshift(mc_stack, state);
 184           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 185           MC_UNSET_RAW_MEM;
 186           MC_replay(mc_stack);
 187           break;
 188         } else {
 189           MC_state_delete(state);
 190         }
 191       }
 192       MC_UNSET_RAW_MEM;
 193     }
 194   }
 195   MC_UNSET_RAW_MEM;
 196   return;
 197 }