src/mc/mc_state.h

   1 /* Copyright (c) 2007-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 #ifndef SIMGRID_MC_STATE_H
   8 #define SIMGRID_MC_STATE_H
   9
  10 #include <list>
  11 #include <memory>
  12
  13 #include <xbt/base.h>
  14 #include <xbt/dynar.h>
  15
  16 #include <simgrid_config.h>
  17 #include "src/simix/smx_private.h"
  18 #include "src/mc/mc_snapshot.h"
  19
  20 namespace simgrid {
  21 namespace mc {
  22
  23 extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
  24
  25 struct PatternCommunication {
  26   int num = 0;
  27   smx_synchro_t comm_addr;
  28   e_smx_comm_type_t type = SIMIX_COMM_SEND;
  29   unsigned long src_proc = 0;
  30   unsigned long dst_proc = 0;
  31   const char *src_host = nullptr;
  32   const char *dst_host = nullptr;
  33   std::string rdv;
  34   std::vector<char> data;
  35   int tag = 0;
  36   int index = 0;
  37
  38   PatternCommunication()
  39   {
  40     std::memset(&comm_addr, 0, sizeof(comm_addr));
  41   }
  42
  43   PatternCommunication dup() const
  44   {
  45     simgrid::mc::PatternCommunication res;
  46     // num?
  47     res.comm_addr = this->comm_addr;
  48     res.type = this->type;
  49     // src_proc?
  50     // dst_proc?
  51     res.dst_proc = this->dst_proc;
  52     res.dst_host = this->dst_host;
  53     res.rdv = this->rdv;
  54     res.data = this->data;
  55     // tag?
  56     res.index = this->index;
  57     return res;
  58   }
  59
  60 };
  61
  62 /* Possible exploration status of a process in a state */
  63 enum class ProcessInterleaveState {
  64   no_interleave=0, /* Do not interleave (do not execute) */
  65   interleave,      /* Interleave the process (one or more request) */
  66   more_interleave, /* Interleave twice the process (for mc_random simcall) */
  67   done             /* Already interleaved */
  68 };
  69
  70 /* On every state, each process has an entry of the following type */
  71 struct ProcessState {
  72   /** Exploration control information */
  73   ProcessInterleaveState state = ProcessInterleaveState::no_interleave;
  74   /** Number of times that the process was interleaved */
  75   unsigned int interleave_count;
  76
  77   bool done() const
  78   {
  79     return this->state == ProcessInterleaveState::done;
  80   }
  81   bool interleave() const {
  82     return this->state == ProcessInterleaveState::interleave
  83       || this->state == ProcessInterleaveState::more_interleave;
  84   }
  85 };
  86
  87 /* An exploration state.
  88  *
  89  *  The `executed_state` is sometimes transformed into another `internal_req`.
  90  *  For example WAITANY is transformes into a WAIT and TESTANY into TEST.
  91  *  See `MC_state_set_executed_request()`.
  92  */
  93 struct XBT_PRIVATE State {
  94
  95   /** Sequential state number (used for debugging) */
  96   int num = 0;
  97
  98   /* Next transition to explore for this communication
  99    *
 100    * Some transitions are not deterministic such as:
 101    *
 102    * * waitany which can receive different messages;
 103    *
 104    * * random which can produce different values.
 105    *
 106    * This variable is used to keep track of which transition
 107    * should be explored next for a given simcall.
 108    */
 109   int req_num = 0;
 110
 111   /** State's exploration status by process */
 112   std::vector<ProcessState> processStates;
 113
 114   /** The simcall */
 115   s_smx_simcall_t executed_req;
 116
 117   /* Internal translation of the simcall
 118    *
 119    * IMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
 120    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
 121    */
 122   s_smx_simcall_t internal_req;
 123
 124   /* Can be used as a copy of the remote synchro object */
 125   s_smx_synchro_t internal_comm;
 126
 127   /** Snapshot of system state (if needed) */
 128   std::shared_ptr<simgrid::mc::Snapshot> system_state;
 129
 130   // For CommunicationDeterminismChecker
 131   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
 132   std::vector<unsigned> communicationIndices;
 133
 134   State();
 135
 136   std::size_t interleaveSize() const;
 137 };
 138
 139 XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
 140
 141 }
 142 }
 143
 144 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
 145 XBT_PRIVATE void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process);
 146 XBT_PRIVATE void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int value);
 147 XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value);
 148 XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state);
 149 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
 150
 151 #endif