[mc] Fix MC with the class-hierarchification of simgrid::simix::Synchro

diff --git a/src/mc/AddressSpace.hpp b/src/mc/AddressSpace.hpp
index a5ff9b3..75fbcae 100644 (file)
--- a/src/mc/AddressSpace.hpp
+++ b/src/mc/AddressSpace.hpp
@@ -7,6 +7,7 @@
 #ifndef SIMGRID_MC_ADDRESS_SPACE_H
 #define SIMGRID_MC_ADDRESS_SPACE_H
 
 #ifndef SIMGRID_MC_ADDRESS_SPACE_H
 #define SIMGRID_MC_ADDRESS_SPACE_H
 

+#include <cassert>

 #include <cstddef>
 #include <cstdint>
 #include <type_traits>
 #include <cstddef>
 #include <cstdint>
 #include <type_traits>


@@ -90,6 +91,17 @@ public:
   static constexpr ReadOptions lazy() { return ReadOptions(1); }
 };
 
   static constexpr ReadOptions lazy() { return ReadOptions(1); }
 };
 

+/** A value read from another process */
+template<class T>
+class Remote {
+private:
+  char buffer[sizeof(T)];
+public:
+  void*       data() { return buffer; }
+  const void* data() const { return buffer; }
+  constexpr std::size_t size() const { return sizeof(T); }
+};
+

 /** A given state of a given process (abstract base class)
  *
  *  Currently, this might either be:
 /** A given state of a given process (abstract base class)
  *
  *  Currently, this might either be:


@@ -126,6 +138,12 @@ public:
     this->read_bytes(buffer, sizeof(T), ptr, process_index);
   }
 
     this->read_bytes(buffer, sizeof(T), ptr, process_index);
   }
 

+  template<class T> inline
+  void read(Remote<T>& buffer, RemotePtr<T> ptr, int process_index = ProcessIndexAny)
+  {
+    this->read_bytes(buffer.data(), sizeof(T), ptr, process_index);
+  }
+

   /** Read a given data structure from the address space */
   template<class T> inline
   T read(RemotePtr<T> ptr, int process_index = ProcessIndexMissing)
   /** Read a given data structure from the address space */
   template<class T> inline
   T read(RemotePtr<T> ptr, int process_index = ProcessIndexMissing)

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 9a44b84..dc3ac5f 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -36,7 +36,8 @@ xbt_dynar_t incomplete_communications_pattern;
 
 /********** Static functions ***********/
 
 
 /********** Static functions ***********/
 

-static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) {
+static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
+{

   if(comm1->type != comm2->type)
     return TYPE_DIFF;
   if (comm1->rdv != comm2->rdv)
   if(comm1->type != comm2->type)
     return TYPE_DIFF;
   if (comm1->rdv != comm2->rdv)


@@ -57,7 +58,7 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternC
 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
   char *type, *res;
 
 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
   char *type, *res;
 

-  if(comm->type == SIMIX_COMM_SEND)
+  if (comm->type == simgrid::mc::PatternCommunicationType::send)

     type = bprintf("The send communications pattern of the process %d is different!", process - 1);
   else
     type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
     type = bprintf("The send communications pattern of the process %d is different!", process - 1);
   else
     type = bprintf("The recv communications pattern of the process %d is different!", process - 1);


@@ -92,35 +93,41 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p
   return res;
 }
 
   return res;
 }
 

-static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
+static void update_comm_pattern(
+  simgrid::mc::PatternCommunication* comm_pattern,
+  simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr)

 {
 {

-  s_smx_synchro_t comm;
-  mc_model_checker->process().read(&comm, remote(comm_addr));
+  // HACK, type punning
+  simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+  mc_model_checker->process().read(temp_comm, comm_addr);
+  simgrid::simix::Comm* comm =
+    static_cast<simgrid::simix::Comm*>(temp_comm.data());

 
   smx_process_t src_proc = mc_model_checker->process().resolveProcess(
 
   smx_process_t src_proc = mc_model_checker->process().resolveProcess(

-    simgrid::mc::remote(comm.comm.src_proc));
+    simgrid::mc::remote(comm->src_proc));

   smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
   smx_process_t dst_proc = mc_model_checker->process().resolveProcess(

-    simgrid::mc::remote(comm.comm.dst_proc));
+    simgrid::mc::remote(comm->dst_proc));

   comm_pattern->src_proc = src_proc->pid;
   comm_pattern->dst_proc = dst_proc->pid;
   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
   comm_pattern->src_proc = src_proc->pid;
   comm_pattern->dst_proc = dst_proc->pid;
   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);

