Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove MC_state_get_executed_request()
[simgrid.git] / 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
21 namespace simgrid {
22 namespace mc {
23
24 extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
25
26 struct PatternCommunication {
27   int num = 0;
28   smx_synchro_t comm_addr;
29   e_smx_comm_type_t type = SIMIX_COMM_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 class ProcessState {
65   /* Possible exploration status of a process in a state */
66   enum class InterleavingType {
67     /** We do not have to execute this process transitions */
68     disabled = 0,
69     /** We still have to execute (some of) this process transitions */
70     interleave,
71     /** We have already executed this process transitions */
72     done,
73   };
74
75   /** Exploration control information */
76   InterleavingType state = InterleavingType::disabled;
77 public:
78
79   /** Number of times that the process was interleaved */
80   // TODO, make this private
81   unsigned int interleave_count = 0;
82
83   bool isDisabled() const
84   {
85     return this->state == InterleavingType::disabled;
86   }
87   bool isDone() const
88   {
89     return this->state == InterleavingType::done;
90   }
91   bool isToInterleave() const
92   {
93     return this->state == InterleavingType::interleave;
94   }
95   void interleave()
96   {
97     this->state = InterleavingType::interleave;
98     this->interleave_count = 0;
99   }
100   void setDone()
101   {
102     this->state = InterleavingType::done;
103   }
104 };
105
106 /* An exploration state.
107  *
108  *  The `executed_state` is sometimes transformed into another `internal_req`.
109  *  For example WAITANY is transformes into a WAIT and TESTANY into TEST.
110  *  See `MC_state_get_request_for_process()`.
111  */
112 struct XBT_PRIVATE State {
113
114   /** Sequential state number (used for debugging) */
115   int num = 0;
116
117   /* Next transition to explore for this communication
118    *
119    * Some transitions are not deterministic such as:
120    *
121    * * waitany which can receive different messages;
122    *
123    * * random which can produce different values.
124    *
125    * This variable is used to keep track of which transition
126    * should be explored next for a given simcall.
127    */
128   int req_num = 0;
129
130   /** State's exploration status by process */
131   std::vector<ProcessState> processStates;
132
133   /** The simcall */
134   s_smx_simcall_t executed_req;
135
136   /* Internal translation of the simcall
137    *
138    * IMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
139    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
140    */
141   s_smx_simcall_t internal_req;
142
143   /* Can be used as a copy of the remote synchro object */
144   s_smx_synchro_t internal_comm;
145
146   /** Snapshot of system state (if needed) */
147   std::shared_ptr<simgrid::mc::Snapshot> system_state;
148
149   // For CommunicationDeterminismChecker
150   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
151   std::vector<unsigned> communicationIndices;
152
153   State();
154
155   std::size_t interleaveSize() const;
156   void interleave(smx_process_t process)
157   {
158     this->processStates[process->pid].interleave();
159   }
160   RecordTraceElement getRecordElement() const;
161 };
162
163 XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
164
165 }
166 }
167
168 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
169 XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state);
170 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
171
172 #endif