src/mc/mc_state.c

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