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 /* On every state, each process has an entry of the following type */
  63 class ProcessState {
  64   /* Possible exploration status of a process in a state */
  65   enum class InterleavingType {
  66     /** We do not have to execute this process transitions */
  67     disabled = 0,
  68     /** We still have to execute (some of) this process transitions */
  69     interleave,
  70     /** We have already executed this process transitions */
  71     done,
  72   };
  73
  74   /** Exploration control information */
  75   InterleavingType state = InterleavingType::disabled;
  76 public:
  77
  78   /** Number of times that the process was interleaved */
  79   // TODO, make this private
  80   unsigned int interleave_count = 0;
  81
  82   bool isDisabled() const
  83   {
  84     return this->state == InterleavingType::disabled;
  85   }
  86   bool isDone() const
  87   {
  88     return this->state == InterleavingType::done;
  89   }
  90   bool isToInterleave() const
  91   {
  92     return this->state == InterleavingType::interleave;
  93   }
  94   void interleave()
  95   {
  96     this->state = InterleavingType::interleave;
  97     this->interleave_count = 0;
  98   }
  99   void setDone()
 100   {
 101     this->state = InterleavingType::done;
 102   }
 103 };
 104
 105 /* An exploration state.
 106  *
 107  *  The `executed_state` is sometimes transformed into another `internal_req`.
 108  *  For example WAITANY is transformes into a WAIT and TESTANY into TEST.
 109  *  See `MC_state_get_request_for_process()`.
 110  */
 111 struct XBT_PRIVATE State {
 112
 113   /** Sequential state number (used for debugging) */
 114   int num = 0;
 115
 116   /* Next transition to explore for this communication
 117    *
 118    * Some transitions are not deterministic such as:
 119    *
 120    * * waitany which can receive different messages;
 121    *
 122    * * random which can produce different values.
 123    *
 124    * This variable is used to keep track of which transition
 125    * should be explored next for a given simcall.
 126    */
 127   int req_num = 0;
 128
 129   /** State's exploration status by process */
 130   std::vector<ProcessState> processStates;
 131
 132   /** The simcall */
 133   s_smx_simcall_t executed_req;
 134
 135   /* Internal translation of the simcall
 136    *
 137    * IMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
 138    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
 139    */
 140   s_smx_simcall_t internal_req;
 141
 142   /* Can be used as a copy of the remote synchro object */
 143   s_smx_synchro_t internal_comm;
 144
 145   /** Snapshot of system state (if needed) */
 146   std::shared_ptr<simgrid::mc::Snapshot> system_state;
 147
 148   // For CommunicationDeterminismChecker
 149   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
 150   std::vector<unsigned> communicationIndices;
 151
 152   State();
 153
 154   std::size_t interleaveSize() const;
 155   void interleave(smx_process_t process)
 156   {
 157     this->processStates[process->pid].interleave();
 158   }
 159 };
 160
 161 XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
 162
 163 }
 164 }
 165
 166 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
 167 XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value);
 168 XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state);
 169 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
 170
 171 #endif