[mc] Cleanup MC init code (split MCer and MCed init)

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 9144932..d63ceef 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -67,7 +67,7 @@ int MC_request_is_enabled(smx_simcall_t req)
 
 #ifdef HAVE_MC
     // Fetch from MCed memory:
-    if (!MC_process_is_self(&mc_model_checker->process())) {
+    if (mc_mode == MC_MODE_SERVER) {
       MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
         &temp_synchro, act, sizeof(temp_synchro),
         MC_PROCESS_INDEX_ANY);
@@ -111,7 +111,7 @@ int MC_request_is_enabled(smx_simcall_t req)
 
 #ifdef HAVE_MC
       // Fetch from MCed memory:
-      if (!MC_process_is_self(&mc_model_checker->process())) {
+      if (mc_mode == MC_MODE_SERVER) {
         MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
           &temp_synchro, act, sizeof(temp_synchro),
           MC_PROCESS_INDEX_ANY);
@@ -129,7 +129,7 @@ int MC_request_is_enabled(smx_simcall_t req)
     smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
 #ifdef HAVE_MC
     s_smx_mutex_t temp_mutex;
-    if (!MC_process_is_self(&mc_model_checker->process())) {
+    if (mc_mode == MC_MODE_SERVER) {
       MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
         &temp_mutex, mutex, sizeof(temp_mutex),
         MC_PROCESS_INDEX_ANY);
@@ -210,7 +210,7 @@ void MC_simcall_handle(smx_simcall_t req, int value)
 #ifndef HAVE_MC
   SIMIX_simcall_handle(req, value);
 #else
-  if (MC_process_is_self(&mc_model_checker->process())) {
+  if (mc_mode == MC_MODE_CLIENT) {
     SIMIX_simcall_handle(req, value);
     return;
   }

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index ae886a4..3565626 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -110,28 +110,24 @@ static void MC_init_dot_output()
 #ifdef HAVE_MC
 void MC_init()
 {
-  MC_init_pid(getpid(), -1);
-}
+  mc_time = xbt_new0(double, simix_process_maxpid);
 
-void MC_init_pid(pid_t pid, int socket)
-{
-  /* Initialize the data structures that must be persistent across every
-     iteration of the model-checker (in RAW memory) */
+  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
+    /* Those requests are handled on the client side and propagated by message
+     * to the server: */
 
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-  mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
+    MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
-  // It's not useful anymore:
-  if (0 && mc_mode == MC_MODE_SERVER) {
-    unsigned long maxpid;
-    MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid",
-      &maxpid, sizeof(maxpid));
-    simix_process_maxpid = maxpid;
+    smx_process_t process;
+    xbt_swag_foreach(process, simix_global->process_list) {
+      MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+    }
   }
+}
 
-  mmalloc_set_current_heap(std_heap);
-  mc_time = xbt_new0(double, MC_smx_get_maxpid());
-  mmalloc_set_current_heap(mc_heap);
+void MC_init_model_checker(pid_t pid, int socket)
+{
+  mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
 
   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 
@@ -145,62 +141,29 @@ void MC_init_pid(pid_t pid, int socket)
   /* Init parmap */
   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 
-  mmalloc_set_current_heap(std_heap);
-
-  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
-    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
-    MC_ignore_local_variable("e", "*");
-    MC_ignore_local_variable("__ex_cleanup", "*");
-    MC_ignore_local_variable("__ex_mctx_en", "*");
-    MC_ignore_local_variable("__ex_mctx_me", "*");
-    MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
-    MC_ignore_local_variable("_log_ev", "*");
-    MC_ignore_local_variable("_throw_ctx", "*");
-    MC_ignore_local_variable("ctx", "*");
-
-    MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
-    MC_ignore_local_variable("next_cont"
-      "ext", "smx_ctx_sysv_suspend_serial");
-    MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
-
-    /* Ignore local variable about time used for tracing */
-    MC_ignore_local_variable("start_time", "*");
-
-    /* Main MC state: */
-    MCer_ignore_global_variable("mc_model_checker");
-    MCer_ignore_global_variable("initial_communications_pattern");
-    MCer_ignore_global_variable("incomplete_communications_pattern");
-    MCer_ignore_global_variable("nb_comm_pattern");
-
-    /* MC __thread variables: */
-    MCer_ignore_global_variable("mc_diff_info");
-    MCer_ignore_global_variable("mc_comp_times");
-    MCer_ignore_global_variable("mc_snapshot_comparison_time");
-
-    /* This MC state is used in MC replay as well: */
-    MCer_ignore_global_variable("mc_time");
-
-    /* Static variable used for tracing */
-    MCer_ignore_global_variable("counter");
-
-    /* SIMIX */
-    MCer_ignore_global_variable("smx_total_comms");
-
-    if (mc_mode == MC_MODE_CLIENT) {
-      /* Those requests are handled on the client side and propagated by message
-       * to the server: */
-
-      MC_ignore_heap(mc_time, MC_smx_get_maxpid() * sizeof(double));
-
-      smx_process_t process;
-      xbt_swag_foreach(process, simix_global->process_list) {
-        MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
-      }
-    }
-
-  }
-
-  mmalloc_set_current_heap(heap);
+  /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
+  MC_ignore_local_variable("e", "*");
+  MC_ignore_local_variable("__ex_cleanup", "*");
+  MC_ignore_local_variable("__ex_mctx_en", "*");
+  MC_ignore_local_variable("__ex_mctx_me", "*");
+  MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
+  MC_ignore_local_variable("_log_ev", "*");
+  MC_ignore_local_variable("_throw_ctx", "*");
+  MC_ignore_local_variable("ctx", "*");
+
+  MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
+  MC_ignore_local_variable("next_cont"
+    "ext", "smx_ctx_sysv_suspend_serial");
+  MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
+
+  /* Ignore local variable about time used for tracing */
+  MC_ignore_local_variable("start_time", "*");
+
+  /* Static variable used for tracing */
+  MCer_ignore_global_variable("counter");
+
+  /* SIMIX */
+  MCer_ignore_global_variable("smx_total_comms");
 }
 #endif
 
@@ -250,12 +213,12 @@ int MC_deadlock_check()
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {
     deadlock = TRUE;
-    MC_EACH_SIMIX_PROCESS(process,
+    xbt_swag_foreach(process, simix_global->process_list) {
       if (MC_process_is_enabled(process)) {
         deadlock = FALSE;
         break;
       }
-    );
+    }
   }
   return deadlock;
 }

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 85e0f21..c9ea7c2 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -48,7 +48,7 @@ typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function
  * @param pid     PID of the target process
  * @param socket  FD for the communication socket **in server mode** (or -1 otherwise)
  */
-void MC_init_pid(pid_t pid, int socket);
+void MC_init_model_checker(pid_t pid, int socket);
 
 extern FILE *dot_output;
 extern const char* colors[13];

diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp
index 5dbbddd..40e9d03 100644 (file)
--- a/src/mc/mc_process.cpp
+++ b/src/mc/mc_process.cpp
@@ -154,7 +154,8 @@ void MC_process_clear(mc_process_t process)
 
 void MC_process_refresh_heap(mc_process_t process)
 {
-  assert(!MC_process_is_self(process));
+  xbt_assert(mc_mode == MC_MODE_SERVER);
+  xbt_assert(!MC_process_is_self(process));
   // Read/dereference/refresh the std_heap pointer:
   if (!process->heap) {
     process->heap = (struct mdesc*) malloc(sizeof(struct mdesc));
@@ -163,11 +164,13 @@ void MC_process_refresh_heap(mc_process_t process)
     process->heap, process->heap_address, sizeof(struct mdesc),
     MC_PROCESS_INDEX_DISABLED
     );
+  process->cache_flags |= MC_PROCESS_CACHE_FLAG_HEAP;
 }
 
 void MC_process_refresh_malloc_info(mc_process_t process)
 {
-  assert(!MC_process_is_self(process));
+  xbt_assert(mc_mode == MC_MODE_SERVER);
+  xbt_assert(!MC_process_is_self(process));
   if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP))
     MC_process_refresh_heap(process);
   // Refresh process->heapinfo:
