[mc] Read smpi_process_count() from remote process

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index d368810..3d92e45 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -204,7 +204,7 @@ static mc_mem_region_t MC_region_new_privatized(
     mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size,
     mc_mem_region_t ref_reg)
 {
-  size_t process_count = smpi_process_count();
+  size_t process_count = MC_smpi_process_count();
   mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
   region->region_type = region_type;
   region->storage_type = MC_REGION_STORAGE_TYPE_PRIVATIZED;
@@ -242,7 +242,7 @@ static void MC_snapshot_add_region(int index, mc_snapshot_t snapshot, mc_region_
 
   mc_mem_region_t region;
   const bool privatization_aware = MC_object_info_is_privatized(object_info);
-  if (privatization_aware && smpi_process_count())
+  if (privatization_aware && MC_smpi_process_count())
     region = MC_region_new_privatized(type, start_addr, permanent_addr, size, ref_reg);
   else
     region = MC_region_new(type, start_addr, permanent_addr, size, ref_reg);
@@ -277,7 +277,7 @@ static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot)
     MC_process_get_malloc_info(process));
 
 #ifdef HAVE_SMPI
-  if (smpi_privatize_global_variables && smpi_process_count()) {
+  if (smpi_privatize_global_variables && MC_smpi_process_count()) {
     // FIXME, cross-process
     snapshot->privatization_index = smpi_loaded_page;
   } else

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 696d688..3420b02 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -13,6 +13,7 @@
 #include "mc_safety.h"
 #include "mc_liveness.h"
 #include "mc_private.h"
+#include "mc_smx.h"
 
 #ifdef HAVE_SMPI
 #include "smpi/private.h"
@@ -269,7 +270,7 @@ static int compare_global_variables(mc_object_info_t object_info,
       return 1;
     }
 
-    size_t process_count = smpi_process_count();
+    size_t process_count = MC_smpi_process_count();
     xbt_assert(process_count == r1->privatized.regions_count
       && process_count == r2->privatized.regions_count);
 

diff --git a/src/mc/mc_smx.c b/src/mc/mc_smx.c
index 2f8b8fc..bf647c7 100644 (file)
--- a/src/mc/mc_smx.c
+++ b/src/mc/mc_smx.c
@@ -250,3 +250,15 @@ const char* MC_smx_process_get_name(smx_process_t p)
   }
   return info->name;
 }
+
+int MC_smpi_process_count(void)
+{
+  if (MC_process_is_self(&mc_model_checker->process))
+    return smpi_process_count();
+  else {
+    int res;
+    MC_process_read_variable(&mc_model_checker->process, "process_count",
+      &res, sizeof(res));
+    return res;
+  }
+}

diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h
index fa7a565..5cd2e1d 100644 (file)
--- a/src/mc/mc_smx.h
+++ b/src/mc/mc_smx.h
@@ -12,6 +12,8 @@
 #include <xbt/log.h>
 #include <simgrid/simix.h>
 
+#include "smpi/private.h"
+
 #include "mc_process.h"
 #include "mc_protocol.h"
 
@@ -83,6 +85,7 @@ const char* MC_smx_process_get_host_name(smx_process_t p);
 /** Execute a given simcall */
 void MC_simcall_handle(smx_simcall_t req, int value);
 
+int MC_smpi_process_count(void);
 
 
 /* ***** Resolve (local/MCer structure from remote/MCed addresses) ***** */