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