src/mc/mc_state.hpp

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