Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
032a6e5b4df569a9569b6954b2caf135290783e7
[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
20 namespace simgrid {
21 namespace mc {
22
23 extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
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 /* Possible exploration status of a process in a state */
63 enum class ProcessInterleaveState {
64   no_interleave=0, /* Do not interleave (do not execute) */
65   interleave,      /* Interleave the process (one or more request) */
66   more_interleave, /* Interleave twice the process (for mc_random simcall) */
67   done             /* Already interleaved */
68 };
69
70 /* On every state, each process has an entry of the following type */
71 struct ProcessState {
72   /** Exploration control information */
73   ProcessInterleaveState state = ProcessInterleaveState::no_interleave;
74   /** Number of times that the process was interleaved */
75   unsigned int interleave_count;
76
77   bool done() const
78   {
79     return this->state == ProcessInterleaveState::done;
80   }
81   bool interleave() const {
82     return this->state == ProcessInterleaveState::interleave
83       || this->state == ProcessInterleaveState::more_interleave;
84   }
85 };
86
87 /* An exploration state.
88  *
89  *  The `executed_state` is sometimes transformed into another `internal_req`.
90  *  For example WAITANY is transformes into a WAIT and TESTANY into TEST.
91  *  See `MC_state_get_request_for_process()`.
92  */
93 struct XBT_PRIVATE State {
94
95   /** Sequential state number (used for debugging) */
96   int num = 0;
97
98   /* Next transition to explore for this communication
99    *
100    * Some transitions are not deterministic such as:
101    *
102    * * waitany which can receive different messages;
103    *
104    * * random which can produce different values.
105    *
106    * This variable is used to keep track of which transition
107    * should be explored next for a given simcall.
108    */
109   int req_num = 0;
110
111   /** State's exploration status by process */
112   std::vector<ProcessState> processStates;
113
114   /** The simcall */
115   s_smx_simcall_t executed_req;
116
117   /* Internal translation of the simcall
118    *
119    * IMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
120    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
121    */
122   s_smx_simcall_t internal_req;
123
124   /* Can be used as a copy of the remote synchro object */
125   s_smx_synchro_t internal_comm;
126
127   /** Snapshot of system state (if needed) */
128   std::shared_ptr<simgrid::mc::Snapshot> system_state;
129
130   // For CommunicationDeterminismChecker
131   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
132   std::vector<unsigned> communicationIndices;
133
134   State();
135
136   std::size_t interleaveSize() const;
137 };
138
139 XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
140
141 }
142 }
143
144 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
145 XBT_PRIVATE void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process);
146 XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value);
147 XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state);
148 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
149
150 #endif