Various cleanups.

[simgrid.git] / src / mc / api / RemoteApp.cpp

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 64aed11e6edf51bdf10915af4b6c18be777cdc39..00f34be192d89c3e9a43026c69c2396dbc9af250 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2015-2023. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -20,9 +20,11 @@
 #include "xbt/log.h"
 #include "xbt/system_error.hpp"
 
+#include <algorithm>
 #include <array>
 #include <boost/tokenizer.hpp>
 #include <memory>
+#include <numeric>
 #include <string>
 
 #include <fcntl.h>
@@ -42,7 +44,7 @@ static simgrid::config::Flag<std::string> _sg_mc_setenv{
 
 namespace simgrid::mc {
 
-static void run_child_process(int socket, const std::vector<char*>& args)
+XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<char*>& args)
 {
   /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
    * env variable is set. If so, MC mode is assumed, and the client is setup from its side
@@ -159,10 +161,14 @@ unsigned long RemoteApp::get_maxpid() const
 
 void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
 {
-  s_mc_message_t msg;
-  memset(&msg, 0, sizeof msg);
-  msg.type = simgrid::mc::MessageType::ACTORS_STATUS;
-  model_checker_->channel().send(msg);
+  // The messaging happens as follows:
+  //
+  // CheckerSide                  AppSide
+  // send ACTORS_STATUS ---->
+  //                    <----- send ACTORS_STATUS_REPLY
+  //                    <----- send `N` `s_mc_message_actors_status_one_t` structs
+  //                    <----- send `M` `s_mc_message_simcall_probe_one_t` structs
+  model_checker_->channel().send(MessageType::ACTORS_STATUS);
 
   s_mc_message_actors_status_answer_t answer;
   ssize_t received = model_checker_->channel().receive(answer);
@@ -180,9 +186,42 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
     xbt_assert(static_cast<size_t>(received) == size);
   }
 
+  std::vector<s_mc_message_simcall_probe_one_t> action_pool(answer.transition_count);
+  if (answer.transition_count > 0) {
+    size_t size = action_pool.size() * sizeof(s_mc_message_simcall_probe_one_t);
+    received    = model_checker_->channel().receive(action_pool.data(), size);
+    xbt_assert(static_cast<size_t>(received) == size);
+  }
+
+  // Ensures that each actor sends precisely `actor.max_considered` transitions. While technically
+  // this doesn't catch the edge case where actor A sends 3 instead of 2 and actor B sends 2 instead
+  // of 3 transitions, that is ignored here since that invariant needs to be enforced on the AppSide
+  const auto expected_transitions = std::accumulate(
+      status.begin(), status.end(), 0, [](int total, const auto& actor) { return total + actor.n_transitions; });
+  xbt_assert(expected_transitions == static_cast<int>(action_pool.size()),
+             "Expected to receive %d transition(s) but was only notified of %lu by the app side", expected_transitions,
+             action_pool.size());
+
   whereto.clear();
-  for (auto const& actor : status)
-    whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered);
+  auto action_pool_iter = std::move_iterator(action_pool.begin());
+
+  for (const auto& actor : status) {
+    xbt_assert(actor.n_transitions == 0 || actor.n_transitions == actor.max_considered,
+               "If any transitions are serialized for an actor, it must match the "
+               "total number of transitions that can be considered for the actor "
+               "(currently %d), but only %d transition(s) was/were said to be encoded",
+               actor.max_considered, actor.n_transitions);
+
+    auto actor_transitions = std::vector<std::unique_ptr<Transition>>(actor.n_transitions);
+    for (int times_considered = 0; times_considered < actor.n_transitions; times_considered++, action_pool_iter++) {
+      std::stringstream stream((*action_pool_iter).buffer.data());
+      auto transition = std::unique_ptr<Transition>(deserialize_transition(actor.aid, times_considered, stream));
+      actor_transitions[times_considered] = std::move(transition);
+    }
+
+    XBT_DEBUG("Received %d transitions for actor %ld", actor.n_transitions, actor.aid);
+    whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions));
+  }
 }
 
 void RemoteApp::check_deadlock() const