Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Implement TestAnyTransition
[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 {
181   int size;
182   stream >> size;
183   for (int i = 0; i < size; i++) {
184
185     Transition* t = recv_transition(issuer, 0, stream);
186     transitions_.push_back(t);
187   }
188 }
189 std::string TestAnyTransition::to_string(bool verbose) const
190 {
191   auto res = xbt::string_printf("%ld: TestAny{ ", aid_);
192   for (auto const* t : transitions_)
193     res += t->to_string(verbose);
194   res += "}";
195   return res;
196 }
197 bool TestAnyTransition::depends(const Transition* other) const
198 {
199   return true;
200 }
201
202 bool CommSendTransition::depends(const Transition* other) const
203 {
204   if (aid_ == other->aid_)
205     return false;
206
207   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
208     return false; // Random is indep with any transition
209
210   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
211     return mbox_ == other_isend->mbox_;
212
213   if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
214     return false;
215
216   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
217     if (mbox_ != test->mbox_)
218       return false;
219
220     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->src_buff_ != src_buff_))
221       return false;
222   }
223
224   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
225     if (wait->timeout_)
226       return true;
227
228     if (mbox_ != wait->mbox_)
229       return false;
230
231     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->src_buff_ != src_buff_))
232       return false;
233   }
234
235   return true;
236 }
237
238 Transition* recv_transition(aid_t issuer, int times_considered, std::stringstream& stream)
239 {
240   short type;
241   stream >> type;
242   Transition::Type simcall = static_cast<Transition::Type>(type);
243
244   switch (simcall) {
245     case Transition::Type::COMM_RECV:
246       return new CommRecvTransition(issuer, times_considered, stream);
247     case Transition::Type::COMM_SEND:
248       return new CommSendTransition(issuer, times_considered, stream);
249     case Transition::Type::COMM_TEST:
250       return new CommTestTransition(issuer, times_considered, stream);
251     case Transition::Type::COMM_WAIT:
252       return new CommWaitTransition(issuer, times_considered, stream);
253
254     case Transition::Type::TESTANY:
255       return new TestAnyTransition(issuer, times_considered, stream);
256
257     case Transition::Type::RANDOM:
258       return new RandomTransition(issuer, times_considered, stream);
259
260     case Transition::Type::UNKNOWN:
261       return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
262     default:
263       xbt_die("recv_transition of type %s unimplemented", Transition::to_c_str(simcall));
264   }
265 }
266
267 } // namespace mc
268 } // namespace simgrid