Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
There's no need to compute the total transition count anymore.
[simgrid.git] / src / mc / remote / AppSide.cpp
1 /* Copyright (c) 2015-2023. 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/remote/AppSide.hpp"
7 #include "simgrid/s4u/Host.hpp"
8 #include "src/internal_config.h"
9 #include "src/kernel/EngineImpl.hpp"
10 #include "src/kernel/actor/ActorImpl.hpp"
11 #include "src/kernel/actor/SimcallObserver.hpp"
12 #include "src/mc/mc_base.hpp"
13 #include "src/mc/mc_config.hpp"
14 #include "src/mc/sosp/RemoteProcessMemory.hpp"
15 #if HAVE_SMPI
16 #include "src/smpi/include/private.hpp"
17 #endif
18 #include "src/sthread/sthread.h"
19 #include "src/xbt/coverage.h"
20 #include "xbt/str.h"
21 #include <simgrid/modelchecker.h>
22
23 #include <cerrno>
24 #include <cstdio> // setvbuf
25 #include <cstdlib>
26 #include <memory>
27 #include <numeric>
28 #include <sys/ptrace.h>
29 #include <sys/socket.h>
30 #include <sys/types.h>
31
32 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
33 XBT_LOG_EXTERNAL_CATEGORY(mc_global);
34
35 namespace simgrid::mc {
36
37 std::unique_ptr<AppSide> AppSide::instance_;
38
39 AppSide* AppSide::initialize()
40 {
41   if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
42     return nullptr;
43
44   // Do not break if we are called multiple times:
45   if (instance_)
46     return instance_.get();
47
48   simgrid::mc::model_checking_mode = ModelCheckingMode::APP_SIDE;
49
50   setvbuf(stdout, nullptr, _IOLBF, 0);
51
52   // Fetch socket from MC_ENV_SOCKET_FD:
53   const char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
54   int fd             = xbt_str_parse_int(fd_env, "Not a number in variable '" MC_ENV_SOCKET_FD "'");
55   XBT_DEBUG("Model-checked application found socket FD %i", fd);
56
57   // Check the socket type/validity:
58   int type;
59   socklen_t socklen = sizeof(type);
60   xbt_assert(getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) == 0, "Could not check socket type");
61   xbt_assert(type == SOCK_SEQPACKET, "Unexpected socket type %i", type);
62   XBT_DEBUG("Model-checked application found expected socket type");
63
64   instance_ = std::make_unique<simgrid::mc::AppSide>(fd);
65
66   // Wait for the model-checker:
67   errno = 0;
68 #if defined __linux__
69   ptrace(PTRACE_TRACEME, 0, nullptr, nullptr);
70 #elif defined BSD
71   ptrace(PT_TRACE_ME, 0, nullptr, 0);
72 #else
73 #error "no ptrace equivalent coded for this platform"
74 #endif
75   xbt_assert(errno == 0 && raise(SIGSTOP) == 0, "Could not wait for the model-checker (errno = %d: %s)", errno,
76              strerror(errno));
77
78   instance_->handle_messages();
79   return instance_.get();
80 }
81
82 void AppSide::handle_deadlock_check(const s_mc_message_t*) const
83 {
84   const auto* engine     = kernel::EngineImpl::get_instance();
85   const auto& actor_list = engine->get_actor_list();
86   bool deadlock = not actor_list.empty() && std::none_of(begin(actor_list), end(actor_list), [](const auto& kv) {
87     return mc::actor_is_enabled(kv.second);
88   });
89
90   if (deadlock) {
91     XBT_CINFO(mc_global, "**************************");
92     XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
93     XBT_CINFO(mc_global, "**************************");
94     engine->display_all_actor_status();
95   }
96   // Send result:
97   s_mc_message_int_t answer = {};
98   answer.type  = MessageType::DEADLOCK_CHECK_REPLY;
99   answer.value = deadlock;
100   xbt_assert(channel_.send(answer) == 0, "Could not send response");
101 }
102 void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const
103 {
104   kernel::actor::ActorImpl* actor = kernel::EngineImpl::get_instance()->get_actor_by_pid(message->aid_);
105   xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_);
106
107   // The client may send some messages to the server while processing the transition
108   actor->simcall_handle(message->times_considered_);
109   // Say the server that the transition is over and that it should proceed
110   xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker");
111
112   // Finish the RPC from the server: return a serialized observer, to build a Transition on Checker side
113   s_mc_message_simcall_execute_answer_t answer = {};
114   answer.type = MessageType::SIMCALL_EXECUTE_ANSWER;
115   std::stringstream stream;
116   if (actor->simcall_.observer_ != nullptr) {
117     actor->simcall_.observer_->serialize(stream);
118   } else {
119     stream << (short)mc::Transition::Type::UNKNOWN;
120   }
121   std::string str = stream.str();
122   xbt_assert(str.size() + 1 <= answer.buffer.size(),
123              "The serialized simcall is too large for the buffer. Please fix the code.");
124   strncpy(answer.buffer.data(), str.c_str(), answer.buffer.size() - 1);
125   answer.buffer.back() = '\0';
126
127   XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> '%s'", actor->get_cname(), str.c_str());
128   xbt_assert(channel_.send(answer) == 0, "Could not send response");
129 }
130
131 void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
132 {
133   bool terminate_asap = msg->value;
134   XBT_DEBUG("Finalize (terminate = %d)", (int)terminate_asap);
135   if (not terminate_asap) {
136     if (XBT_LOG_ISENABLED(mc_client, xbt_log_priority_debug))
137       kernel::EngineImpl::get_instance()->display_all_actor_status();
138 #if HAVE_SMPI
139     XBT_DEBUG("Smpi_enabled: %d", SMPI_is_inited());
140     if (SMPI_is_inited())
141       SMPI_finalize();
142 #endif
143   }
144   coverage_checkpoint();
145   xbt_assert(channel_.send(MessageType::FINALIZE_REPLY) == 0, "Could not answer to FINALIZE");
146   std::fflush(stdout);
147   if (terminate_asap)
148     ::_Exit(0);
149 }
150 void AppSide::handle_initial_addresses()
151 {
152   this->need_memory_info_                       = true;
153   s_mc_message_initial_addresses_reply_t answer = {};
154   answer.type                                   = MessageType::INITIAL_ADDRESSES_REPLY;
155   answer.mmalloc_default_mdp                    = mmalloc_get_current_heap();
156   xbt_assert(channel_.send(answer) == 0, "Could not send response with initial addresses.");
157 }
158 void AppSide::handle_actors_status() const
159 {
160   auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
161   const int num_actors   = actor_list.size();
162   XBT_DEBUG("Serialize the actors to answer ACTORS_STATUS from the checker. %d actors to go.", num_actors);
163
164   std::vector<s_mc_message_actors_status_one_t> status(num_actors);
165   int i                 = 0;
166
167   for (auto const& [aid, actor] : actor_list) {
168     status[i].aid            = aid;
169     status[i].enabled        = mc::actor_is_enabled(actor);
170     status[i].max_considered = actor->simcall_.observer_->get_max_consider();
171     status[i].n_transitions  = mc::actor_is_enabled(actor) ? status[i].max_considered : 0;
172     i++;
173   }
174
175   struct s_mc_message_actors_status_answer_t answer = {};
176   answer.type             = MessageType::ACTORS_STATUS_REPLY;
177   answer.count            = num_actors;
178
179   xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
180   if (answer.count > 0) {
181     size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t);
182     xbt_assert(channel_.send(status.data(), size) == 0, "Could not send ACTORS_STATUS_REPLY data");
183   }
184
185   // Serialize each transition to describe what each actor is doing
186   XBT_DEBUG("Deliver ACTOR_TRANSITION_PROBE payload");
187   for (const auto& actor_status : status) {
188     if (not actor_status.enabled)
189       continue;
190
191     const auto& actor        = actor_list.at(actor_status.aid);
192     const int max_considered = actor_status.max_considered;
193
194     for (int times_considered = 0; times_considered < max_considered; times_considered++) {
195       std::stringstream stream;
196       s_mc_message_simcall_probe_one_t probe;
197
198       if (actor->simcall_.observer_ != nullptr) {
199         actor->simcall_.observer_->prepare(times_considered);
200         actor->simcall_.observer_->serialize(stream);
201       } else {
202         stream << (short)mc::Transition::Type::UNKNOWN;
203       }
204
205       std::string str = stream.str();
206       xbt_assert(str.size() + 1 <= probe.buffer.size(),
207                  "The serialized transition is too large for the buffer. Please fix the code.");
208       strncpy(probe.buffer.data(), str.c_str(), probe.buffer.size() - 1);
209       probe.buffer.back() = '\0';
210
211       xbt_assert(channel_.send(probe) == 0, "Could not send ACTOR_TRANSITION_PROBE payload");
212     }
213     // NOTE: We do NOT need to reset `times_considered` for each actor's
214     // simcall observer here to the "original" value (i.e. the value BEFORE
215     // multiple prepare() calls were made for serialization purposes) since
216     // each SIMCALL_EXECUTE provides a `times_considered` to be used to prepare
217     // the transition before execution.
218   }
219 }
220 void AppSide::handle_actors_maxpid() const
221 {
222   s_mc_message_int_t answer = {};
223   answer.type               = MessageType::ACTORS_MAXPID_REPLY;
224   answer.value              = kernel::actor::ActorImpl::get_maxpid();
225   xbt_assert(channel_.send(answer) == 0, "Could not send response");
226 }
227
228 #define assert_msg_size(_name_, _type_)                                                                                \
229   xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size,            \
230              sizeof(_type_))
231
232 void AppSide::handle_messages()
233 {
234   while (true) { // Until we get a CONTINUE message
235     XBT_DEBUG("Waiting messages from model-checker");
236
237     std::array<char, MC_MESSAGE_LENGTH> message_buffer;
238     ssize_t received_size = channel_.receive(message_buffer.data(), message_buffer.size());
239
240     if (received_size == 0) {
241       XBT_DEBUG("Socket closed on the Checker side, bailing out.");
242       ::_Exit(0); // Nobody's listening to that process anymore => exit as quickly as possible.
243     }
244     xbt_assert(received_size >= 0, "Could not receive commands from the model-checker");
245     xbt_assert(static_cast<size_t>(received_size) >= sizeof(s_mc_message_t), "Cannot handle short message (size=%zd)",
246                received_size);
247
248     const s_mc_message_t* message = (s_mc_message_t*)message_buffer.data();
249     switch (message->type) {
250       case MessageType::DEADLOCK_CHECK:
251         assert_msg_size("DEADLOCK_CHECK", s_mc_message_t);
252         handle_deadlock_check(message);
253         break;
254
255       case MessageType::CONTINUE:
256         assert_msg_size("MESSAGE_CONTINUE", s_mc_message_t);
257         return;
258
259       case MessageType::SIMCALL_EXECUTE:
260         assert_msg_size("SIMCALL_EXECUTE", s_mc_message_simcall_execute_t);
261         handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data());
262         break;
263
264       case MessageType::FINALIZE:
265         assert_msg_size("FINALIZE", s_mc_message_int_t);
266         handle_finalize((s_mc_message_int_t*)message_buffer.data());
267         break;
268
269       case MessageType::INITIAL_ADDRESSES:
270         assert_msg_size("INITIAL_ADDRESSES", s_mc_message_t);
271         handle_initial_addresses();
272         break;
273
274       case MessageType::ACTORS_STATUS:
275         assert_msg_size("ACTORS_STATUS", s_mc_message_t);
276         handle_actors_status();
277         break;
278
279       case MessageType::ACTORS_MAXPID:
280         assert_msg_size("ACTORS_MAXPID", s_mc_message_t);
281         handle_actors_maxpid();
282         break;
283
284       default:
285         xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
286         break;
287     }
288   }
289 }
290
291 void AppSide::main_loop()
292 {
293   simgrid::mc::processes_time.resize(simgrid::kernel::actor::ActorImpl::get_maxpid());
294   MC_ignore_heap(simgrid::mc::processes_time.data(),
295                  simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
296
297   sthread_disable();
298   coverage_checkpoint();
299   sthread_enable();
300   while (true) {
301     simgrid::mc::execute_actors();
302     xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send WAITING message to model-checker");
303     this->handle_messages();
304   }
305 }
306
307 void AppSide::report_assertion_failure()
308 {
309   xbt_assert(channel_.send(MessageType::ASSERTION_FAILED) == 0, "Could not send assertion to model-checker");
310   this->handle_messages();
311 }
312
313 void AppSide::ignore_memory(void* addr, std::size_t size) const
314 {
315   if (not MC_is_active() || not need_memory_info_)
316     return;
317
318   s_mc_message_ignore_memory_t message = {};
319   message.type = MessageType::IGNORE_MEMORY;
320   message.addr = (std::uintptr_t)addr;
321   message.size = size;
322   xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_MEMORY message to model-checker");
323 }
324
325 void AppSide::ignore_heap(void* address, std::size_t size) const
326 {
327   if (not MC_is_active() || not need_memory_info_)
328     return;
329
330   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
331
332   s_mc_message_ignore_heap_t message = {};
333   message.type    = MessageType::IGNORE_HEAP;
334   message.address = address;
335   message.size    = size;
336   message.block   = ((char*)address - (char*)heap->heapbase) / BLOCKSIZE + 1;
337   if (heap->heapinfo[message.block].type == 0) {
338     message.fragment = -1;
339     heap->heapinfo[message.block].busy_block.ignore++;
340   } else {
341     message.fragment = (ADDR2UINT(address) % BLOCKSIZE) >> heap->heapinfo[message.block].type;
342     heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
343   }
344
345   xbt_assert(channel_.send(message) == 0, "Could not send ignored region to MCer");
346 }
347
348 void AppSide::unignore_heap(void* address, std::size_t size) const
349 {
350   if (not MC_is_active() || not need_memory_info_)
351     return;
352
353   s_mc_message_ignore_memory_t message = {};
354   message.type = MessageType::UNIGNORE_HEAP;
355   message.addr = (std::uintptr_t)address;
356   message.size = size;
357   xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_HEAP message to model-checker");
358 }
359
360 void AppSide::declare_symbol(const char* name, int* value) const
361 {
362   if (not MC_is_active() || not need_memory_info_) {
363     XBT_CRITICAL("Ignore AppSide::declare_symbol(%s)", name);
364     return;
365   }
366
367   s_mc_message_register_symbol_t message = {};
368   message.type = MessageType::REGISTER_SYMBOL;
369   xbt_assert(strlen(name) + 1 <= message.name.size(), "Symbol is too long");
370   strncpy(message.name.data(), name, message.name.size() - 1);
371   message.callback = nullptr;
372   message.data     = value;
373   xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker");
374 }
375
376 /** Register a stack in the model checker
377  *
378  *  The stacks are allocated in the heap. The MC handle them specifically
379  *  when we analyze/compare the content of the heap so it must be told where
380  *  they are with this function.
381  */
382 void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
383 {
384   if (not MC_is_active() || not need_memory_info_)
385     return;
386
387   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
388
389   s_stack_region_t region = {};
390   region.address = stack;
391   region.context = context;
392   region.size    = size;
393   region.block   = ((char*)stack - (char*)heap->heapbase) / BLOCKSIZE + 1;
394
395   s_mc_message_stack_region_t message = {};
396   message.type         = MessageType::STACK_REGION;
397   message.stack_region = region;
398   xbt_assert(channel_.send(message) == 0, "Could not send STACK_REGION to model-checker");
399 }
400 } // namespace simgrid::mc