Fix the liveness tests by ignoring the Comm ID memory that breaks the state equality...

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index e2ca778..2c308dd 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -26,6 +26,7 @@ XBT_PUBLIC int MC_is_active();
 XBT_PUBLIC void MC_automaton_new_propositional_symbol_pointer(const char* id, int* value);
 
 XBT_PUBLIC void MC_ignore(void* addr, size_t size);
+XBT_PUBLIC void MC_unignore(void* addr, size_t size);
 XBT_PUBLIC void MC_ignore_heap(void* address, size_t size);
 XBT_PUBLIC void MC_unignore_heap(void* address, size_t size);
 

diff --git a/src/kernel/activity/CommImpl.cpp b/src/kernel/activity/CommImpl.cpp
index f3b7f48..5615d87 100644 (file)
--- a/src/kernel/activity/CommImpl.cpp
+++ b/src/kernel/activity/CommImpl.cpp
@@ -23,6 +23,17 @@ namespace simgrid::kernel::activity {
 
 unsigned CommImpl::next_id_ = 0;
 
+/* In stateful MC, we need to ignore some private memory that is not relevant to the application state */
+void CommImpl::setup_mc()
+{
+  MC_ignore(&CommImpl::next_id_, sizeof(CommImpl::next_id_));
+}
+
+CommImpl::CommImpl()
+{
+  MC_ignore((void*)&id_, sizeof(id_));
+}
+
 std::function<void(CommImpl*, void*, size_t)> CommImpl::copy_data_callback_ = [](kernel::activity::CommImpl* comm,
                                                                                  void* buff, size_t buff_size) {
   xbt_assert((buff_size == sizeof(void*)), "Cannot copy %zu bytes: must be sizeof(void*)", buff_size);
@@ -111,6 +122,8 @@ CommImpl::~CommImpl()
   } else if (mbox_) {
     mbox_->remove(this);
   }
+
+  MC_unignore((void*)&id_, sizeof(id_));
 }
 
 /**  @brief Starts the simulation of a communication synchro. */

diff --git a/src/kernel/activity/CommImpl.hpp b/src/kernel/activity/CommImpl.hpp
index a096940..4fcf67c 100644 (file)
--- a/src/kernel/activity/CommImpl.hpp
+++ b/src/kernel/activity/CommImpl.hpp
@@ -36,7 +36,7 @@ class XBT_PUBLIC CommImpl : public ActivityImpl_T<CommImpl> {
   const unsigned id_ = ++next_id_; // ID of this comm (for MC) -- 0 as an ID denotes "invalid/unknown comm"
 
 public:
-  CommImpl() = default;
+  CommImpl();
 
   static void set_copy_data_callback(const std::function<void(CommImpl*, void*, size_t)>& callback);
 
@@ -83,6 +83,9 @@ looking if a given communication matches my needs. For that, myself must match t
 expectations of the other side, too. See  */
   std::function<void(CommImpl*, void*, size_t)> copy_data_fun;
 
+  /* In stateful MC, we need to ignore some private memory that is not relevant to the application state */
+  static void setup_mc();
+
   /* Model actions */
   timeout_action_type src_timeout_{nullptr, [](resource::Action* a) { a->unref(); }}; /* timeout set by the sender */
   timeout_action_type dst_timeout_{nullptr, [](resource::Action* a) { a->unref(); }}; /* timeout set by the receiver */

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index b0bed22..af36677 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -74,6 +74,16 @@ void MC_ignore(void* addr, size_t size)
 #endif
 }
 
