MC: stop reading maxpid in memory, but ask it over the network instead

diff --git a/src/kernel/actor/ActorImpl.hpp b/src/kernel/actor/ActorImpl.hpp
index 34c90cb..69741ac 100644 (file)
--- a/src/kernel/actor/ActorImpl.hpp
+++ b/src/kernel/actor/ActorImpl.hpp
@@ -40,8 +40,6 @@ public:
   aid_t get_ppid() const { return ppid_; }
 
   static unsigned long get_maxpid() { return maxpid_; }
-  // In MC mode, the application sends this pointer to the MC
-  static unsigned long* get_maxpid_addr() { return &maxpid_; }
 };
 
 /*------------------------- [ ActorRestartingTrait ] -------------------------*/

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 5efb133..8fca2ee 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -52,6 +52,8 @@ void ModelChecker::start()
         } else if (events == EV_SIGNAL) {
           if (sig == SIGCHLD)
             mc->handle_waitpid();
+          else
+            xbt_die("Unexpected signal: %d", sig);
         } else {
           xbt_die("Unexpected event");
         }
@@ -163,7 +165,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
       memcpy(&message, buffer, sizeof(message));
 
-      get_remote_process().init(message.mmalloc_default_mdp, message.maxpid);
+      get_remote_process().init(message.mmalloc_default_mdp);
       break;
     }
 

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 4addcf5..a5111d1 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -156,7 +156,19 @@ void RemoteApp::restore_initial_state() const
 
 unsigned long RemoteApp::get_maxpid() const
 {
-  return model_checker_->get_remote_process().get_maxpid();
+  // note: we could maybe cache it and count the actor creation on checker side too.
+  // But counting correctly accross state checkpoint/restore would be annoying.
+
+  model_checker_->channel().send(MessageType::ACTORS_MAXPID);
+  s_mc_message_int_t answer;
+  ssize_t answer_size = model_checker_->channel().receive(answer);
+  xbt_assert(answer_size != -1, "Could not receive message");
+  xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
+  xbt_assert(answer.type == MessageType::ACTORS_MAXPID_REPLY,
+             "Received unexpected message %s (%i); expected MessageType::ACTORS_MAXPID_REPLY (%i)",
+             to_c_str(answer.type), (int)answer.type, (int)MessageType::ACTORS_MAXPID_REPLY);
+
+  return answer.value;
 }
 
 void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 4617ec7..b8ba57e 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -77,8 +77,7 @@ AppSide* AppSide::initialize()
 
   s_mc_message_initial_addresses_t message = {};
   message.type                = MessageType::INITIAL_ADDRESSES;
-  message.mmalloc_default_mdp = mmalloc_get_current_heap();
-  message.maxpid              = kernel::actor::ActorImpl::get_maxpid_addr();
+  message.mmalloc_default_mdp              = mmalloc_get_current_heap();
   xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
 
   instance_->handle_messages();
@@ -224,6 +223,13 @@ void AppSide::handle_actors_status() const
       xbt_assert(channel_.send(probe) == 0, "Could not send ACTOR_TRANSITION_PROBE payload");
   }
 }
+void AppSide::handle_actors_maxpid() const
+{
+  s_mc_message_int_t answer = {};
+  answer.type               = MessageType::ACTORS_MAXPID_REPLY;
+  answer.value              = kernel::actor::ActorImpl::get_maxpid();
+  xbt_assert(channel_.send(answer) == 0, "Could not send response");
+}
 
 #define assert_msg_size(_name_, _type_)                                                                                \
   xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size,            \
@@ -267,6 +273,11 @@ void AppSide::handle_messages() const
         handle_actors_status();
         break;
 
+      case MessageType::ACTORS_MAXPID:
+        assert_msg_size("ACTORS_MAXPID", s_mc_message_t);
+        handle_actors_maxpid();
+        break;
+
       default:
         xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
         break;

diff --git a/src/mc/remote/AppSide.hpp b/src/mc/remote/AppSide.hpp
index 6c1afb8..7389f54 100644 (file)
--- a/src/mc/remote/AppSide.hpp
+++ b/src/mc/remote/AppSide.hpp
@@ -33,6 +33,7 @@ private:
   void handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const;
   void handle_finalize(const s_mc_message_int_t* msg) const;
   void handle_actors_status() const;
