Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
better name
[simgrid.git] / src / mc / api / TransitionComm.cpp
1 /* Copyright (c) 2015-2022. 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 #include "src/mc/api/TransitionComm.hpp"
7 #include "xbt/asserts.h"
8 #include <simgrid/config.h>
9 #if SIMGRID_HAVE_MC
10 #include "src/mc/ModelChecker.hpp"
11 #include "src/mc/Session.hpp"
12 #include "src/mc/api/State.hpp"
13 #endif
14
15 #include <sstream>
16
17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_comm, mc_transition,
18                                 "Logging specific to MC transitions about communications");
19
20 namespace simgrid {
21 namespace mc {
22
23 CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream)
24     : Transition(Type::COMM_WAIT, issuer, times_considered)
25 {
26   stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
27   XBT_DEBUG("CommWaitTransition %s comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu",
28             (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, src_buff_, dst_buff_, size_);
29 }
30 std::string CommWaitTransition::to_string(bool verbose) const
31 {
32   auto res = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
33                                 (timeout_ ? "timeout" : "no timeout"));
34   if (verbose) {
35     res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
36     res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
37   }
38   res += ")";
39   return res;
40 }
41 bool CommWaitTransition::depends(const Transition* other) const
42 {
43   if (aid_ == other->aid_)
44     return false;
45
46   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
47     return false; // Random is indep with any transition
48
49   if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
50     return recv->depends(this);
51
52   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
53     return send->depends(this);
54
55   if (auto* test = dynamic_cast<const CommTestTransition*>(other))
56     return test->depends(this);
57
58   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
59     if (timeout_ || wait->timeout_)
60       return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
61
62     if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_)
63       return false;
64     if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr &&
65         dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_)
66       return false;
67   }
68
69   return true;
70 }
71 CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream)
72     : Transition(Type::COMM_TEST, issuer, times_considered)
73 {
74   stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
75   XBT_DEBUG("CommTestTransition comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu", comm_, sender_,
76             receiver_, mbox_, src_buff_, dst_buff_, size_);
77 }
78 std::string CommTestTransition::to_string(bool verbose) const
79 {
80   auto res = xbt::string_printf("%ld: TestComm(from %ld to %ld, mbox=%u", aid_, sender_, receiver_, mbox_);
81   if (verbose) {
82     res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
83     res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
84   }
85   res += ")";
86   return res;
87 }
88 bool CommTestTransition::depends(const Transition* other) const
89 {
90   if (aid_ == other->aid_)
91     return false;
92
93   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
94     return false; // Test & Random are independent (Random is independent with anything)
95
96   if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
97     return recv->depends(this); // Recv < Test (alphabetical ordering)
98
99   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
100     return send->depends(this); // Send < Test (alphabetical ordering)
101
102   if (dynamic_cast<const CommTestTransition*>(other) != nullptr)
103     return false; // Test & Test are independent
104
105   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
106     if (wait->timeout_)
107       return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
108
109     /* Wait & Test are independent */
110     return false;
111   }
112
113   return true;
114 }
115
116 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
117     : Transition(Type::COMM_RECV, issuer, times_considered)
118 {
119   stream >> mbox_ >> dst_buff_;
120 }
121 std::string CommRecvTransition::to_string(bool verbose) const
122 {
123   auto res = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
124   if (verbose)
125     res += ", buff=" + xbt::string_printf("%p", dst_buff_);
126   res += ")";
127   return res;
128 }
129 bool CommRecvTransition::depends(const Transition* other) const
130 {
131   if (aid_ == other->aid_)
132     return false;
133
134   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
135     return false; // Random is indep with any transition
136
137   if (const auto* recv = dynamic_cast<const CommRecvTransition*>(other))
138     return mbox_ == recv->mbox_;
139
140   if (dynamic_cast<const CommSendTransition*>(other) != nullptr)
141     return false;
142
143   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
144     if (mbox_ != test->mbox_)
145       return false;
146
147     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->dst_buff_ != dst_buff_))
148       return false;
149   }
150
151   if (auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
152     if (wait->timeout_)
153       return true;
154
155     if (mbox_ != wait->mbox_)
156       return false;
157
158     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->dst_buff_ != dst_buff_))
159       return false;
160   }
161
162   return true;
163 }
164
165 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
166     : Transition(Type::COMM_SEND, issuer, times_considered)
167 {
168   stream >> mbox_ >> src_buff_ >> size_;
169   XBT_DEBUG("SendTransition mbox:%u buff:%p size:%zu", mbox_, src_buff_, size_);
170 }
171 std::string CommSendTransition::to_string(bool verbose = false) const
172 {
173   auto res = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
174   if (verbose)
175     res += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
176   res += ")";
177   return res;
178 }
179 TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
180     : Transition(Type::TESTANY, issuer, times_considered)
181 {
182   int size;
183   stream >> size;
184   for (int i = 0; i < size; i++) {
185
186     Transition* t = deserialize_transition(issuer, 0, stream);
187     transitions_.push_back(t);
188   }
189 }
190 std::string TestAnyTransition::to_string(bool verbose) const
191 {
192   auto res = xbt::string_printf("%ld: TestAny{ ", aid_);
193   for (auto const* t : transitions_)
194     res += t->to_string(verbose);
195   res += "}";
196   return res;
197 }
198 bool TestAnyTransition::depends(const Transition* other) const
199 {
200   return true;
201 }
202
203 bool CommSendTransition::depends(const Transition* other) const
204 {
205   if (aid_ == other->aid_)
206     return false;
207
208   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
209     return false; // Random is indep with any transition
210
211   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
212     return mbox_ == other_isend->mbox_;
213
214   if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
215     return false;
216
217   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
218     if (mbox_ != test->mbox_)
219       return false;
220
221     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->src_buff_ != src_buff_))
222       return false;
223   }
224
225   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
226     if (wait->timeout_)
227       return true;
228
229     if (mbox_ != wait->mbox_)
230       return false;
231
232     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->src_buff_ != src_buff_))
233       return false;
234   }
235
236   return true;
237 }
238
239 Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream)
240 {
241   short type;
242   stream >> type;
243   xbt_assert(type >= 0 && type <= static_cast<short>(Transition::Type::UNKNOWN), "Invalid transition type %d received",
244              type);
245
246   auto simcall = static_cast<Transition::Type>(type);
247
248   switch (simcall) {
249     case Transition::Type::COMM_RECV:
250       return new CommRecvTransition(issuer, times_considered, stream);
251     case Transition::Type::COMM_SEND:
252       return new CommSendTransition(issuer, times_considered, stream);
253     case Transition::Type::COMM_TEST:
254       return new CommTestTransition(issuer, times_considered, stream);
255     case Transition::Type::COMM_WAIT:
256       return new CommWaitTransition(issuer, times_considered, stream);
257
258     case Transition::Type::TESTANY:
259       return new TestAnyTransition(issuer, times_considered, stream);
260
261     case Transition::Type::RANDOM:
262       return new RandomTransition(issuer, times_considered, stream);
263
264     case Transition::Type::UNKNOWN:
265       return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
266   }
267   THROW_IMPOSSIBLE; // Some compilers don't detect that each branch of the above switch has a return
268 }
269
270 } // namespace mc
271 } // namespace simgrid