src/mc/mc_state.hpp

   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_HPP
   7 #define SIMGRID_MC_STATE_HPP
   8
   9 #include <list>
  10 #include <memory>
  11
  12 #include "src/mc/mc_snapshot.hpp"
  13 #include "src/mc/mc_record.hpp"
  14 #include "src/mc/Transition.hpp"
  15
  16 namespace simgrid {
  17 namespace mc {
  18
  19 enum class PatternCommunicationType {
  20   none = 0,
  21   send = 1,
  22   receive = 2,
  23 };
  24
  25 class PatternCommunication {
  26 public:
  27   int num = 0;
  28   simgrid::kernel::activity::CommImpl* comm_addr;
  29   PatternCommunicationType type = PatternCommunicationType::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  * This represents both the process and its transition because
  65  *   a process cannot have more than one enabled transition at a given time.
  66  */
  67 class ProcessState {
  68   /* Possible exploration status of a process transition in a state.
  69    * Either the checker did not consider the transition, or it was considered and to do, or considered and done.
  70    */
  71   enum class InterleavingType {
  72     /** This process transition is not considered by the checker (yet?) */
  73     disabled = 0,
  74     /** The checker algorithm decided that this process transitions should be done at some point */
  75     todo,
  76     /** The checker algorithm decided that this should be done, but it was done in the meanwhile */
  77     done,
  78   };
  79
  80   /** Exploration control information */
  81   InterleavingType state = InterleavingType::disabled;
  82 public:
  83   /** Number of times that the process was considered to be executed */
  84   // TODO, make this private
  85   unsigned int times_considered = 0;
  86
  87   bool isDisabled() const {
  88     return this->state == InterleavingType::disabled;
  89   }
  90   bool isDone() const {
  91     return this->state == InterleavingType::done;
  92   }
  93   bool isTodo() const {
  94     return this->state == InterleavingType::todo;
  95   }
  96   /** Mark that we should try executing this process at some point in the future of the checker algorithm */
  97   void consider() {
  98     this->state            = InterleavingType::todo;
  99     this->times_considered = 0;
 100   }
 101   void setDone() {
 102     this->state = InterleavingType::done;
 103   }
 104 };
 105
 106 /* A node in the exploration graph (kind-of)
 107  */
 108 class XBT_PRIVATE State {
 109 public:
 110   /** Sequential state number (used for debugging) */
 111   int num = 0;
 112
 113   /** State's exploration status by process */
 114   std::vector<ProcessState> actorStates;
 115
 116   Transition transition;
 117
 118   /** The simcall which was executed, going out of that state */
 119   s_smx_simcall_t executed_req;
 120
 121   /* Internal translation of the executed_req simcall
 122    *
 123    * SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
 124    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
 125    */
 126   s_smx_simcall_t internal_req;
 127
 128   /* Can be used as a copy of the remote synchro object */
 129   simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> internal_comm;
 130
 131   /** Snapshot of system state (if needed) */
 132   std::shared_ptr<simgrid::mc::Snapshot> system_state;
 133
 134   // For CommunicationDeterminismChecker
 135   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
 136   std::vector<unsigned> communicationIndices;
 137
 138   State(unsigned long state_number);
 139
 140   std::size_t interleaveSize() const;
 141   void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->pid].consider(); }
 142   Transition getTransition() const;
 143 };
 144
 145 }
 146 }
 147
 148 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);
 149
 150 #endif