-  if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
+  if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {

     size_t buff_size;
     mc_model_checker->process().read(
     size_t buff_size;
     mc_model_checker->process().read(

-      &buff_size, remote(comm.comm.dst_buff_size));
+      &buff_size, remote(comm->dst_buff_size));

     comm_pattern->data.resize(buff_size);
     mc_model_checker->process().read_bytes(
       comm_pattern->data.data(), comm_pattern->data.size(),
     comm_pattern->data.resize(buff_size);
     mc_model_checker->process().read_bytes(
       comm_pattern->data.data(), comm_pattern->data.size(),

-      remote(comm.comm.src_buff));
+      remote(comm->src_buff));

   }
 }
 
 namespace simgrid {
 namespace mc {
 
   }
 }
 
 namespace simgrid {
 namespace mc {
 

-void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
-
+void CommunicationDeterminismChecker::deterministic_comm_pattern(
+  int process, simgrid::mc::PatternCommunication* comm, int backtracking)
+{

   simgrid::mc::PatternCommunicationList* list =
     xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
 
   simgrid::mc::PatternCommunicationList* list =
     xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
 


@@ -129,12 +136,12 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, si
       compare_comm_pattern(list->list[list->index_comm].get(), comm);
 
     if (diff != NONE_DIFF) {
       compare_comm_pattern(list->list[list->index_comm].get(), comm);
 
     if (diff != NONE_DIFF) {

-      if (comm->type == SIMIX_COMM_SEND){
+      if (comm->type == simgrid::mc::PatternCommunicationType::send) {

         this->send_deterministic = 0;
         if (this->send_diff != nullptr)
           xbt_free(this->send_diff);
         this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
         this->send_deterministic = 0;
         if (this->send_diff != nullptr)
           xbt_free(this->send_diff);
         this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);

-      }else{
+      } else {

         this->recv_deterministic = 0;
         if (this->recv_diff != nullptr)
           xbt_free(this->recv_diff);
         this->recv_deterministic = 0;
         if (this->recv_diff != nullptr)
           xbt_free(this->recv_diff);


@@ -185,17 +192,20 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
 
   if (call_type == MC_CALL_TYPE_SEND) {
     /* Create comm pattern */
 
   if (call_type == MC_CALL_TYPE_SEND) {
     /* Create comm pattern */

-    pattern->type = SIMIX_COMM_SEND;
+    pattern->type = simgrid::mc::PatternCommunicationType::send;

     pattern->comm_addr = simcall_comm_isend__get__result(request);
 
     pattern->comm_addr = simcall_comm_isend__get__result(request);
 

-    s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
-      (std::uint64_t) pattern->comm_addr);
+    simgrid::mc::Remote<simgrid::simix::Comm> temp_synchro;
+    mc_model_checker->process().read(temp_synchro, remote(
+      static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
+    simgrid::simix::Comm* synchro =
+      static_cast<simgrid::simix::Comm*>(temp_synchro.data());

 
     char* remote_name = mc_model_checker->process().read<char*>(
 
     char* remote_name = mc_model_checker->process().read<char*>(

-      (std::uint64_t)(synchro.comm.mbox ? &synchro.comm.mbox->name : &synchro.comm.mbox_cpy->name));
+      (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name));

     pattern->rdv = mc_model_checker->process().read_string(remote_name);
     pattern->src_proc = mc_model_checker->process().resolveProcess(
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
     pattern->src_proc = mc_model_checker->process().resolveProcess(

-      simgrid::mc::remote(synchro.comm.src_proc))->pid;
+      simgrid::mc::remote(synchro->src_proc))->pid;

     pattern->src_host = MC_smx_process_get_host_name(issuer);
 
     struct s_smpi_mpi_request mpi_request =
     pattern->src_host = MC_smx_process_get_host_name(issuer);
 
     struct s_smpi_mpi_request mpi_request =


@@ -203,11 +213,11 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
         (std::uint64_t) simcall_comm_isend__get__data(request));
     pattern->tag = mpi_request.tag;
 
         (std::uint64_t) simcall_comm_isend__get__data(request));
     pattern->tag = mpi_request.tag;
 

-    if(synchro.comm.src_buff != nullptr){
-      pattern->data.resize(synchro.comm.src_buff_size);
+    if (synchro->src_buff != nullptr){
+      pattern->data.resize(synchro->src_buff_size);

       mc_model_checker->process().read_bytes(
         pattern->data.data(), pattern->data.size(),
       mc_model_checker->process().read_bytes(
         pattern->data.data(), pattern->data.size(),

-        remote(synchro.comm.src_buff));
+        remote(synchro->src_buff));

     }
     if(mpi_request.detached){
       if (!this->initial_communications_pattern_done) {
     }
     if(mpi_request.detached){
       if (!this->initial_communications_pattern_done) {


@@ -226,7 +236,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
       return;
     }
   } else if (call_type == MC_CALL_TYPE_RECV) {
       return;
     }
   } else if (call_type == MC_CALL_TYPE_RECV) {

-    pattern->type = SIMIX_COMM_RECEIVE;
+    pattern->type = simgrid::mc::PatternCommunicationType::receive;

     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 
     struct s_smpi_mpi_request mpi_request;
     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 
     struct s_smpi_mpi_request mpi_request;


@@ -234,15 +244,18 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
       &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
     pattern->tag = mpi_request.tag;
 
       &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
     pattern->tag = mpi_request.tag;
 

-    s_smx_synchro_t synchro;
-    mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
+    simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+    mc_model_checker->process().read(temp_comm, remote(
+      static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
+    simgrid::simix::Comm* comm =
+      static_cast<simgrid::simix::Comm*>(temp_comm.data());

 
     char* remote_name;
     mc_model_checker->process().read(&remote_name,
 
     char* remote_name;
     mc_model_checker->process().read(&remote_name,

-      remote(synchro.comm.mbox ? &synchro.comm.mbox->name : &synchro.comm.mbox_cpy->name));
+      remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));

     pattern->rdv = mc_model_checker->process().read_string(remote_name);
     pattern->dst_proc = mc_model_checker->process().resolveProcess(
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
     pattern->dst_proc = mc_model_checker->process().resolveProcess(

-      simgrid::mc::remote(synchro.comm.dst_proc))->pid;
+      simgrid::mc::remote(comm->dst_proc))->pid;

     pattern->dst_host = MC_smx_process_get_host_name(issuer);
   } else
     xbt_die("Unexpected call_type %i", (int) call_type);
     pattern->dst_host = MC_smx_process_get_host_name(issuer);
   } else
     xbt_die("Unexpected call_type %i", (int) call_type);


@@ -256,7 +269,9 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
 }
 
 
 }
 
 

-void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking)
+void CommunicationDeterminismChecker::complete_comm_pattern(
+  xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr,
+  unsigned int issuer, int backtracking)

 {
   simgrid::mc::PatternCommunication* current_comm_pattern;
   unsigned int cursor = 0;
 {
   simgrid::mc::PatternCommunication* current_comm_pattern;
   unsigned int cursor = 0;


@@ -265,7 +280,7 @@ void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, sm
 
   /* Complete comm pattern */
   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
 
   /* Complete comm pattern */
   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)

-    if (current_comm_pattern->comm_addr == comm_addr) {
+    if (remote(current_comm_pattern->comm_addr) == comm_addr) {

       update_comm_pattern(current_comm_pattern, comm_addr);
       completed = 1;
       simgrid::mc::PatternCommunication* temp;
       update_comm_pattern(current_comm_pattern, comm_addr);
       completed = 1;
       simgrid::mc::PatternCommunication* temp;

diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp
index 0680226..6235b80 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.hpp
+++ b/src/mc/CommunicationDeterminismChecker.hpp
@@ -35,7 +35,9 @@ private:
 public:
   // These are used by functions which should be moved in CommunicationDeterminismChecker:
   void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
 public:
   // These are used by functions which should be moved in CommunicationDeterminismChecker:
   void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);

-  void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
+  void complete_comm_pattern(
+    xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr,
+    unsigned int issuer, int backtracking);

 private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;
 private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;

diff --git a/src/mc/Type.hpp b/src/mc/Type.hpp
index 972b08d..5551e23 100644 (file)
--- a/src/mc/Type.hpp
+++ b/src/mc/Type.hpp
@@ -29,10 +29,14 @@ namespace mc {
  */
 class Member {
 public:
  */
 class Member {
 public:

+  typedef int flags_type;
+  static constexpr flags_type INHERITANCE_FLAG = 1;
+  static constexpr flags_type VIRTUAL_POINTER_FLAG = 2;
+

   Member() {}
 
   /** Whether this member represent some inherited part of the object */
   Member() {}
 
   /** Whether this member represent some inherited part of the object */

-  bool inheritance = false;
+  flags_type flags = 0;

 
   /** Name of the member (if any) */
   std::string name;
 
   /** Name of the member (if any) */
   std::string name;


@@ -45,6 +49,15 @@ public:
   unsigned type_id = 0;
   simgrid::mc::Type* type = nullptr;
 
   unsigned type_id = 0;
   simgrid::mc::Type* type = nullptr;
 

+  bool isInheritance() const
+  {
+    return this->flags & INHERITANCE_FLAG;
+  }
+  bool isVirtualPointer() const
+  {
+    return this->flags & VIRTUAL_POINTER_FLAG;
+  }
+

   /** Whether the member is at a fixed offset from the base address */
   bool has_offset_location() const
   {
   /** Whether the member is at a fixed offset from the base address */
   bool has_offset_location() const
   {

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 56d1ebd..df6234a 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -6,6 +6,8 @@
 
 #include <cassert>
 
 
 #include <cassert>
 

+#include <algorithm>
+

 #include <simgrid_config.h>
 
 #include <xbt/log.h>
 #include <simgrid_config.h>
 
 #include <xbt/log.h>


@@ -21,7 +23,11 @@
 #include "src/mc/mc_protocol.h"
 
 #include "src/simix/Synchro.h"
 #include "src/mc/mc_protocol.h"
 
 #include "src/simix/Synchro.h"

+#include "src/simix/SynchroIo.hpp"

 #include "src/simix/SynchroComm.hpp"
 #include "src/simix/SynchroComm.hpp"

+#include "src/simix/SynchroRaw.hpp"
+#include "src/simix/SynchroSleep.hpp"
+#include "src/simix/SynchroExec.hpp"

 
 #if HAVE_MC
 #include "src/mc/mc_request.h"
 
 #if HAVE_MC
 #include "src/mc/mc_request.h"


@@ -73,9 +79,7 @@ void wait_for_requests(void)
 bool request_is_enabled(smx_simcall_t req)
 {
   unsigned int index = 0;
 bool request_is_enabled(smx_simcall_t req)
 {
   unsigned int index = 0;

-#if HAVE_MC
-  simgrid::simix::Synchro temp_synchro;
-#endif
+  // TODO, add support for the subtypes?

 
   switch (req->call) {
   case SIMCALL_NONE:
 
   switch (req->call) {
   case SIMCALL_NONE:


@@ -88,9 +92,11 @@ bool request_is_enabled(smx_simcall_t req)
 
 #if HAVE_MC
     // Fetch from MCed memory:
 
 #if HAVE_MC
     // Fetch from MCed memory:

+    // HACK, type puning
+    simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;

     if (mc_model_checker != nullptr) {
     if (mc_model_checker != nullptr) {

-      mc_model_checker->process().read(&temp_synchro, remote(act));
-      act = &temp_synchro;
+      mc_model_checker->process().read(temp_comm, remote(act));
+      act = static_cast<simgrid::simix::Comm*>(temp_comm.data());

     }
 #endif
 
     }
 #endif
 


@@ -136,10 +142,12 @@ bool request_is_enabled(smx_simcall_t req)
     for (index = 0; index < comms->used; ++index) {
 #if HAVE_MC
       // Fetch act from MCed memory:
     for (index = 0; index < comms->used; ++index) {
 #if HAVE_MC
       // Fetch act from MCed memory:

+      // HACK, type puning
+      simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;

       if (mc_model_checker != nullptr) {
         memcpy(&act, buffer + comms->elmsize * index, sizeof(act));
       if (mc_model_checker != nullptr) {
         memcpy(&act, buffer + comms->elmsize * index, sizeof(act));

-        mc_model_checker->process().read(&temp_synchro, remote(act));
-        act = &temp_synchro;
+        mc_model_checker->process().read(temp_comm, remote(act));
+        act = static_cast<simgrid::simix::Comm*>(temp_comm.data());

       }
       else
 #endif
       }
       else
 #endif

diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp
index 1241a60..0b2549e 100644 (file)
--- a/src/mc/mc_comm_pattern.cpp
+++ b/src/mc/mc_comm_pattern.cpp
@@ -87,13 +87,17 @@ void MC_handle_comm_pattern(
   case MC_CALL_TYPE_WAIT:
   case MC_CALL_TYPE_WAITANY:
     {
   case MC_CALL_TYPE_WAIT:
   case MC_CALL_TYPE_WAITANY:
     {

-      smx_synchro_t comm_addr = nullptr;
+      simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr = nullptr;

       if (call_type == MC_CALL_TYPE_WAIT)
       if (call_type == MC_CALL_TYPE_WAIT)

-        comm_addr = simcall_comm_wait__get__comm(req);
-      else
+        comm_addr = remote(static_cast<simgrid::simix::Comm*>(
+          simcall_comm_wait__get__comm(req)));
+      else {
+        simgrid::simix::Comm* addr;

         // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
         // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):

-        simgrid::mc::read_element(mc_model_checker->process(), &comm_addr,
+        simgrid::mc::read_element(mc_model_checker->process(), &addr,

           remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));
           remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));

+        comm_addr = remote(addr);
+      }

       checker->complete_comm_pattern(pattern, comm_addr,
         MC_smx_simcall_get_issuer(req)->pid, backtracking);
     }
       checker->complete_comm_pattern(pattern, comm_addr,
         MC_smx_simcall_get_issuer(req)->pid, backtracking);
     }

diff --git a/src/mc/mc_dwarf.cpp b/src/mc/mc_dwarf.cpp
index 32742ef..30b5f38 100644 (file)
--- a/src/mc/mc_dwarf.cpp
+++ b/src/mc/mc_dwarf.cpp
@@ -17,6 +17,8 @@
 #include <dwarf.h>
 #include <elfutils/libdw.h>
 
 #include <dwarf.h>
 #include <elfutils/libdw.h>
 

+#include <boost/algorithm/string/predicate.hpp>
+

 #include <simgrid_config.h>
 #include "src/simgrid/util.hpp"
 #include <xbt/log.h>
 #include <simgrid_config.h>
 #include "src/simgrid/util.hpp"
 #include <xbt/log.h>


@@ -571,11 +573,35 @@ static void MC_dwarf_add_members(simgrid::mc::ObjectInformation* info, Dwarf_Die
 
       // TODO, we should use another type (because is is not a type but a member)
       simgrid::mc::Member member;
 
       // TODO, we should use another type (because is is not a type but a member)
       simgrid::mc::Member member;

-      member.inheritance = tag == DW_TAG_inheritance;
+      if (tag == DW_TAG_inheritance)
+        member.flags |= simgrid::mc::Member::INHERITANCE_FLAG;

 
       const char *name = MC_dwarf_attr_integrate_string(&child, DW_AT_name);
       if (name)
         member.name = name;
 
       const char *name = MC_dwarf_attr_integrate_string(&child, DW_AT_name);
       if (name)
         member.name = name;

+      // Those base names are used by GCC and clang for virtual table pointers
+      // respectively ("__vptr$ClassName", "__vptr.ClassName"):
+      if (boost::algorithm::starts_with(member.name, "__vptr$") ||
+        boost::algorithm::starts_with(member.name, "__vptr."))
+        member.flags |= simgrid::mc::Member::VIRTUAL_POINTER_FLAG;
+      // A cleaner stolution would be to check against the type:
+      // ---
+      // tag: DW_TAG_member
+      // name: "_vptr$Foo"
+      // type:
+      //   # Type for a pointer to a vtable
+      //   tag: DW_TAG_pointer_type
+      //   type:
+      //     # Type for a vtable:
+      //     tag: DW_TAG_pointer_type
+      //     name: "__vtbl_ptr_type"
+      //     type:
+      //       tag: DW_TAG_subroutine_type
+      //       type:
+      //         tag: DW_TAG_base_type
+      //         name: "int"
+      // ---
+

       member.byte_size =
           MC_dwarf_attr_integrate_uint(&child, DW_AT_byte_size, 0);
       member.type_id = MC_dwarf_at_type(&child);
       member.byte_size =
           MC_dwarf_attr_integrate_uint(&child, DW_AT_byte_size, 0);
       member.type_id = MC_dwarf_at_type(&child);

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index a1c4361..1d37779 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -27,13 +27,13 @@ static char *pointer_to_string(void *pointer);
 static char *buff_size_to_string(size_t size);
 
 static inline
 static char *buff_size_to_string(size_t size);
 
 static inline

-smx_synchro_t MC_get_comm(smx_simcall_t r)
+simgrid::simix::Comm* MC_get_comm(smx_simcall_t r)

 {
   switch (r->call ) {
   case SIMCALL_COMM_WAIT:
 {
   switch (r->call ) {
   case SIMCALL_COMM_WAIT:

-    return simcall_comm_wait__get__comm(r);
+    return static_cast<simgrid::simix::Comm*>(simcall_comm_wait__get__comm(r));

   case SIMCALL_COMM_TEST:
   case SIMCALL_COMM_TEST:

-    return simcall_comm_test__get__comm(r);
+    return static_cast<simgrid::simix::Comm*>(simcall_comm_test__get__comm(r));

   default:
     return nullptr;
   }
   default:
     return nullptr;
   }


@@ -67,33 +67,33 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
 
   // Those are internal requests, we do not need indirection
   // because those objects are copies:
 
   // Those are internal requests, we do not need indirection
   // because those objects are copies:

-  smx_synchro_t synchro1 = MC_get_comm(r1);
-  smx_synchro_t synchro2 = MC_get_comm(r2);
+  simgrid::simix::Comm* synchro1 = MC_get_comm(r1);
+  simgrid::simix::Comm* synchro2 = MC_get_comm(r2);

 
   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
       && r2->call == SIMCALL_COMM_WAIT) {
 
     smx_mailbox_t mbox = MC_get_mbox(r1);
 
 
   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
       && r2->call == SIMCALL_COMM_WAIT) {
 
     smx_mailbox_t mbox = MC_get_mbox(r1);
 

-    if (mbox != synchro2->comm.mbox_cpy
+    if (mbox != synchro2->mbox_cpy

         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
 
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
 

-    if ((r1->issuer != synchro2->comm.src_proc)
-        && (r1->issuer != synchro2->comm.dst_proc)
+    if ((r1->issuer != synchro2->src_proc)
+        && (r1->issuer != synchro2->dst_proc)

         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
 
     if ((r1->call == SIMCALL_COMM_ISEND)
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
 
     if ((r1->call == SIMCALL_COMM_ISEND)

-        && (synchro2->comm.type == SIMIX_COMM_SEND)
-        && (synchro2->comm.src_buff !=
+        && (synchro2->type == SIMIX_COMM_SEND)
+        && (synchro2->src_buff !=

             simcall_comm_isend__get__src_buff(r1))
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
 
     if ((r1->call == SIMCALL_COMM_IRECV)
             simcall_comm_isend__get__src_buff(r1))
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
 
     if ((r1->call == SIMCALL_COMM_IRECV)

-        && (synchro2->comm.type == SIMIX_COMM_RECEIVE)
-        && (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
+        && (synchro2->type == SIMIX_COMM_RECEIVE)
+        && (synchro2->dst_buff != simcall_comm_irecv__get__dst_buff(r1))

         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
   }
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return false;
   }


@@ -109,28 +109,28 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
 
   if (r1->call == SIMCALL_COMM_WAIT
       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
 
   if (r1->call == SIMCALL_COMM_WAIT
       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)

-      && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == nullptr))
+      && (synchro1->src_proc == nullptr || synchro1->dst_proc == nullptr))

     return false;
 
   if (r1->call == SIMCALL_COMM_TEST &&
       (simcall_comm_test__get__comm(r1) == nullptr
     return false;
 
   if (r1->call == SIMCALL_COMM_TEST &&
       (simcall_comm_test__get__comm(r1) == nullptr

-       || synchro1->comm.src_buff == nullptr
-       || synchro1->comm.dst_buff == nullptr))
+       || synchro1->src_buff == nullptr
+       || synchro1->dst_buff == nullptr))

     return false;
 
   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
     return false;
 
   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT

-      && synchro1->comm.src_buff == synchro2->comm.src_buff
-      && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
+      && synchro1->src_buff == synchro2->src_buff
+      && synchro1->dst_buff == synchro2->dst_buff)

     return false;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
     return false;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST

-      && synchro1->comm.src_buff != nullptr
-      && synchro1->comm.dst_buff != nullptr
-      && synchro2->comm.src_buff != nullptr
-      && synchro2->comm.dst_buff != nullptr
-      && synchro1->comm.dst_buff != synchro2->comm.src_buff
-      && synchro1->comm.dst_buff != synchro2->comm.dst_buff
-      && synchro2->comm.dst_buff != synchro1->comm.src_buff)
+      && synchro1->src_buff != nullptr
+      && synchro1->dst_buff != nullptr
+      && synchro2->src_buff != nullptr
+      && synchro2->dst_buff != nullptr
+      && synchro1->dst_buff != synchro2->src_buff
+      && synchro1->dst_buff != synchro2->dst_buff
+      && synchro2->dst_buff != synchro1->src_buff)

     return false;
 
   return true;
     return false;
 
   return true;


@@ -154,25 +154,27 @@ bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
 
   // Those are internal requests, we do not need indirection
   // because those objects are copies:
 
   // Those are internal requests, we do not need indirection
   // because those objects are copies:

-  smx_synchro_t synchro1 = MC_get_comm(r1);
-  smx_synchro_t synchro2 = MC_get_comm(r2);
+  simgrid::simix::Comm* synchro1 = MC_get_comm(r1);
+  simgrid::simix::Comm* synchro2 = MC_get_comm(r2);

 
   switch(r1->call) {
   case SIMCALL_COMM_ISEND:
 
   switch(r1->call) {
   case SIMCALL_COMM_ISEND:

-    return simcall_comm_isend__get__mbox(r1) == simcall_comm_isend__get__mbox(r2);
+    return simcall_comm_isend__get__mbox(r1)
+      == simcall_comm_isend__get__mbox(r2);

   case SIMCALL_COMM_IRECV:
   case SIMCALL_COMM_IRECV:

-    return simcall_comm_irecv__get__mbox(r1) == simcall_comm_irecv__get__mbox(r2);
+    return simcall_comm_irecv__get__mbox(r1)
+      == simcall_comm_irecv__get__mbox(r2);

   case SIMCALL_COMM_WAIT:
   case SIMCALL_COMM_WAIT:

-    if (synchro1->comm.src_buff == synchro2->comm.src_buff
-        && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
+    if (synchro1->src_buff == synchro2->src_buff
+        && synchro1->dst_buff == synchro2->dst_buff)

       return false;
       return false;

-    else if (synchro1->comm.src_buff != nullptr
-        && synchro1->comm.dst_buff != nullptr
-        && synchro2->comm.src_buff != nullptr
-        && synchro2->comm.dst_buff != nullptr
-        && synchro1->comm.dst_buff != synchro2->comm.src_buff
-        && synchro1->comm.dst_buff != synchro2->comm.dst_buff
-        && synchro2->comm.dst_buff != synchro1->comm.src_buff)
+    else if (synchro1->src_buff != nullptr
+        && synchro1->dst_buff != nullptr
+        && synchro2->src_buff != nullptr
+        && synchro2->dst_buff != nullptr
+        && synchro1->dst_buff != synchro2->src_buff
+        && synchro1->dst_buff != synchro2->dst_buff
+        && synchro2->dst_buff != synchro1->src_buff)

       return false;
     else
       return true;
       return false;
     else
       return true;


@@ -273,7 +275,8 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid
   }
 
   case SIMCALL_COMM_WAIT: {
   }
 
   case SIMCALL_COMM_WAIT: {

-    smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
+    simgrid::simix::Comm* remote_act =
+      static_cast<simgrid::simix::Comm*>(simcall_comm_wait__get__comm(req));

     char* p;
     if (value == -1) {
       type = "WaitTimeout";
     char* p;
     if (value == -1) {
       type = "WaitTimeout";


@@ -283,19 +286,19 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid
       type = "Wait";
       p = pointer_to_string(remote_act);
 
       type = "Wait";
       p = pointer_to_string(remote_act);
 

-      s_smx_synchro_t synchro;
-      smx_synchro_t act;
+      simgrid::mc::Remote<simgrid::simix::Comm> temp_synchro;
+      simgrid::simix::Comm* act;

       if (use_remote_comm) {
       if (use_remote_comm) {

-        mc_model_checker->process().read_bytes(&synchro,
-          sizeof(synchro), remote(remote_act));
-        act = &synchro;
+        mc_model_checker->process().read(temp_synchro, remote(
+          static_cast<simgrid::simix::Comm*>(remote_act)));
+        act = static_cast<simgrid::simix::Comm*>(temp_synchro.data());

       } else
         act = remote_act;
 
       smx_process_t src_proc = mc_model_checker->process().resolveProcess(
       } else
         act = remote_act;
 
       smx_process_t src_proc = mc_model_checker->process().resolveProcess(

-        simgrid::mc::remote(act->comm.src_proc));
+        simgrid::mc::remote(act->src_proc));

       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(

-        simgrid::mc::remote(act->comm.dst_proc));
+        simgrid::mc::remote(act->dst_proc));

       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
                      src_proc ? src_proc->pid : 0,
                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",
       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
                      src_proc ? src_proc->pid : 0,
                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",


@@ -309,18 +312,19 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid
   }
 
   case SIMCALL_COMM_TEST: {
   }
 
   case SIMCALL_COMM_TEST: {

-    smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
-    s_smx_synchro_t synchro;
-      smx_synchro_t act;
-      if (use_remote_comm) {
-        mc_model_checker->process().read_bytes(&synchro,
-          sizeof(synchro), remote(remote_act));
-        act = &synchro;
-      } else
-        act = remote_act;
+    simgrid::simix::Comm* remote_act = static_cast<simgrid::simix::Comm*>(
+      simcall_comm_test__get__comm(req));
+    simgrid::mc::Remote<simgrid::simix::Comm> temp_synchro;
+    simgrid::simix::Comm* act;
+    if (use_remote_comm) {
+      mc_model_checker->process().read(temp_synchro, remote(
+        static_cast<simgrid::simix::Comm*>(remote_act)));
+      act = static_cast<simgrid::simix::Comm*>(temp_synchro.data());
+    } else
+      act = remote_act;

 
     char* p;
 
     char* p;

-    if (act->comm.src_proc == nullptr || act->comm.dst_proc == nullptr) {
+    if (act->src_proc == nullptr || act->dst_proc == nullptr) {

       type = "Test FALSE";
       p = pointer_to_string(remote_act);
       args = bprintf("comm=%s", p);
       type = "Test FALSE";
       p = pointer_to_string(remote_act);
       args = bprintf("comm=%s", p);


@@ -329,9 +333,9 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid
       p = pointer_to_string(remote_act);
 
       smx_process_t src_proc = mc_model_checker->process().resolveProcess(
       p = pointer_to_string(remote_act);
 
       smx_process_t src_proc = mc_model_checker->process().resolveProcess(

-        simgrid::mc::remote(act->comm.src_proc));
+        simgrid::mc::remote(act->src_proc));

       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(

-        simgrid::mc::remote(act->comm.dst_proc));
+        simgrid::mc::remote(act->dst_proc));

       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
                      src_proc->pid,
                      MC_smx_process_get_name(src_proc),
       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
                      src_proc->pid,
                      MC_smx_process_get_name(src_proc),


@@ -459,10 +463,11 @@ bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
     return true;
   }
 
     return true;
   }
 

-  s_smx_synchro_t synchro;
-  mc_model_checker->process().read_bytes(
-    &synchro, sizeof(synchro), remote(remote_act));
-  return synchro.comm.src_proc && synchro.comm.dst_proc;
+  simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+  mc_model_checker->process().read(temp_comm, remote(
+    static_cast<simgrid::simix::Comm*>(remote_act)));
+  simgrid::simix::Comm* comm = static_cast<simgrid::simix::Comm*>(temp_comm.data());
+  return comm->src_proc && comm->dst_proc;

 }
 
 bool process_is_enabled(smx_process_t process)
 }
 
 bool process_is_enabled(smx_process_t process)


@@ -523,14 +528,15 @@ std::string request_get_dot_output(smx_simcall_t req, int value)
         label = simgrid::xbt::string_printf("[(%lu)] WaitTimeout", issuer->pid);
     } else {
       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
         label = simgrid::xbt::string_printf("[(%lu)] WaitTimeout", issuer->pid);
     } else {
       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);

-      s_smx_synchro_t synchro;
-      mc_model_checker->process().read_bytes(&synchro,
-        sizeof(synchro), remote(remote_act));
+      simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+      mc_model_checker->process().read(temp_comm, remote(
+        static_cast<simgrid::simix::Comm*>(remote_act)));
+      simgrid::simix::Comm* comm = static_cast<simgrid::simix::Comm*>(temp_comm.data());

 
       smx_process_t src_proc = mc_model_checker->process().resolveProcess(
 
       smx_process_t src_proc = mc_model_checker->process().resolveProcess(

-        simgrid::mc::remote(synchro.comm.src_proc));
+        simgrid::mc::remote(comm->src_proc));

       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(

-        simgrid::mc::remote(synchro.comm.dst_proc));
+        simgrid::mc::remote(comm->dst_proc));

       if (issuer->host)
         label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
                     issuer->pid,
       if (issuer->host)
         label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
                     issuer->pid,


@@ -548,10 +554,11 @@ std::string request_get_dot_output(smx_simcall_t req, int value)
 
   case SIMCALL_COMM_TEST: {
     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
 
   case SIMCALL_COMM_TEST: {
     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);

-    s_smx_synchro_t synchro;
-    mc_model_checker->process().read_bytes(&synchro,
-      sizeof(synchro), remote(remote_act));
-    if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == nullptr) {
+    simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+    mc_model_checker->process().read(temp_comm, remote(
+      static_cast<simgrid::simix::Comm*>(remote_act)));
+    simgrid::simix::Comm* comm = static_cast<simgrid::simix::Comm*>(temp_comm.data());
+    if (comm->src_proc == nullptr || comm->dst_proc == nullptr) {

       if (issuer->host)
         label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
                     issuer->pid,
       if (issuer->host)
         label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
                     issuer->pid,

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 50df4a3..771b348 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -49,7 +49,7 @@ namespace mc {
 
 State::State()
 {
 
 State::State()
 {

-  std::memset(&this->internal_comm, 0, sizeof(this->internal_comm));
+  std::memset(this->internal_comm.data(), 0, this->internal_comm.size());

   std::memset(&this->internal_req, 0, sizeof(this->internal_req));
   std::memset(&this->executed_req, 0, sizeof(this->executed_req));
 }
   std::memset(&this->internal_req, 0, sizeof(this->internal_req));
   std::memset(&this->executed_req, 0, sizeof(this->executed_req));
 }


@@ -126,14 +126,15 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       }
 
       case SIMCALL_COMM_WAIT: {
       }
 
       case SIMCALL_COMM_WAIT: {

-        smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
-        s_smx_synchro_t act;
-        mc_model_checker->process().read_bytes(
-          &act, sizeof(act), remote(remote_act));
-        if (act.comm.src_proc && act.comm.dst_proc)
+        simgrid::mc::RemotePtr<simgrid::simix::Comm> remote_act = remote(
+          static_cast<simgrid::simix::Comm*>(simcall_comm_wait__get__comm(&process->simcall)));
+        simgrid::mc::Remote<simgrid::simix::Comm> temp_act;
+        mc_model_checker->process().read(temp_act, remote_act);
+        simgrid::simix::Comm* act = static_cast<simgrid::simix::Comm*>(temp_act.data());
+        if (act->src_proc && act->dst_proc)

           state->transition.argument = 0;
           state->transition.argument = 0;

-        else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
-              && act.comm.detached == 1)
+        else if (act->src_proc == nullptr && act->type == SIMIX_COMM_READY
+              && act->detached == 1)

           state->transition.argument = 0;
         else
           state->transition.argument = -1;
           state->transition.argument = 0;
         else
           state->transition.argument = -1;


@@ -178,7 +179,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
     read_element(mc_model_checker->process(),
       &remote_comm, remote(simcall_comm_waitany__get__comms(req)),
       state->transition.argument, sizeof(remote_comm));
     read_element(mc_model_checker->process(),
       &remote_comm, remote(simcall_comm_waitany__get__comms(req)),
       state->transition.argument, sizeof(remote_comm));

-    mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
+    mc_model_checker->process().read(state->internal_comm, remote(
+      static_cast<simgrid::simix::Comm*>(remote_comm)));

     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
     simcall_comm_wait__set__timeout(&state->internal_req, 0);
     break;
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
     simcall_comm_wait__set__timeout(&state->internal_req, 0);
     break;


@@ -193,7 +195,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       read_element(mc_model_checker->process(),
         &remote_comm, remote(simcall_comm_testany__get__comms(req)),
         state->transition.argument, sizeof(remote_comm));
       read_element(mc_model_checker->process(),
         &remote_comm, remote(simcall_comm_testany__get__comms(req)),
         state->transition.argument, sizeof(remote_comm));

-      mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
+      mc_model_checker->process().read(state->internal_comm, remote(
+        static_cast<simgrid::simix::Comm*>(remote_comm)));

     }
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
     }
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index f5d86b5..1e47840 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -15,6 +15,11 @@
 
 #include <simgrid_config.h>
 #include "src/simix/smx_private.h"
 
 #include <simgrid_config.h>
 #include "src/simix/smx_private.h"

+#include "src/simix/SynchroIo.hpp"
+#include "src/simix/SynchroComm.hpp"
+#include "src/simix/SynchroRaw.hpp"
+#include "src/simix/SynchroSleep.hpp"
+#include "src/simix/SynchroExec.hpp"

 #include "src/mc/mc_snapshot.h"
 #include "src/mc/mc_record.h"
 #include "src/mc/Transition.hpp"
 #include "src/mc/mc_snapshot.h"
 #include "src/mc/mc_record.h"
 #include "src/mc/Transition.hpp"


@@ -22,10 +27,16 @@
 namespace simgrid {
 namespace mc {
 
 namespace simgrid {
 namespace mc {
 

+enum class PatternCommunicationType {
+  none = 0,
+  send = 1,
+  receive = 2,
+};
+

 struct PatternCommunication {
   int num = 0;
   smx_synchro_t comm_addr;
 struct PatternCommunication {
   int num = 0;
   smx_synchro_t comm_addr;

-  e_smx_comm_type_t type = SIMIX_COMM_SEND;
+  PatternCommunicationType type = PatternCommunicationType::send;

   unsigned long src_proc = 0;
   unsigned long dst_proc = 0;
   const char *src_host = nullptr;
   unsigned long src_proc = 0;
   unsigned long dst_proc = 0;
   const char *src_host = nullptr;


@@ -125,7 +136,7 @@ struct XBT_PRIVATE State {
   s_smx_simcall_t internal_req;
 
   /* Can be used as a copy of the remote synchro object */
   s_smx_simcall_t internal_req;
 
   /* Can be used as a copy of the remote synchro object */

-  s_smx_synchro_t internal_comm;
+  simgrid::mc::Remote<simgrid::simix::Comm> internal_comm;

 
   /** Snapshot of system state (if needed) */
   std::shared_ptr<simgrid::mc::Snapshot> system_state;
 
   /** Snapshot of system state (if needed) */
   std::shared_ptr<simgrid::mc::Snapshot> system_state;

diff --git a/src/smpi/smpi_base.cpp b/src/smpi/smpi_base.cpp
index a8e8409..eeaada7 100644 (file)
--- a/src/smpi/smpi_base.cpp
+++ b/src/smpi/smpi_base.cpp
@@ -884,16 +884,10 @@ void smpi_mpi_wait(MPI_Request * request, MPI_Status * status)
     return;
   }
 
     return;
   }
 

-  if ((*request)->action != NULL) { // this is not a detached send
+  if ((*request)->action != NULL)
+    // this is not a detached send

     simcall_comm_wait((*request)->action, -1.0);
 
     simcall_comm_wait((*request)->action, -1.0);
 

-    if((MC_is_active() || MC_record_replay_is_active()) && (*request)->action) {
-      simgrid::simix::Comm *comm = dynamic_cast<simgrid::simix::Comm*>( (*request)->action );
-
-      comm->dst_data = NULL; // dangling pointer: dst_data is freed with a wait, need to set it to NULL for system state comparison
-    }
-  }
-

   finish_wait(request, status);
   if (*request != MPI_REQUEST_NULL && ((*request)->flags & NON_PERSISTENT))
       *request = MPI_REQUEST_NULL;
   finish_wait(request, status);
   if (*request != MPI_REQUEST_NULL && ((*request)->flags & NON_PERSISTENT))
       *request = MPI_REQUEST_NULL;