Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
get_pattern_comm_rdv() defined in mc_api and used in CommDet checker
authorEhsan Azimi <eazimi@ehsan.irisa.fr>
Fri, 20 Nov 2020 17:32:31 +0000 (18:32 +0100)
committerEhsan Azimi <eazimi@ehsan.irisa.fr>
Fri, 20 Nov 2020 17:32:31 +0000 (18:32 +0100)
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/mc_api.cpp
src/mc/mc_api.hpp

index baae6c8..a686d4a 100644 (file)
@@ -192,7 +192,8 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_
 
     char* remote_name = mc_model_checker->get_remote_simulation().read<char*>(RemotePtr<char*>(
         (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_)));
-    pattern->rdv      = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
+    // pattern->rdv      = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
+    pattern->rdv      = mc_api::get().get_pattern_comm_rdv(pattern->comm_addr);
     pattern->src_proc =
         mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid();
     pattern->src_host = MC_smx_actor_get_host_name(issuer);
index b5cb13d..f21715f 100644 (file)
@@ -1,11 +1,13 @@
 #include "mc_api.hpp"
 
+#include "src/kernel/activity/MailboxImpl.hpp"
 #include "src/mc/Session.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
 #include "src/mc/mc_smx.hpp"
 #include "src/mc/remote/RemoteSimulation.hpp"
+#include "src/mc/mc_pattern.hpp"
 
 #include <xbt/asserts.h>
 #include <xbt/log.h>
@@ -207,6 +209,18 @@ void mc_api::copy_index_comm_pattern(const simgrid::mc::State* state) const
   MC_state_copy_index_communications_pattern((simgrid::mc::State*)state);
 }
 
+std::string mc_api::get_pattern_comm_rdv(void* addr) const
+{
+  Remote<kernel::activity::CommImpl> temp_synchro;
+  mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr));
+  const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer();
+
+  char* remote_name = mc_model_checker->get_remote_simulation().read<char*>(RemotePtr<char*>(
+      (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->get_name() : &synchro->mbox_cpy->get_name())));
+  auto rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
+  return rdv;
+}
+
 std::size_t mc_api::get_remote_heap_bytes() const
 {
   RemoteSimulation& process = mc_model_checker->get_remote_simulation();
index 8c9788f..e42ab91 100644 (file)
@@ -46,6 +46,7 @@ public:
   // COMM FUNCTIONS
   void copy_incomplete_comm_pattern(const simgrid::mc::State* state) const;
   void copy_index_comm_pattern(const simgrid::mc::State* state) const;
+  std::string get_pattern_comm_rdv(void* addr) const;
 
   // REMOTE
   std::size_t get_remote_heap_bytes() const;