Merge branch 'master' of https://framagit.org/simgrid/simgrid

diff --git a/docs/source/Installing_SimGrid.rst b/docs/source/Installing_SimGrid.rst
index 2e1143b..7cd2404 100644 (file)
--- a/docs/source/Installing_SimGrid.rst
+++ b/docs/source/Installing_SimGrid.rst
@@ -426,11 +426,15 @@ simgrid without downloading the source with pip:
   $ pip install simgrid
 
 If you installed SimGrid to a non-standard directory (such as ``/opt/simgrid`` as advised earlier), you should tell python where
-to find the libraries as follows (notice the ``/lib`` added to the configured prefix).
+to find the libraries as follows (notice the elements suffixed to the configured prefix).
 
 .. code-block:: console
 
-  $ PYTHONPATH="/opt/simgrid/lib" python your_script.py
+  $ PYTHONPATH="/opt/simgrid/lib/python3/dist-packages" LD_LIBRARY_PATH="/opt/simgrid/lib" python your_script.py
 
-You can add the PYTHONPATH variable to your bash profile to not specify it each time by adding this line to your ``~/.profile``:
-``export PYTHONPATH=$PYTHONPATH:/opt/simgrid/lib/``
+You can add those variables to your bash profile to not specify it each time by adding these lines to your ``~/.profile``:
+
+.. code-block:: console
+
+  export PYTHONPATH="$PYTHONPATH:/opt/simgrid/lib/python3/dist-packages"
+  export LD_LIBRARY_PATH="$PYTHONPATH:/opt/simgrid/lib"

diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
index 3a2ddd8..e1087e9 100644 (file)
--- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
+++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
@@ -16,7 +16,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 > [0.000000] [mc_explo/INFO]   3: iSend(mbox=0)
 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
 > [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 140 unique states visited; 33 backtracks (228 transition replays, 401 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 98 unique states visited; 21 backtracks (153 transition replays, 272 states visited overall)
 
 ! expect return 1
 ! timeout 20
@@ -35,7 +35,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 > [0.000000] [mc_explo/INFO]   2: iSend(mbox=0)
 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
 > [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;2;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 157 unique states visited; 32 backtracks (184 transition replays, 373 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 83 unique states visited; 12 backtracks (65 transition replays, 160 states visited overall)
 
 ! expect return 1
 ! timeout 20
@@ -53,8 +53,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 > [0.000000] [mc_explo/INFO]   3: iSend(mbox=0)
 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
 > [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1'
-<<<<<<< HEAD
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 49 unique states visited; 5 backtracks (23 transition replays, 77 states visited overall)
-=======
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 49 unique states visited; 5 backtracks (23 transition replays, 77 states visited overall)
->>>>>>> 3bbac43bba2350e10f84605693da4b1244ef9da2
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 3 backtracks (11 transition replays, 58 states visited overall)

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 7452071..5615d87 100644 (file)
--- a/src/kernel/activity/CommImpl.cpp
+++ b/src/kernel/activity/CommImpl.cpp
@@ -21,6 +21,19 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(ker_network, kernel, "Kernel network-related syn
 
 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);
@@ -109,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 340a19d..4fcf67c 100644 (file)
--- a/src/kernel/activity/CommImpl.hpp
+++ b/src/kernel/activity/CommImpl.hpp
@@ -32,8 +32,11 @@ class XBT_PUBLIC CommImpl : public ActivityImpl_T<CommImpl> {
   s4u::Host* to_     = nullptr; /* Otherwise, computed at start() time from the actors */
   CommImplType type_ = CommImplType::SEND; /* Type of the communication (SEND or RECEIVE) */
 
+  static unsigned next_id_;        // Next ID to be given (for MC)
+  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);
 
@@ -52,7 +55,8 @@ public:
 
   double get_rate() const { return rate_; }
   MailboxImpl* get_mailbox() const { return mbox_; }
-  long get_mailbox_id() const { return mbox_id_; }
+  unsigned get_mailbox_id() const { return mbox_id_; }
+  unsigned get_id() const { return id_; }
   bool is_detached() const { return detached_; }
   bool is_assigned() const { return (to_ != nullptr && from_ != nullptr); }
 
@@ -79,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/kernel/actor/CommObserver.cpp b/src/kernel/actor/CommObserver.cpp
index 6b87562..bb2d4bf 100644 (file)
--- a/src/kernel/actor/CommObserver.cpp
+++ b/src/kernel/actor/CommObserver.cpp
@@ -43,7 +43,7 @@ static void serialize_activity_test(const activity::ActivityImpl* act, std::stri
 {
   if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
     stream << "  " << (short)mc::Transition::Type::COMM_TEST;
-    stream << ' ' << (uintptr_t)comm;
+    stream << ' ' << comm->get_id();
     stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
     stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
     stream << ' ' << comm->get_mailbox_id();
@@ -57,7 +57,7 @@ static std::string to_string_activity_test(const activity::ActivityImpl* act)
   if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
     const std::string src_buff_id = ptr_to_id<unsigned char>(comm->src_buff_);
     const std::string dst_buff_id = ptr_to_id<unsigned char>(comm->dst_buff_);
-    return "CommTest(comm_id:" + ptr_to_id<activity::CommImpl const>(comm) +
+    return "CommTest(comm_id:" + std::to_string(comm->get_id()) +
            " src:" + std::to_string(comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1) +
            " dst:" + std::to_string(comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1) +
            " mbox:" + std::to_string(comm->get_mailbox_id()) + " srcbuf:" + src_buff_id + " dstbuf:" + dst_buff_id +
@@ -97,7 +97,7 @@ static void serialize_activity_wait(const activity::ActivityImpl* act, bool time
 {
   if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
     stream << (short)mc::Transition::Type::COMM_WAIT << ' ';
-    stream << timeout << ' ' << (uintptr_t)comm;
+    stream << timeout << ' ' << comm->get_id();
 
     stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
     stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
@@ -112,7 +112,7 @@ static std::string to_string_activity_wait(const activity::ActivityImpl* act)
   if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
     const std::string src_buff_id = ptr_to_id<unsigned char>(comm->src_buff_);
     const std::string dst_buff_id = ptr_to_id<unsigned char>(comm->dst_buff_);
-    return "CommWait(comm_id:" + ptr_to_id<activity::CommImpl const>(comm) +
+    return "CommWait(comm_id:" + std::to_string(comm->get_id()) +
            " src:" + std::to_string(comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1) +
            " dst:" + std::to_string(comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1) +
            " mbox:" + (comm->get_mailbox() == nullptr ? "-" : comm->get_mailbox()->get_name()) +
@@ -204,15 +204,15 @@ void CommIsendSimcall::serialize(std::stringstream& stream) const
 {
   /* Note that the comm_ is 0 until after the execution of the simcall */
   stream << (short)mc::Transition::Type::COMM_ASYNC_SEND << ' ';
-  stream << (uintptr_t)comm_ << ' ' << mbox_->get_id() << ' ' << (uintptr_t)src_buff_ << ' ' << src_buff_size_ << ' '
-         << tag_;
+  stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << (uintptr_t)src_buff_ << ' '
+         << src_buff_size_ << ' ' << tag_;
   XBT_DEBUG("SendObserver comm:%p mbox:%u buff:%p size:%zu tag:%d", comm_, mbox_->get_id(), src_buff_, src_buff_size_,
             tag_);
   stream << ' ' << fun_call_;
 }
 std::string CommIsendSimcall::to_string() const
 {
-  return "CommAsyncSend(comm_id: " + std::to_string((uintptr_t)comm_) + " mbox:" + std::to_string(mbox_->get_id()) +
+  return "CommAsyncSend(comm_id: " + std::to_string(comm_->get_id()) + " mbox:" + std::to_string(mbox_->get_id()) +
          " srcbuf:" + ptr_to_id<unsigned char>(src_buff_) + " bufsize:" + std::to_string(src_buff_size_) +
          " tag: " + std::to_string(tag_) + ")";
 }
@@ -221,15 +221,14 @@ void CommIrecvSimcall::serialize(std::stringstream& stream) const
 {
   /* Note that the comm_ is 0 until after the execution of the simcall */
   stream << (short)mc::Transition::Type::COMM_ASYNC_RECV << ' ';
-  stream << (uintptr_t)comm_ << ' ' << mbox_->get_id() << ' ' << (uintptr_t)dst_buff_ << ' ' << tag_;
+  stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << (uintptr_t)dst_buff_ << ' ' << tag_;
   XBT_DEBUG("RecvObserver comm:%p mbox:%u buff:%p tag:%d", comm_, mbox_->get_id(), dst_buff_, tag_);
   stream << ' ' << fun_call_;
 }
 std::string CommIrecvSimcall::to_string() const
 {
-  return "CommAsyncRecv(comm_id: " + ptr_to_id<activity::CommImpl const>(comm_) +
-         " mbox:" + std::to_string(mbox_->get_id()) + " dstbuf:" + ptr_to_id<unsigned char>(dst_buff_) +
-         " tag: " + std::to_string(tag_) + ")";
+  return "CommAsyncRecv(comm_id: " + std::to_string(comm_->get_id()) + " mbox:" + std::to_string(mbox_->get_id()) +
+         " dstbuf:" + ptr_to_id<unsigned char>(dst_buff_) + " tag: " + std::to_string(tag_) + ")";
 }
 
 } // namespace simgrid::kernel::actor

diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
index d9d8e26..deeec23 100644 (file)
--- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp
+++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
@@ -166,7 +166,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
   });
   xbt_assert(issuer != C.end(),
              "Invariant violation! A (supposedly) enabled `CommWait` transition "
-             "waiting on communication %lu should not be enabled: the receive/send "
+             "waiting on communication %u should not be enabled: the receive/send "
              "transition which generated the communication is not an action taken "
              "to reach state(C) (the state of the configuration), which should "
              "be an impossibility if `%s` is enabled. Please report this as "
@@ -409,7 +409,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
   });
   xbt_assert(issuer != C.end(),
              "An enabled `CommTest` transition (%s) is testing a communication"
-             "%lu not created by a receive/send "
+             "%u not created by a receive/send "
              "transition. SimGrid cannot currently handle test actions "
              "under which a test is performed on a communication that was "
              "not directly created by a receive/send operation of the same actor.",

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
   {

diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp
index f6886c3..56c785b 100644 (file)
--- a/src/mc/transition/TransitionComm.cpp
+++ b/src/mc/transition/TransitionComm.cpp
@@ -18,15 +18,15 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_comm, mc_transition,
 
 namespace simgrid::mc {
 
-CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, uintptr_t comm_,
-                                       aid_t sender_, aid_t receiver_, unsigned mbox_, uintptr_t sbuff_,
-                                       uintptr_t rbuff_, size_t size_)
+CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, unsigned comm_, aid_t sender_,
+                                       aid_t receiver_, unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_,
+                                       size_t size_)
     : Transition(Type::COMM_WAIT, issuer, times_considered)
     , timeout_(timeout_)
     , comm_(comm_)
+    , mbox_(mbox_)
     , sender_(sender_)
     , receiver_(receiver_)
-    , mbox_(mbox_)
     , sbuff_(sbuff_)
     , rbuff_(rbuff_)
     , size_(size_)
@@ -37,8 +37,8 @@ CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, std::
 {
   xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >>
              user_fun_call_);
-  XBT_DEBUG("CommWaitTransition %s comm:%" PRIxPTR ", sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR
-            " rbuff:%" PRIxPTR " size:%zu",
+  XBT_DEBUG("CommWaitTransition %s comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
+            " size:%zu",
             (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
 }
 std::string CommWaitTransition::to_string(bool verbose) const
@@ -68,14 +68,14 @@ bool CommWaitTransition::depends(const Transition* other) const
 
   return false; // Comm transitions are INDEP with non-comm transitions
 }
-CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, uintptr_t comm_, aid_t sender_,
+CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_,
                                        aid_t receiver_, unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_,
                                        size_t size_)
     : Transition(Type::COMM_TEST, issuer, times_considered)
     , comm_(comm_)
+    , mbox_(mbox_)
     , sender_(sender_)
     , receiver_(receiver_)
-    , mbox_(mbox_)
     , sbuff_(sbuff_)
     , rbuff_(rbuff_)
     , size_(size_)
@@ -85,7 +85,7 @@ CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::
     : Transition(Type::COMM_TEST, issuer, times_considered)
 {
   xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> user_fun_call_);
-  XBT_DEBUG("CommTestTransition comm:%" PRIxPTR ", sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
+  XBT_DEBUG("CommTestTransition comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
             " size:%zu",
             comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
 }
@@ -122,7 +122,7 @@ bool CommTestTransition::depends(const Transition* other) const
   return false; // Comm transitions are INDEP with non-comm transitions
 }
 
-CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_,
                                        uintptr_t rbuff_, int tag_)
     : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
     , comm_(comm_)
@@ -163,7 +163,7 @@ bool CommRecvTransition::depends(const Transition* other) const
     if (mbox_ != test->mbox_)
       return false;
 
-    if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->rbuff_ != rbuff_))
+    if ((aid_ != test->sender_) && (aid_ != test->receiver_))
       return false;
 
     // If the test is checking a paired comm already, we're independent!
@@ -181,7 +181,7 @@ bool CommRecvTransition::depends(const Transition* other) const
     if (mbox_ != wait->mbox_)
       return false;
 
-    if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->rbuff_ != rbuff_))
+    if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
       return false;
 
     // If the wait is waiting on a paired comm already, we're independent!
@@ -195,7 +195,7 @@ bool CommRecvTransition::depends(const Transition* other) const
   return false; // Comm transitions are INDEP with non-comm transitions
 }
 
-CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_,
                                        uintptr_t sbuff_, size_t size_, int tag_)
     : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
     , comm_(comm_)
@@ -209,7 +209,7 @@ CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::
     : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
 {
   xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_ >> user_fun_call_);
-  XBT_DEBUG("SendTransition comm:%" PRIxPTR " mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_);
+  XBT_DEBUG("SendTransition comm:%u mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_);
 }
 std::string CommSendTransition::to_string(bool verbose = false) const
 {
@@ -239,7 +239,7 @@ bool CommSendTransition::depends(const Transition* other) const
     if (mbox_ != test->mbox_)
       return false;
 
-    if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->sbuff_ != sbuff_))
+    if ((aid_ != test->sender_) && (aid_ != test->receiver_))
       return false;
 
     // If the test is checking a paired comm already, we're independent!
@@ -257,7 +257,7 @@ bool CommSendTransition::depends(const Transition* other) const
     if (mbox_ != wait->mbox_)
       return false;
 
-    if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->sbuff_ != sbuff_))
+    if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
       return false;
 
     // If the wait is waiting on a paired comm already, we're independent!

diff --git a/src/mc/transition/TransitionComm.hpp b/src/mc/transition/TransitionComm.hpp
index 597a530..cf51c18 100644 (file)
--- a/src/mc/transition/TransitionComm.hpp
+++ b/src/mc/transition/TransitionComm.hpp
@@ -21,10 +21,10 @@ class CommTestTransition;
 
 class CommWaitTransition : public Transition {
   bool timeout_;
-  uintptr_t comm_;
+  unsigned comm_;
+  unsigned mbox_;
   aid_t sender_;
   aid_t receiver_;
-  unsigned mbox_;
   uintptr_t sbuff_;
   uintptr_t rbuff_;
   size_t size_;
@@ -33,15 +33,15 @@ class CommWaitTransition : public Transition {
   friend CommTestTransition;
 
 public:
-  CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, uintptr_t comm_, aid_t sender_, aid_t receiver_,
+  CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, unsigned comm_, aid_t sender_, aid_t receiver_,
                      unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
   CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream);
   std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 
   bool get_timeout() const { return timeout_; }
-  /** Address of the corresponding Communication object in the application */
-  uintptr_t get_comm() const { return comm_; }
+  /** ID of the corresponding Communication object in the application, or 0 if unknown */
+  unsigned get_comm() const { return comm_; }
   /** Sender ID */
   aid_t get_sender() const { return sender_; }
   /** Receiver ID */
@@ -56,10 +56,10 @@ public:
   size_t get_size() const { return size_; }
 };
 class CommTestTransition : public Transition {
-  uintptr_t comm_;
+  unsigned comm_;
+  unsigned mbox_;
   aid_t sender_;
   aid_t receiver_;
-  unsigned mbox_;
   uintptr_t sbuff_;
   uintptr_t rbuff_;
   size_t size_;
@@ -67,14 +67,14 @@ class CommTestTransition : public Transition {
   friend CommRecvTransition;
 
 public:
-  CommTestTransition(aid_t issuer, int times_considered, uintptr_t comm_, aid_t sender_, aid_t receiver_,
-                     unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
+  CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_, aid_t receiver_, unsigned mbox_,
+                     uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
   CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream);
   std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 
-  /** Address of the corresponding Communication object in the application */
-  uintptr_t get_comm() const { return comm_; }
+  /** ID of the corresponding Communication object in the application, or 0 if unknown */
+  unsigned get_comm() const { return comm_; }
   /** Sender ID */
   aid_t get_sender() const { return sender_; }
   /** Receiver ID */
@@ -90,19 +90,19 @@ public:
 };
 
 class CommRecvTransition : public Transition {
-  uintptr_t comm_; /* Addr of the CommImpl */
+  unsigned comm_; /* ID of the CommImpl or 0 if not known */
   unsigned mbox_;
   uintptr_t rbuff_;
   int tag_;
 
 public:
-  CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t rbuff_, int tag_);
+  CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, uintptr_t rbuff_, int tag_);
   CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream);
   std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 