@@ -178,6 +181,7 @@ void MC_process_refresh_malloc_info(mc_process_t process)
     process->heap_info,
     process->heap->heapinfo, malloc_info_bytesize,
     MC_PROCESS_INDEX_DISABLED);
+  process->cache_flags |= MC_PROCESS_CACHE_FLAG_MALLOC_INFO;
 }
 
 #define SO_RE "\\.so[\\.0-9]*$"

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index b203933..ab32689 100644 (file)
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -86,6 +86,8 @@ static void MC_process_refresh_simix_process_list(
 
 void MC_process_smx_refresh(mc_process_t process)
 {
+  xbt_assert(mc_mode == MC_MODE_SERVER);
+  xbt_assert(!MC_process_is_self(process));
   if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
     return;
 
@@ -119,7 +121,7 @@ void MC_process_smx_refresh(mc_process_t process)
  */
 smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
 {
-  if (MC_process_is_self(&mc_model_checker->process()))
+  if (mc_mode == MC_MODE_CLIENT)
     return req->issuer;
 
   MC_process_smx_refresh(&mc_model_checker->process());
@@ -145,7 +147,7 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address)
 {
   if (!process_remote_address)
     return NULL;
-  if (MC_process_is_self(&mc_model_checker->process()))
+  if (mc_mode == MC_MODE_CLIENT)
     return process_remote_address;
 
   mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address);
@@ -157,7 +159,7 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address)
 
 mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address)
 {
-  if (MC_process_is_self(&mc_model_checker->process()))
+  if (mc_mode == MC_MODE_CLIENT)
     xbt_die("No process_info for local process is not enabled.");
 
   unsigned index;
@@ -173,7 +175,7 @@ mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_a
 
 const char* MC_smx_process_get_host_name(smx_process_t p)
 {
-  if (MC_process_is_self(&mc_model_checker->process()))
+  if (mc_mode == MC_MODE_CLIENT)
     return SIMIX_host_get_name(p->smx_host);
 
   mc_process_t process = &mc_model_checker->process();
@@ -198,7 +200,7 @@ const char* MC_smx_process_get_host_name(smx_process_t p)
 const char* MC_smx_process_get_name(smx_process_t p)
 {
   mc_process_t process = &mc_model_checker->process();
-  if (MC_process_is_self(process))
+  if (mc_mode == MC_MODE_CLIENT)
     return p->name;
   if (!p->name)
     return NULL;
@@ -212,7 +214,7 @@ const char* MC_smx_process_get_name(smx_process_t p)
 
 int MC_smpi_process_count(void)
 {
-  if (MC_process_is_self(&mc_model_checker->process()))
+  if (mc_mode == MC_MODE_CLIENT)
     return smpi_process_count();
   else {
     int res;

diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h
index 123052c..32b78cc 100644 (file)
--- a/src/mc/mc_smx.h
+++ b/src/mc/mc_smx.h
@@ -68,7 +68,7 @@ const char* MC_smx_process_get_name(smx_process_t p);
 const char* MC_smx_process_get_host_name(smx_process_t p);
 
 #define MC_EACH_SIMIX_PROCESS(process, code) \
-  if (MC_process_is_self(&mc_model_checker->process())) { \
+  if (mc_mode == MC_MODE_CLIENT) { \
     xbt_swag_foreach(process, simix_global->process_list) { \
       code; \
     } \

diff --git a/src/mc/mcer_ignore.cpp b/src/mc/mcer_ignore.cpp
index 3e8b3bf..54d2da2 100644 (file)
--- a/src/mc/mcer_ignore.cpp
+++ b/src/mc/mcer_ignore.cpp
@@ -112,7 +112,6 @@ void MC_heap_region_ignore_remove(void *address, size_t size)
 void MCer_ignore_global_variable(const char *name)
 {
   mc_process_t process = &mc_model_checker->process();
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
   xbt_assert(process->object_infos, "MC subsystem not initialized");
 
   size_t n = process->object_infos_size;
@@ -138,7 +137,6 @@ void MCer_ignore_global_variable(const char *name)
       }
     }
   }
-  mmalloc_set_current_heap(heap);
 }
 
 // ***** Ignore local variables
@@ -156,15 +154,12 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name)
   mc_process_t process = &mc_model_checker->process();
   if (strcmp(frame_name, "*") == 0)
     frame_name = NULL;
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   size_t n = process->object_infos_size;
   size_t i;
   for (i=0; i!=n; ++i) {
     MC_ignore_local_variable_in_object(var_name, frame_name, process->object_infos[i]);
   }
-
-  mmalloc_set_current_heap(heap);
 }
 
 static void MC_ignore_local_variable_in_object(const char *var_name,

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 29d5fe2..f06240e 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -82,7 +82,7 @@ static int do_parent(int socket, pid_t child)
     mc_mode = MC_MODE_SERVER;
     mc_server = new s_mc_server(child, socket);
     mc_server->start();
-    MC_init_pid(child, socket);
+    MC_init_model_checker(child, socket);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
       MC_modelcheck_comm_determinism();
     else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')

diff --git a/src/simix/popping_generated.c b/src/simix/popping_generated.c
index 9f8e55c..9b302ca 100644 (file)
--- a/src/simix/popping_generated.c
+++ b/src/simix/popping_generated.c
@@ -160,11 +160,6 @@ const char* simcall_names[] = {
  */
 void SIMIX_simcall_handle(smx_simcall_t simcall, int value) {
   XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));
-  #ifdef HAVE_MC
-  if (mc_model_checker) {
-    MC_invalidate_cache();
-  }
-  #endif
   SIMCALL_SET_MC_VALUE(simcall, value);
   if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP)
     return;

diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py
index 997a60b..15d7c99 100755 (executable)
--- a/src/simix/simcalls.py
+++ b/src/simix/simcalls.py
@@ -302,11 +302,6 @@ if __name__=='__main__':
   fd.write(' */\n');
   fd.write('void SIMIX_simcall_handle(smx_simcall_t simcall, int value) {\n');
   fd.write('  XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));\n');
-  fd.write('  #ifdef HAVE_MC\n');
-  fd.write('  if (mc_model_checker) {\n');
-  fd.write('    MC_invalidate_cache();\n');
-  fd.write('  }\n');
-  fd.write('  #endif\n');
   fd.write('  SIMCALL_SET_MC_VALUE(simcall, value);\n');
   fd.write('  if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP)\n');
   fd.write('    return;\n');