src/mc/mc_state.hpp

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