-  /** Address of the corresponding Communication object in the application */
-  uintptr_t get_comm() const { return comm_; }
+  /** ID of the corresponding Communication object in the application (or 0 if unknown)*/
+  unsigned get_comm() const { return comm_; }
   /** Mailbox ID */
   unsigned get_mailbox() const { return mbox_; }
   /** Receiver buffer */
@@ -112,21 +112,21 @@ public:
 };
 
 class CommSendTransition : public Transition {
-  uintptr_t comm_; /* Addr of the CommImpl */
+  unsigned comm_;
   unsigned mbox_;
   uintptr_t sbuff_;
   size_t size_;
   int tag_;
 
 public:
-  CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t sbuff_,
-                     size_t size_, int tag_);
+  CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, uintptr_t sbuff_, size_t size_,
+                     int tag_);
   CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream);
   std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 
-  /** Address of the corresponding Communication object in the application */
-  uintptr_t get_comm() const { return comm_; }
+  /** ID of the corresponding Communication object in the application, or 0 if unknown */
+  unsigned get_comm() const { return comm_; }
   /** Mailbox ID */
   unsigned get_mailbox() const { return mbox_; }
   /** Sender buffer */

diff --git a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
index 35dd161..740b47a 100644 (file)
--- a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
+++ b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
@@ -73,4 +73,4 @@ $ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper
 > If this is too much, consider sharing allocations for computation buffers.
 > This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
 > 
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 228 unique states visited; 54 backtracks (866 transition replays, 1148 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 211 unique states visited; 50 backtracks (837 transition replays, 1098 states visited overall)