src/mc/mc_state.c

   1
   2
   3 #include "../simix/private.h"
   4 #include "xbt/fifo.h"
   5 #include "private.h"
   6
   7 /**
   8  * \brief Creates a state data structure used by the exploration algorithm
   9  */
  10 mc_state_t MC_state_new(void)
  11 {
  12   mc_state_t state = NULL;
  13
  14   state = xbt_new0(s_mc_state_t, 1);
  15   state->max_pid = simix_process_maxpid;
  16   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
  17
  18   mc_stats->expanded_states++;
  19   return state;
  20 }
  21
  22 /**
  23  * \brief Deletes a state data structure
  24  * \param trans The state to be deleted
  25  */
  26 void MC_state_delete(mc_state_t state)
  27 {
  28   xbt_free(state->proc_status);
  29   xbt_free(state);
  30 }
  31
  32 void MC_state_interleave_process(mc_state_t state, smx_process_t process)
  33 {
  34   state->proc_status[process->pid].state = MC_INTERLEAVE;
  35   state->proc_status[process->pid].interleave_count = 0;
  36 }
  37
  38 unsigned int MC_state_interleave_size(mc_state_t state)
  39 {
  40   unsigned int i, size=0;
  41
  42   for(i=0; i < state->max_pid; i++){
  43     if(state->proc_status[i].state == MC_INTERLEAVE)
  44       size++;
  45   }
  46
  47   return size;
  48 }
  49
  50 int MC_state_process_is_done(mc_state_t state, smx_process_t process){
  51   return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE;
  52 }
  53
  54 void MC_state_set_executed_request(mc_state_t state, smx_req_t req, int value)
  55 {
  56   state->executed_req = *req;
  57   state->req_num = value;
  58
  59   /* The waitany and testany request are transformed into a wait or test request over the
  60    * corresponding communication action so it can be treated later by the dependence
  61    * function. */
  62   switch(req->call){
  63     case REQ_COMM_WAITANY:
  64       state->internal_req.call = REQ_COMM_WAIT;
  65       state->internal_req.issuer = req->issuer;
  66       state->internal_comm = *xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t);
  67       state->internal_req.comm_wait.comm = &state->internal_comm;
  68       state->internal_req.comm_wait.timeout = 0;
  69       break;
  70
  71     case REQ_COMM_TESTANY:
  72       state->internal_req.call = REQ_COMM_TEST;
  73       state->internal_req.issuer = req->issuer;
  74
  75       if(value > 0)
  76         state->internal_comm = *xbt_dynar_get_as(req->comm_testany.comms, value, smx_action_t);
  77
  78       state->internal_req.comm_wait.comm = &state->internal_comm;
  79       state->internal_req.comm_test.result = value;
  80       break;
  81
  82     case REQ_COMM_WAIT:
  83       state->internal_req = *req;
  84       state->internal_comm = *(req->comm_wait.comm);
  85       state->executed_req.comm_wait.comm = &state->internal_comm;
  86       state->internal_req.comm_wait.comm = &state->internal_comm;
  87       break;
  88
  89     case REQ_COMM_TEST:
  90       state->internal_req = *req;
  91       state->internal_comm = *req->comm_test.comm;
  92       state->executed_req.comm_test.comm = &state->internal_comm;
  93       state->internal_req.comm_test.comm = &state->internal_comm;
  94       break;
  95
  96     default:
  97       state->internal_req = *req;
  98       break;
  99   }
 100 }
 101
 102 smx_req_t MC_state_get_executed_request(mc_state_t state, int *value)
 103 {
 104   *value = state->req_num;
 105   return &state->executed_req;
 106 }
 107
 108 smx_req_t MC_state_get_internal_request(mc_state_t state)
 109 {
 110   return &state->internal_req;
 111 }
 112
 113 smx_req_t MC_state_get_request(mc_state_t state, int *value)
 114 {
 115   smx_process_t process = NULL;
 116   mc_procstate_t procstate = NULL;
 117   unsigned int start_count;
 118
 119   xbt_swag_foreach(process, simix_global->process_list){
 120     procstate = &state->proc_status[process->pid];
 121
 122     if(procstate->state == MC_INTERLEAVE){
 123       if(MC_process_is_enabled(process)){
 124         switch(process->request.call){
 125           case REQ_COMM_WAITANY:
 126             *value = -1;
 127             while(procstate->interleave_count < xbt_dynar_length(process->request.comm_waitany.comms)){
 128               if(MC_request_is_enabled_by_idx(&process->request, procstate->interleave_count++)){
 129                 *value = procstate->interleave_count-1;
 130                 break;
 131               }
 132             }
 133
 134             if(procstate->interleave_count >= xbt_dynar_length(process->request.comm_waitany.comms))
 135               procstate->state = MC_DONE;
 136
 137             if(*value != -1)
 138               return &process->request;
 139
 140             break;
 141
 142           case REQ_COMM_TESTANY:
 143             start_count = procstate->interleave_count;
 144             *value = -1;
 145             while(procstate->interleave_count < xbt_dynar_length(process->request.comm_testany.comms)){
 146               if(MC_request_is_enabled_by_idx(&process->request, procstate->interleave_count++)){
 147                 *value = procstate->interleave_count - 1;
 148                 break;
 149               }
 150             }
 151
 152             if(procstate->interleave_count >= xbt_dynar_length(process->request.comm_testany.comms))
 153               procstate->state = MC_DONE;
 154
 155             if(*value != -1 || start_count == 0)
 156               return &process->request;
 157
 158             break;
 159
 160           case REQ_COMM_WAIT:
 161             if(process->request.comm_wait.comm->comm.src_proc
 162                && process->request.comm_wait.comm->comm.dst_proc){
 163               *value = 0;
 164             }else{
 165               *value = -1;
 166             }
 167             procstate->state = MC_DONE;
 168             return &process->request;
 169
 170             break;
 171
 172           default:
 173             procstate->state = MC_DONE;
 174             *value = 0;
 175             return &process->request;
 176             break;
 177         }
 178       }
 179     }
 180   }
 181
 182   return NULL;
 183 }