src/mc/mc_state.cpp

   1 /* Copyright (c) 2008-2014. The SimGrid Team.
   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 <assert.h>
   8
   9 #include "../simix/smx_private.h"
  10 #include "xbt/fifo.h"
  11 #include "mc_state.h"
  12 #include "mc_request.h"
  13 #include "mc_private.h"
  14 #include "mc_comm_pattern.h"
  15 #include "mc_smx.h"
  16
  17 using simgrid::mc::remote;
  18
  19 extern "C" {
  20
  21 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
  22                                 "Logging specific to MC (state)");
  23
  24 /**
  25  * \brief Creates a state data structure used by the exploration algorithm
  26  */
  27 mc_state_t MC_state_new()
  28 {
  29   mc_state_t state = xbt_new0(s_mc_state_t, 1);
  30
  31   state->max_pid = MC_smx_get_maxpid();
  32   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
  33   state->system_state = NULL;
  34   state->num = ++mc_stats->expanded_states;
  35   state->in_visited_states = 0;
  36   state->incomplete_comm_pattern = NULL;
  37   /* Stateful model checking */
  38   if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
  39     state->system_state = MC_take_snapshot(state->num);
  40     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
  41       MC_state_copy_incomplete_communications_pattern(state);
  42       MC_state_copy_index_communications_pattern(state);
  43     }
  44   }
  45   return state;
  46 }
  47
  48 /**
  49  * \brief Deletes a state data structure
  50  * \param trans The state to be deleted
  51  */
  52 void MC_state_delete(mc_state_t state, int free_snapshot){
  53   if (state->system_state && free_snapshot){
  54     delete state->system_state;
  55   }
  56   if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
  57     xbt_free(state->index_comm);
  58     xbt_free(state->incomplete_comm_pattern);
  59   }
  60   xbt_free(state->proc_status);
  61   xbt_free(state);
  62 }
  63
  64 void MC_state_interleave_process(mc_state_t state, smx_process_t process)
  65 {
  66   assert(state);
  67   state->proc_status[process->pid].state = MC_INTERLEAVE;
  68   state->proc_status[process->pid].interleave_count = 0;
  69 }
  70
  71 void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process)
  72 {
  73   if (state->proc_status[process->pid].state == MC_INTERLEAVE)
  74     state->proc_status[process->pid].state = MC_DONE;
  75 }
  76
  77 unsigned int MC_state_interleave_size(mc_state_t state)
  78 {
  79   unsigned int i, size = 0;
  80
  81   for (i = 0; i < state->max_pid; i++) {
  82     if ((state->proc_status[i].state == MC_INTERLEAVE)
  83         || (state->proc_status[i].state == MC_MORE_INTERLEAVE))
  84       size++;
  85   }
  86
  87   return size;
  88 }
  89
  90 int MC_state_process_is_done(mc_state_t state, smx_process_t process)
  91 {
  92   return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE;
  93 }
  94
  95 void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
  96                                    int value)
  97 {
  98   state->executed_req = *req;
  99   state->req_num = value;
 100
 101   smx_process_t process = NULL;
 102
 103   /* The waitany and testany request are transformed into a wait or test request over the
 104    * corresponding communication action so it can be treated later by the dependence
 105    * function. */
 106   switch (req->call) {
 107   case SIMCALL_COMM_WAITANY:
 108     state->internal_req.call = SIMCALL_COMM_WAIT;
 109     state->internal_req.issuer = req->issuer;
 110     MC_process_read_dynar_element(&mc_model_checker->process(),
 111       &state->internal_comm, simcall_comm_waitany__get__comms(req),
 112       value, sizeof(state->internal_comm));
 113     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
 114     simcall_comm_wait__set__timeout(&state->internal_req, 0);
 115     break;
 116
 117   case SIMCALL_COMM_TESTANY:
 118     state->internal_req.call = SIMCALL_COMM_TEST;
 119     state->internal_req.issuer = req->issuer;
 120
 121     if (value > 0)
 122         MC_process_read_dynar_element(&mc_model_checker->process(),
 123           &state->internal_comm, simcall_comm_testany__get__comms(req),
 124           value, sizeof(state->internal_comm));
 125
 126     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
 127     simcall_comm_test__set__result(&state->internal_req, value);
 128     break;
 129
 130   case SIMCALL_COMM_WAIT:
 131     state->internal_req = *req;
 132     mc_model_checker->process().read_bytes(&state->internal_comm ,
 133       sizeof(state->internal_comm), remote(simcall_comm_wait__get__comm(req)));
 134     simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
 135     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
 136     break;
 137
 138   case SIMCALL_COMM_TEST:
 139     state->internal_req = *req;
 140     mc_model_checker->process().read_bytes(&state->internal_comm,
 141       sizeof(state->internal_comm), remote(simcall_comm_test__get__comm(req)));
 142     simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
 143     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
 144     break;
 145
 146   case SIMCALL_MC_RANDOM: {
 147     state->internal_req = *req;
 148     int random_max = simcall_mc_random__get__max(req);
 149     if (value != random_max) {
 150       MC_EACH_SIMIX_PROCESS(process,
 151         mc_procstate_t procstate = &state->proc_status[process->pid];
 152         const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 153         if (process->pid == issuer->pid) {
 154           procstate->state = MC_MORE_INTERLEAVE;
 155           break;
 156         }
 157       );
 158     }
 159     break;
 160   }
 161
 162   default:
 163     state->internal_req = *req;
 164     break;
 165   }
 166 }
 167
 168 smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value)
 169 {
 170   *value = state->req_num;
 171   return &state->executed_req;
 172 }
 173
 174 smx_simcall_t MC_state_get_internal_request(mc_state_t state)
 175 {
 176   return &state->internal_req;
 177 }
 178
 179 static inline smx_simcall_t MC_state_get_request_for_process(
 180   mc_state_t state, int*value, smx_process_t process)
 181 {
 182   mc_procstate_t procstate = &state->proc_status[process->pid];
 183
 184   if (procstate->state != MC_INTERLEAVE
 185       && procstate->state != MC_MORE_INTERLEAVE)
 186       return NULL;
 187   if (!MC_process_is_enabled(process))
 188     return NULL;
 189
 190   switch (process->simcall.call) {
 191
 192       case SIMCALL_COMM_WAITANY:
 193         *value = -1;
 194         while (procstate->interleave_count <
 195               MC_process_read_dynar_length(&mc_model_checker->process(),
 196                 simcall_comm_waitany__get__comms(&process->simcall))) {
 197           if (MC_request_is_enabled_by_idx
 198               (&process->simcall, procstate->interleave_count++)) {
 199             *value = procstate->interleave_count - 1;
 200             break;
 201           }
 202         }
 203
 204         if (procstate->interleave_count >=
 205             MC_process_read_dynar_length(&mc_model_checker->process(),
 206               simcall_comm_waitany__get__comms(&process->simcall)))
 207           procstate->state = MC_DONE;
 208
 209         if (*value != -1)
 210           return &process->simcall;
 211
 212         break;
 213
 214       case SIMCALL_COMM_TESTANY: {
 215         unsigned start_count = procstate->interleave_count;
 216         *value = -1;
 217         while (procstate->interleave_count <
 218                 MC_process_read_dynar_length(&mc_model_checker->process(),
 219                   simcall_comm_testany__get__comms(&process->simcall))) {
 220           if (MC_request_is_enabled_by_idx
 221               (&process->simcall, procstate->interleave_count++)) {
 222             *value = procstate->interleave_count - 1;
 223             break;
 224           }
 225         }
 226
 227         if (procstate->interleave_count >=
 228             MC_process_read_dynar_length(&mc_model_checker->process(),
 229               simcall_comm_testany__get__comms(&process->simcall)))
 230           procstate->state = MC_DONE;
 231
 232         if (*value != -1 || start_count == 0)
 233           return &process->simcall;
 234
 235         break;
 236       }
 237
 238       case SIMCALL_COMM_WAIT: {
 239         smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
 240         s_smx_synchro_t act;
 241         mc_model_checker->process().read_bytes(
 242           &act, sizeof(act), remote(remote_act));
 243         if (act.comm.src_proc && act.comm.dst_proc) {
 244           *value = 0;
 245         } else {
 246           if (act.comm.src_proc == NULL && act.comm.type == SIMIX_COMM_READY
 247               && act.comm.detached == 1)
 248             *value = 0;
 249           else
 250             *value = -1;
 251         }
 252         procstate->state = MC_DONE;
 253         return &process->simcall;
 254       }
 255
 256       case SIMCALL_MC_RANDOM:
 257         if (procstate->state == MC_INTERLEAVE)
 258           *value = simcall_mc_random__get__min(&process->simcall);
 259         else {
 260           if (state->req_num < simcall_mc_random__get__max(&process->simcall))
 261             *value = state->req_num + 1;
 262         }
 263         procstate->state = MC_DONE;
 264         return &process->simcall;
 265
 266       default:
 267         procstate->state = MC_DONE;
 268         *value = 0;
 269         return &process->simcall;
 270   }
 271   return NULL;
 272 }
 273
 274 smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
 275 {
 276   smx_process_t process = NULL;
 277   MC_EACH_SIMIX_PROCESS(process,
 278     smx_simcall_t res = MC_state_get_request_for_process(state, value, process);
 279     if (res)
 280       return res;
 281   );
 282
 283   return NULL;
 284 }
 285
 286 }