[mc] Move cross process reading support for SBT structure in a separate file

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 836b430..9efb8bf 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -649,6 +649,8 @@ set(MC_SRC
   src/mc/mc_server.h
   src/mc/mc_smx.h
   src/mc/mc_smx.cpp
   src/mc/mc_server.h
   src/mc/mc_smx.h
   src/mc/mc_smx.cpp

+  src/mc/mc_xbt.hpp
+  src/mc/mc_xbt.cpp

   )
 
 set(MC_SIMGRID_MC_SRC
   )
 
 set(MC_SIMGRID_MC_SRC

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 008f129..bc0e314 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -22,7 +22,9 @@
 #include "mc_server.h"
 #endif
 
 #include "mc_server.h"
 #endif
 

+#ifdef HAVE_MC

 using simgrid::mc::remote;
 using simgrid::mc::remote;

+#endif

 
 extern "C" {
 
 
 extern "C" {
 

diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp
index a5b6e49..f63a529 100644 (file)
--- a/src/mc/mc_comm_pattern.cpp
+++ b/src/mc/mc_comm_pattern.cpp
@@ -11,6 +11,9 @@
 
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"
 
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"

+#include "mc_xbt.hpp"
+
+using simgrid::mc::remote;

 
 extern "C" {
 
 
 extern "C" {
 


@@ -125,8 +128,8 @@ void MC_handle_comm_pattern(
         comm_addr = simcall_comm_wait__get__comm(req);
       else
         // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
         comm_addr = simcall_comm_wait__get__comm(req);
       else
         // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):

-        MC_process_read_dynar_element(&mc_model_checker->process(), &comm_addr,
-          simcall_comm_waitany__get__comms(req), value, sizeof(comm_addr));
+        simgrid::mc::read_element(mc_model_checker->process(), &comm_addr,
+          remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));

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

diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp
index 476a1a9..66bb067 100644 (file)
--- a/src/mc/mc_process.cpp
+++ b/src/mc/mc_process.cpp
@@ -593,30 +593,3 @@ void Process::clear_bytes(remote_ptr<void> address, size_t len)
 
 }
 }
 
 }
 }

-
-extern "C" {
-
-const void* MC_process_read_dynar_element(mc_process_t process,
-  void* local, const void* remote_dynar, size_t i, size_t len)
-{
-  s_xbt_dynar_t d;
-  process->read_bytes(&d, sizeof(d), remote(remote_dynar));
-  if (i >= d.used)
-    xbt_die("Out of bound index %zi/%lu", i, d.used);
-  if (len != d.elmsize)
-    xbt_die("Bad size in MC_process_read_dynar_element");
-  process->read_bytes(local, len, remote(xbt_dynar_get_ptr(&d, i)));
-  return local;
-}
-
-unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar)
-{
-  if (!remote_dynar)
-    return 0;
-  unsigned long res;
-  process->read_bytes(&res, sizeof(res),
-    remote(&((xbt_dynar_t)remote_dynar)->used));
-  return res;
-}
-
-}

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index c21e951..703dd55 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -176,11 +176,6 @@ int open_vm(pid_t pid, int flags);
 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 

-XBT_INTERNAL const void* MC_process_read_dynar_element(mc_process_t process,
-  void* local, const void* remote_dynar, size_t i, size_t len);
-XBT_INTERNAL unsigned long MC_process_read_dynar_length(mc_process_t process,
-  const void* remote_dynar);
-

 XBT_INTERNAL void MC_invalidate_cache(void);
 
 SG_END_DECL()
 XBT_INTERNAL void MC_invalidate_cache(void);
 
 SG_END_DECL()

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index e28f119..27d74e3 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -10,6 +10,7 @@
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_smx.h"
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_smx.h"

+#include "mc_xbt.hpp"

 
 using simgrid::mc::remote;
 
 
 using simgrid::mc::remote;
 


