[mc] Add support of privatized global variables in per-page snapshot

Not very useful because state comparison does not work with SMPI
privatisation yet.

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index c07f6661df0132f9cc0fd2e887b855fbf4b918d6..abb2dee35a942df2c95ffa9eb44efdab2a333f51 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -166,9 +166,10 @@ static void MC_get_memory_regions(mc_snapshot_t snapshot)
     snapshot->privatization_regions =
         xbt_new(mc_mem_region_t, SIMIX_process_count());
     for (i = 0; i < SIMIX_process_count(); i++) {
     snapshot->privatization_regions =
         xbt_new(mc_mem_region_t, SIMIX_process_count());
     for (i = 0; i < SIMIX_process_count(); i++) {

-      // TODO, add support for sparse snapshot
+      mc_mem_region_t ref_reg =
+        mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->privatization_regions[i] : NULL;

       snapshot->privatization_regions[i] =
       snapshot->privatization_regions[i] =

-        MC_region_new(-1, mappings[i], size_data_exe, NULL);
+        MC_region_new(-1, mappings[i], size_data_exe, ref_reg);

     }
     snapshot->privatization_index = loaded_page;
   }
     }
     snapshot->privatization_index = loaded_page;
   }

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 6eaa3bf79fca7357d0136ffd1c22657f20f42a72..ada39e645a5ceaac2ae2ea43b1e35812a702ab38 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -246,6 +246,8 @@ static int compare_global_variables(int region_type, mc_mem_region_t r1,
                                     mc_mem_region_t r2, mc_snapshot_t snapshot1,
                                     mc_snapshot_t snapshot2)
 {
                                     mc_mem_region_t r2, mc_snapshot_t snapshot1,
                                     mc_snapshot_t snapshot2)
 {

+  xbt_assert(r1 && r2,
+    "Missing region. Did you enable SMPI privatisation? It is not compatible with state comparison.");

   struct mc_compare_state state;
 
   xbt_dynar_t variables;
   struct mc_compare_state state;
 
   xbt_dynar_t variables;