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