src/mc/mc_state.cpp

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