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