+void MC_unignore(void* addr, size_t size)
+{
+#if SIMGRID_HAVE_STATEFUL_MC
+  xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE,
+             "This should be called from the client side");
+  if (MC_is_active())
+    AppSide::get()->unignore_memory(addr, size);
+#endif
+}
+
 void MC_ignore_heap(void *address, size_t size)
 {
 #if SIMGRID_HAVE_STATEFUL_MC

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 39326a0..90f221d 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -362,6 +362,7 @@ void AppSide::main_loop()
   simgrid::mc::processes_time.resize(simgrid::kernel::actor::ActorImpl::get_maxpid());
   MC_ignore_heap(simgrid::mc::processes_time.data(),
                  simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
+  kernel::activity::CommImpl::setup_mc();
 
   sthread_disable();
   coverage_checkpoint();
@@ -393,7 +394,24 @@ void AppSide::ignore_memory(void* addr, std::size_t size) const
   message.size = size;
   xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_MEMORY message to model-checker: %s", strerror(errno));
 #else
-  xbt_die("Cannot really call ignore_heap() in non-SIMGRID_MC mode.");
+  xbt_die("Cannot really call ignore_memory() in non-SIMGRID_MC mode.");
+#endif
+}
+
+void AppSide::unignore_memory(void* addr, std::size_t size) const
+{
+  if (not MC_is_active() || not need_memory_info_)
+    return;
+
+#if SIMGRID_HAVE_STATEFUL_MC
+  s_mc_message_ignore_memory_t message = {};
+  message.type                         = MessageType::UNIGNORE_MEMORY;
+  message.addr                         = (std::uintptr_t)addr;
+  message.size                         = size;
+  xbt_assert(channel_.send(message) == 0, "Could not send UNIGNORE_MEMORY message to model-checker: %s",
+             strerror(errno));
+#else
+  xbt_die("Cannot really call unignore_memory() in non-SIMGRID_MC mode.");
 #endif
 }
 

diff --git a/src/mc/remote/AppSide.hpp b/src/mc/remote/AppSide.hpp
index 3941ffa..57189e6 100644 (file)
--- a/src/mc/remote/AppSide.hpp
+++ b/src/mc/remote/AppSide.hpp
@@ -46,6 +46,7 @@ public:
   XBT_ATTRIB_NORETURN void main_loop();
   void report_assertion_failure();
   void ignore_memory(void* addr, std::size_t size) const;
+  void unignore_memory(void* addr, std::size_t size) const;
   void ignore_heap(void* addr, std::size_t size) const;
   void unignore_heap(void* addr, std::size_t size) const;
   void declare_symbol(const char* name, int* value) const;

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index 4f16f57..f7316ec 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -354,6 +354,20 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size)
       break;
     }
 
+    case MessageType::UNIGNORE_MEMORY: {
+      consumed = sizeof(s_mc_message_ignore_memory_t);
+#if SIMGRID_HAVE_STATEFUL_MC
+      if (remote_memory_ != nullptr) {
+        s_mc_message_ignore_memory_t message;
+        xbt_assert(size >= static_cast<ssize_t>(sizeof(message)), "Broken message");
+        memcpy(&message, buffer, sizeof(message));
+        get_remote_memory()->unignore_region(message.addr, message.size);
+      } else
+#endif
+        XBT_INFO("Ignoring an UNIGNORE_MEMORY message because we don't need to introspect memory.");
+      break;
+    }
+
     case MessageType::STACK_REGION: {
       consumed = sizeof(s_mc_message_stack_region_t);
 #if SIMGRID_HAVE_STATEFUL_MC

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index e4cac55..dfe103b 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, NEED_MEMINFO, NEED_MEMINFO_REPLY, FORK, FORK_REPLY, WAIT_CHILD,
-                       WAIT_CHILD_REPLY, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION,
-                       REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
+                       WAIT_CHILD_REPLY, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, UNIGNORE_MEMORY,
+                       STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
                        SIMCALL_EXECUTE_REPLY, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY_COUNT,
                        ACTORS_STATUS_REPLY_SIMCALL, ACTORS_STATUS_REPLY_TRANSITION, ACTORS_MAXPID, ACTORS_MAXPID_REPLY,
                        FINALIZE, FINALIZE_REPLY);

diff --git a/src/mc/sosp/RemoteProcessMemory.cpp b/src/mc/sosp/RemoteProcessMemory.cpp
index 18093b3..1d256c1 100644 (file)
--- a/src/mc/sosp/RemoteProcessMemory.cpp
+++ b/src/mc/sosp/RemoteProcessMemory.cpp
@@ -395,6 +395,20 @@ void RemoteProcessMemory::ignore_region(std::uint64_t addr, std::size_t size)
     ignored_regions_.insert(pos, region);
 }
 
+void RemoteProcessMemory::unignore_region(std::uint64_t addr, std::size_t size)
+{
+  IgnoredRegion region;
+  region.addr = addr;
+  region.size = size;
+
+  auto pos = std::lower_bound(ignored_regions_.begin(), ignored_regions_.end(), region,
+                              [](auto const& reg1, auto const& reg2) {
+                                return reg1.addr < reg2.addr || (reg1.addr == reg2.addr && reg1.size < reg2.size);
+                              });
+  if (pos != ignored_regions_.end())
+    ignored_regions_.erase(pos);
+}
+
 void RemoteProcessMemory::ignore_heap(IgnoredHeapRegion const& region)
 {
   // Binary search the position of insertion:

diff --git a/src/mc/sosp/RemoteProcessMemory.hpp b/src/mc/sosp/RemoteProcessMemory.hpp
index eeff932..0643a58 100644 (file)
--- a/src/mc/sosp/RemoteProcessMemory.hpp
+++ b/src/mc/sosp/RemoteProcessMemory.hpp
@@ -112,6 +112,7 @@ public:
 
   std::vector<IgnoredRegion> const& ignored_regions() const { return ignored_regions_; }
   void ignore_region(std::uint64_t address, std::size_t size);
+  void unignore_region(std::uint64_t address, std::size_t size);
 
   bool in_maestro_stack(RemotePtr<void> p) const
   {