@@ -374,8 +375,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
     if (!xbt_dynar_is_empty(&comms)) {
       smx_synchro_t remote_sync;
       &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
     if (!xbt_dynar_is_empty(&comms)) {
       smx_synchro_t remote_sync;

-      MC_process_read_dynar_element(&mc_model_checker->process(),
-        &remote_sync, simcall_comm_waitany__get__comms(req), value,
+      read_element(mc_model_checker->process(),
+        &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,

         sizeof(remote_sync));
       char* p = pointer_to_string(remote_sync);
       args = bprintf("comm=%s (%d of %lu)",
         sizeof(remote_sync));
       char* p = pointer_to_string(remote_sync);
       args = bprintf("comm=%s (%d of %lu)",


@@ -395,8 +396,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       type = "TestAny";
       args =
           bprintf("(%d of %lu)", value + 1,
       type = "TestAny";
       args =
           bprintf("(%d of %lu)", value + 1,

-                  MC_process_read_dynar_length(&mc_model_checker->process(),
-                    simcall_comm_testany__get__comms(req)));
+                  read_length(mc_model_checker->process(),
+                    remote(simcall_comm_testany__get__comms(req))));

     }
     break;
 
     }
     break;
 


@@ -502,15 +503,17 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
     break;
 
   case SIMCALL_COMM_WAITANY: {
     break;
 
   case SIMCALL_COMM_WAITANY: {

-    MC_process_read_dynar_element(
-      &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
+    read_element(
+      mc_model_checker->process(), &remote_act,
+      remote(simcall_comm_waitany__get__comms(req)),

       idx, sizeof(remote_act));
     }
     break;
 
   case SIMCALL_COMM_TESTANY: {
       idx, sizeof(remote_act));
     }
     break;
 
   case SIMCALL_COMM_TESTANY: {

-    MC_process_read_dynar_element(
-      &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
+    read_element(
+      mc_model_checker->process(), &remote_act,
+      remote(simcall_comm_testany__get__comms(req)),

       idx, sizeof(remote_act));
     }
     break;
       idx, sizeof(remote_act));
     }
     break;


@@ -610,8 +613,8 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
   }
 
   case SIMCALL_COMM_WAITANY: {
   }
 
   case SIMCALL_COMM_WAITANY: {

-    unsigned long comms_size = MC_process_read_dynar_length(
-      &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
+    unsigned long comms_size = read_length(
+      mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));

     if (issuer->smx_host)
       label =
           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
     if (issuer->smx_host)
       label =
           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index f3b35cd..208187e 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -13,6 +13,7 @@
 #include "mc_private.h"
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"
 #include "mc_private.h"
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"

+#include "mc_xbt.hpp"

 
 using simgrid::mc::remote;
 
 
 using simgrid::mc::remote;
 


@@ -107,8 +108,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
   case SIMCALL_COMM_WAITANY:
     state->internal_req.call = SIMCALL_COMM_WAIT;
     state->internal_req.issuer = req->issuer;
   case SIMCALL_COMM_WAITANY:
     state->internal_req.call = SIMCALL_COMM_WAIT;
     state->internal_req.issuer = req->issuer;

-    MC_process_read_dynar_element(&mc_model_checker->process(),
-      &state->internal_comm, simcall_comm_waitany__get__comms(req),
+    read_element(mc_model_checker->process(),
+      &state->internal_comm, remote(simcall_comm_waitany__get__comms(req)),

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


@@ -119,8 +120,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
     state->internal_req.issuer = req->issuer;
 
     if (value > 0)
     state->internal_req.issuer = req->issuer;
 
     if (value > 0)

-        MC_process_read_dynar_element(&mc_model_checker->process(),
-          &state->internal_comm, simcall_comm_testany__get__comms(req),
+        read_element(mc_model_checker->process(),
+          &state->internal_comm, remote(simcall_comm_testany__get__comms(req)),

           value, sizeof(state->internal_comm));
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
           value, sizeof(state->internal_comm));
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);


@@ -192,8 +193,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_COMM_WAITANY:
         *value = -1;
         while (procstate->interleave_count <
       case SIMCALL_COMM_WAITANY:
         *value = -1;
         while (procstate->interleave_count <

-              MC_process_read_dynar_length(&mc_model_checker->process(),
-                simcall_comm_waitany__get__comms(&process->simcall))) {
+              read_length(mc_model_checker->process(),
+                remote(simcall_comm_waitany__get__comms(&process->simcall)))) {

           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;


@@ -202,8 +203,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         }
 
         if (procstate->interleave_count >=
         }
 
         if (procstate->interleave_count >=

-            MC_process_read_dynar_length(&mc_model_checker->process(),
-              simcall_comm_waitany__get__comms(&process->simcall)))
+            simgrid::mc::read_length(mc_model_checker->process(),
+              simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))

           procstate->state = MC_DONE;
 
         if (*value != -1)
           procstate->state = MC_DONE;
 
         if (*value != -1)


@@ -215,8 +216,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         unsigned start_count = procstate->interleave_count;
         *value = -1;
         while (procstate->interleave_count <
         unsigned start_count = procstate->interleave_count;
         *value = -1;
         while (procstate->interleave_count <

-                MC_process_read_dynar_length(&mc_model_checker->process(),
-                  simcall_comm_testany__get__comms(&process->simcall))) {
+                read_length(mc_model_checker->process(),
+                  remote(simcall_comm_testany__get__comms(&process->simcall)))) {

           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;


@@ -225,8 +226,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         }
 
         if (procstate->interleave_count >=
         }
 
         if (procstate->interleave_count >=

-            MC_process_read_dynar_length(&mc_model_checker->process(),
-              simcall_comm_testany__get__comms(&process->simcall)))
+            read_length(mc_model_checker->process(),
+              remote(simcall_comm_testany__get__comms(&process->simcall))))

           procstate->state = MC_DONE;
 
         if (*value != -1 || start_count == 0)
           procstate->state = MC_DONE;
 
         if (*value != -1 || start_count == 0)

diff --git a/src/mc/mc_xbt.cpp b/src/mc/mc_xbt.cpp
new file mode 100644 (file)
index 0000000..7742139
--- /dev/null
+++ b/src/mc/mc_xbt.cpp
@@ -0,0 +1,36 @@
+/* Copyright (c) 2014-2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "mc/AddressSpace.hpp"
+#include "mc_xbt.hpp"
+
+namespace simgrid {
+namespace mc {
+
+void read_element(AddressSpace const& as,
+  void* local, remote_ptr<s_xbt_dynar_t> addr, size_t i, size_t len)
+{
+  s_xbt_dynar_t d;
+  as.read_bytes(&d, sizeof(d), addr);
+  if (i >= d.used)
+    xbt_die("Out of bound index %zi/%lu", i, d.used);
+  if (len != d.elmsize)
+    xbt_die("Bad size in simgrid::mc::read_element");
+  as.read_bytes(local, len, remote(xbt_dynar_get_ptr(&d, i)));
+}
+
+std::size_t read_length(AddressSpace const& as, remote_ptr<s_xbt_dynar_t> addr)
+{
+  if (!addr)
+    return 0;
+  unsigned long res;
+  as.read_bytes(&res, sizeof(res),
+    remote(&((xbt_dynar_t)addr.address())->used));
+  return res;
+}
+
+}
+}

diff --git a/src/mc/mc_xbt.hpp b/src/mc/mc_xbt.hpp
new file mode 100644 (file)
index 0000000..5303195
--- /dev/null
+++ b/src/mc/mc_xbt.hpp
@@ -0,0 +1,22 @@
+/* Copyright (c) 2014-2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_XBT_HPP
+#define SIMGRID_MC_XBT_HPP
+
+#include "mc/AddressSpace.hpp"
+
+namespace simgrid {
+namespace mc {
+
+void read_element(AddressSpace const& as,
+  void* local, remote_ptr<s_xbt_dynar_t> addr, size_t i, size_t len);
+std::size_t read_length(AddressSpace const& as, remote_ptr<s_xbt_dynar_t> addr);
+
+}
+}
+
+#endif