+  void handle_actors_maxpid() const;
 
 public:
   Channel const& get_channel() const { return channel_; }

diff --git a/src/mc/remote/RemoteProcess.cpp b/src/mc/remote/RemoteProcess.cpp
index ad816fc..fc4e89a 100644 (file)
--- a/src/mc/remote/RemoteProcess.cpp
+++ b/src/mc/remote/RemoteProcess.cpp
@@ -105,10 +105,9 @@ int open_vm(pid_t pid, int flags)
 
 RemoteProcess::RemoteProcess(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
 
-void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid)
+void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp)
 {
-  this->heap_address      = remote(mmalloc_default_mdp);
-  this->maxpid_addr_      = remote(maxpid);
+  this->heap_address = remote(mmalloc_default_mdp);
 
   this->memory_map_ = simgrid::xbt::get_memory_map(this->pid_);
   this->init_memory_map_info();

diff --git a/src/mc/remote/RemoteProcess.hpp b/src/mc/remote/RemoteProcess.hpp
index 3a6b24e..615575c 100644 (file)
--- a/src/mc/remote/RemoteProcess.hpp
+++ b/src/mc/remote/RemoteProcess.hpp
@@ -71,7 +71,7 @@ private:
 public:
   explicit RemoteProcess(pid_t pid);
   ~RemoteProcess() override;
-  void init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid);
+  void init(xbt_mheap_t mmalloc_default_mdp);
 
   RemoteProcess(RemoteProcess const&) = delete;
   RemoteProcess(RemoteProcess&&)      = delete;

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index 435d60d..4eef95b 100644 (file)
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -25,8 +25,8 @@ namespace simgrid::mc {
 
 XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
                        STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
-                       SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, FINALIZE,
-                       FINALIZE_REPLY);
+                       SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID,
+                       ACTORS_MAXPID_REPLY, FINALIZE, FINALIZE_REPLY);
 } // namespace simgrid::mc
 
 constexpr unsigned MC_MESSAGE_LENGTH                 = 512;
@@ -56,7 +56,6 @@ struct s_mc_message_int_t {
 struct s_mc_message_initial_addresses_t {
   simgrid::mc::MessageType type;
   xbt_mheap_t mmalloc_default_mdp;
-  unsigned long* maxpid;
 };
 
 struct s_mc_message_ignore_heap_t {

diff --git a/src/mc/sosp/Snapshot_test.cpp b/src/mc/sosp/Snapshot_test.cpp
index c7a1804..6c52fb6 100644 (file)
--- a/src/mc/sosp/Snapshot_test.cpp
+++ b/src/mc/sosp/Snapshot_test.cpp
@@ -61,7 +61,7 @@ void snap_test_helper::Init()
   REQUIRE(1 << xbt_pagebits == xbt_pagesize);
 
   process = std::make_unique<simgrid::mc::RemoteProcess>(getpid());
-  process->init(nullptr, nullptr);
+  process->init(nullptr);
   mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process), -1);
 }
 

diff --git a/teshsuite/mc/dwarf-expression/dwarf-expression.cpp b/teshsuite/mc/dwarf-expression/dwarf-expression.cpp
index 3853ce5..a9f639d 100644 (file)
--- a/teshsuite/mc/dwarf-expression/dwarf-expression.cpp
+++ b/teshsuite/mc/dwarf-expression/dwarf-expression.cpp
@@ -149,7 +149,7 @@ static void test_deref(simgrid::dwarf::ExpressionContext const& state)
 int main()
 {
   auto* process = new simgrid::mc::RemoteProcess(getpid());
-  process->init(nullptr, nullptr);
+  process->init(nullptr);
 
   simgrid::dwarf::ExpressionContext state;
   state.address_space = (simgrid::mc::AddressSpace*) process;

diff --git a/teshsuite/mc/dwarf/dwarf.cpp b/teshsuite/mc/dwarf/dwarf.cpp
index 18a0c31..39aec32 100644 (file)
--- a/teshsuite/mc/dwarf/dwarf.cpp
+++ b/teshsuite/mc/dwarf/dwarf.cpp
@@ -123,7 +123,7 @@ int main(int argc, char** argv)
   simgrid::mc::Type* type;
 
   simgrid::mc::RemoteProcess process(getpid());
-  process.init(nullptr, nullptr);
+  process.init(nullptr);
 
   test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));