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 #include "src/mc/mc_record.h"
  20
  21 namespace simgrid {
  22 namespace mc {
  23
  24 extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
  25
  26 struct PatternCommunication {
  27   int num = 0;
  28   smx_synchro_t comm_addr;
  29   e_smx_comm_type_t type = SIMIX_COMM_SEND;
  30   unsigned long src_proc = 0;
  31   unsigned long dst_proc = 0;
  32   const char *src_host = nullptr;
  33   const char *dst_host = nullptr;
  34   std::string rdv;
  35   std::vector<char> data;
  36   int tag = 0;
  37   int index = 0;
  38
  39   PatternCommunication()
  40   {
  41     std::memset(&comm_addr, 0, sizeof(comm_addr));
  42   }
  43
  44   PatternCommunication dup() const
  45   {
  46     simgrid::mc::PatternCommunication res;
  47     // num?
  48     res.comm_addr = this->comm_addr;
  49     res.type = this->type;
  50     // src_proc?
  51     // dst_proc?
  52     res.dst_proc = this->dst_proc;
  53     res.dst_host = this->dst_host;
  54     res.rdv = this->rdv;
  55     res.data = this->data;
  56     // tag?
  57     res.index = this->index;
  58     return res;
  59   }
  60
  61 };
  62
  63 /* On every state, each process has an entry of the following type */
  64 class ProcessState {
  65   /* Possible exploration status of a process in a state */
  66   enum class InterleavingType {
  67     /** We do not have to execute this process transitions */
  68     disabled = 0,
  69     /** We still have to execute (some of) this process transitions */
  70     interleave,
  71     /** We have already executed this process transitions */
  72     done,
  73   };
  74
  75   /** Exploration control information */
  76   InterleavingType state = InterleavingType::disabled;
  77 public:
  78
  79   /** Number of times that the process was interleaved */
  80   // TODO, make this private
  81   unsigned int interleave_count = 0;
  82
  83   bool isDisabled() const
  84   {
  85     return this->state == InterleavingType::disabled;
  86   }
  87   bool isDone() const
  88   {
  89     return this->state == InterleavingType::done;
  90   }
  91   bool isToInterleave() const
  92   {
  93     return this->state == InterleavingType::interleave;
  94   }
  95   void interleave()
  96   {
  97     this->state = InterleavingType::interleave;
  98     this->interleave_count = 0;
  99   }
 100   void setDone()
 101   {
 102     this->state = InterleavingType::done;
 103   }
 104 };
 105
 106 /* An exploration state.
 107  *
 108  *  The `executed_state` is sometimes transformed into another `internal_req`.
 109  *  For example WAITANY is transformes into a WAIT and TESTANY into TEST.
 110  *  See `MC_state_get_request_for_process()`.
 111  */
 112 struct XBT_PRIVATE State {
 113
 114   /** Sequential state number (used for debugging) */
 115   int num = 0;
 116
 117   /* Next transition to explore for this communication
 118    *
 119    * Some transitions are not deterministic such as:
 120    *
 121    * * waitany which can receive different messages;
 122    *
 123    * * random which can produce different values.
 124    *
 125    * This variable is used to keep track of which transition
 126    * should be explored next for a given simcall.
 127    */
 128   int req_num = 0;
 129
 130   /** State's exploration status by process */
 131   std::vector<ProcessState> processStates;
 132
 133   /** The simcall */
 134   s_smx_simcall_t executed_req;
 135
 136   /* Internal translation of the simcall
 137    *
 138    * IMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
 139    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
 140    */
 141   s_smx_simcall_t internal_req;
 142
 143   /* Can be used as a copy of the remote synchro object */
 144   s_smx_synchro_t internal_comm;
 145
 146   /** Snapshot of system state (if needed) */
 147   std::shared_ptr<simgrid::mc::Snapshot> system_state;
 148
 149   // For CommunicationDeterminismChecker
 150   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
 151   std::vector<unsigned> communicationIndices;
 152
 153   State();
 154
 155   std::size_t interleaveSize() const;
 156   void interleave(smx_process_t process)
 157   {
 158     this->processStates[process->pid].interleave();
 159   }
 160   RecordTraceElement getRecordElement() const;
 161 };
 162
 163 XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
 164
 165 }
 166 }
 167
 168 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
 169 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);
 170
 171 #endif