src/mc/mc_state.h

   1 /* Copyright (c) 2007-2017. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #ifndef SIMGRID_MC_STATE_H
   7 #define SIMGRID_MC_STATE_H
   8
   9 #include <list>
  10 #include <memory>
  11
  12 #include <xbt/base.h>
  13 #include <xbt/dynar.h>
  14
  15 #include "src/simix/smx_private.h"
  16 #include "src/kernel/activity/SynchroIo.hpp"
  17 #include "src/kernel/activity/SynchroComm.hpp"
  18 #include "src/kernel/activity/SynchroRaw.hpp"
  19 #include "src/kernel/activity/SynchroSleep.hpp"
  20 #include "src/kernel/activity/SynchroExec.hpp"
  21 #include "src/mc/mc_snapshot.h"
  22 #include "src/mc/mc_record.h"
  23 #include "src/mc/Transition.hpp"
  24
  25 namespace simgrid {
  26 namespace mc {
  27
  28 enum class PatternCommunicationType {
  29   none = 0,
  30   send = 1,
  31   receive = 2,
  32 };
  33
  34 struct PatternCommunication {
  35   int num = 0;
  36   smx_activity_t comm_addr;
  37   PatternCommunicationType type = PatternCommunicationType::send;
  38   unsigned long src_proc = 0;
  39   unsigned long dst_proc = 0;
  40   const char *src_host = nullptr;
  41   const char *dst_host = nullptr;
  42   std::string rdv;
  43   std::vector<char> data;
  44   int tag = 0;
  45   int index = 0;
  46
  47   PatternCommunication()
  48   {
  49     std::memset(&comm_addr, 0, sizeof(comm_addr));
  50   }
  51
  52   PatternCommunication dup() const
  53   {
  54     simgrid::mc::PatternCommunication res;
  55     // num?
  56     res.comm_addr = this->comm_addr;
  57     res.type = this->type;
  58     // src_proc?
  59     // dst_proc?
  60     res.dst_proc = this->dst_proc;
  61     res.dst_host = this->dst_host;
  62     res.rdv = this->rdv;
  63     res.data = this->data;
  64     // tag?
  65     res.index = this->index;
  66     return res;
  67   }
  68
  69 };
  70
  71 /* On every state, each process has an entry of the following type.
  72  * This represents both the process and its transition because
  73  *   a process cannot have more than one enabled transition at a given time.
  74  */
  75 class ProcessState {
  76   /* Possible exploration status of a process transition in a state.
  77    * Either the checker did not consider the transition, or it was considered and to do, or considered and done.
  78    */
  79   enum class InterleavingType {
  80     /** This process transition is not considered by the checker (yet?) */
  81     disabled = 0,
  82     /** The checker algorithm decided that this process transitions should be done at some point */
  83     todo,
  84     /** The checker algorithm decided that this should be done, but it was done in the meanwhile */
  85     done,
  86   };
  87
  88   /** Exploration control information */
  89   InterleavingType state = InterleavingType::disabled;
  90 public:
  91   /** Number of times that the process was considered to be executed */
  92   // TODO, make this private
  93   unsigned int times_considered = 0;
  94
  95   bool isDisabled() const {
  96     return this->state == InterleavingType::disabled;
  97   }
  98   bool isDone() const {
  99     return this->state == InterleavingType::done;
 100   }
 101   bool isTodo() const {
 102     return this->state == InterleavingType::todo;
 103   }
 104   /** Mark that we should try executing this process at some point in the future of the checker algorithm */
 105   void consider() {
 106     this->state            = InterleavingType::todo;
 107     this->times_considered = 0;
 108   }
 109   void setDone() {
 110     this->state = InterleavingType::done;
 111   }
 112 };
 113
 114 /* A node in the exploration graph (kind-of)
 115  */
 116 struct XBT_PRIVATE State {
 117
 118   /** Sequential state number (used for debugging) */
 119   int num = 0;
 120
 121   /** State's exploration status by process */
 122   std::vector<ProcessState> actorStates;
 123
 124   Transition transition;
 125
 126   /** The simcall which was executed, going out of that state */
 127   s_smx_simcall_t executed_req;
 128
 129   /* Internal translation of the executed_req simcall
 130    *
 131    * SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
 132    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
 133    */
 134   s_smx_simcall_t internal_req;
 135
 136   /* Can be used as a copy of the remote synchro object */
 137   simgrid::mc::Remote<simgrid::kernel::activity::Comm> internal_comm;
 138
 139   /** Snapshot of system state (if needed) */
 140   std::shared_ptr<simgrid::mc::Snapshot> system_state;
 141
 142   // For CommunicationDeterminismChecker
 143   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
 144   std::vector<unsigned> communicationIndices;
 145
 146   State(unsigned long state_number);
 147
 148   std::size_t interleaveSize() const;
 149   void interleave(smx_actor_t actor) {
 150     this->actorStates[actor->pid].consider();
 151   }
 152   Transition getTransition() const;
 153 };
 154
 155 }
 156 }
 157
 158 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);
 159
 160 #endif