From 26af220e017a088b56105b2f21fadecf7d6e2a88 Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Fri, 17 Apr 2015 14:02:45 +0200
Subject: [PATCH] [mc] C++ class ModelChecker

---
 buildtools/Cmake/DefinePackages.cmake         |  4 +-
 src/mc/ModelChecker.cpp                       | 49 +++++++++++++++++
 .../{mc_model_checker.h => ModelChecker.hpp}  | 42 +++++++++------
 src/mc/mc_base.cpp                            | 26 ++++-----
 src/mc/mc_checkpoint.cpp                      | 49 ++++++-----------
 src/mc/mc_client.cpp                          |  1 -
 src/mc/mc_client_api.cpp                      |  4 +-
 src/mc/mc_comm_determinism.cpp                | 24 ++++-----
 src/mc/mc_comm_pattern.cpp                    |  2 +-
 src/mc/mc_compare.cpp                         |  4 +-
 src/mc/mc_diff.cpp                            | 10 ++--
 src/mc/mc_forward.h                           | 23 ++++++--
 src/mc/mc_global.cpp                          | 14 +++--
 src/mc/mc_hash.cpp                            |  2 +-
 src/mc/mc_ignore.cpp                          |  4 +-
 src/mc/mc_model_checker.cpp                   | 41 --------------
 src/mc/mc_page_snapshot.cpp                   |  8 +--
 src/mc/mc_private.h                           |  2 +
 src/mc/mc_process.h                           |  2 +
 src/mc/mc_record.cpp                          |  1 -
 src/mc/mc_request.cpp                         | 34 ++++++------
 src/mc/mc_server.cpp                          | 28 +++++-----
 src/mc/mc_smx.cpp                             | 53 +++++++++----------
 src/mc/mc_smx.h                               | 10 ++--
 src/mc/mc_snapshot.cpp                        |  6 +--
 src/mc/mc_snapshot.h                          | 15 +++---
 src/mc/mc_state.cpp                           | 18 +++----
 src/mc/mc_visited.cpp                         | 20 +++----
 src/mc/simgrid_mc.cpp                         |  1 -
 src/simix/popping_generated.c                 |  3 +-
 src/simix/simcalls.py                         |  3 +-
 src/simix/smx_global.c                        |  1 -
 teshsuite/mc/dwarf/CMakeLists.txt             |  4 +-
 teshsuite/mc/dwarf/{dwarf.c => dwarf.cpp}     | 11 ++--
 34 files changed, 266 insertions(+), 253 deletions(-)
 create mode 100644 src/mc/ModelChecker.cpp
 rename src/mc/{mc_model_checker.h => ModelChecker.hpp} (52%)
 delete mode 100644 src/mc/mc_model_checker.cpp
 rename teshsuite/mc/dwarf/{dwarf.c => dwarf.cpp} (94%)

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 10ae1ba3c2..83cce2052e 100644
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -598,8 +598,8 @@ set(MC_SRC
   src/mc/mc_unw.cpp
   src/mc/mc_unw_vmread.cpp
   src/mc/mc_mmalloc.h
-  src/mc/mc_model_checker.h
-  src/mc/mc_model_checker.cpp
+  src/mc/ModelChecker.hpp
+  src/mc/ModelChecker.cpp
   src/mc/mc_object_info.h
   src/mc/mc_object_info.cpp
   src/mc/mc_checkpoint.cpp
diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
new file mode 100644
index 0000000000..061ca74d19
--- /dev/null
+++ b/src/mc/ModelChecker.cpp
@@ -0,0 +1,49 @@
+/* Copyright (c) 2008-2014. 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 <cassert>
+
+#include "ModelChecker.hpp"
+#include "mc_page_store.h"
+
+::simgrid::mc::ModelChecker* mc_model_checker = NULL;
+
+namespace simgrid {
+namespace mc {
+
+ModelChecker::ModelChecker(pid_t pid, int socket)
+{
+  this->page_store_ = mc_pages_store_new();
+  this->fd_clear_refs_ = -1;
+  this->hostnames_ = xbt_dict_new();
+  MC_process_init(&this->process(), pid, socket);
+}
+
+ModelChecker::~ModelChecker()
+{
+  mc_pages_store_delete(this->page_store_);
+  if(this->record_)
+    xbt_dynar_free(&this->record_);
+  MC_process_clear(&this->process_);
+  xbt_dict_free(&this->hostnames_);
+}
+
+const char* ModelChecker::get_host_name(const char* hostname)
+{
+  // Lookup the host name in the dictionary (or create it):
+  xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
+  if (!elt) {
+    xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+    xbt_dict_set(this->hostnames_, hostname, NULL, NULL);
+    elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
+    assert(elt);
+    mmalloc_set_current_heap(heap);
+  }
+  return elt->key;
+}
+
+}
+}
diff --git a/src/mc/mc_model_checker.h b/src/mc/ModelChecker.hpp
similarity index 52%
rename from src/mc/mc_model_checker.h
rename to src/mc/ModelChecker.hpp
index 4c42b816d9..5fb8204411 100644
--- a/src/mc/mc_model_checker.h
+++ b/src/mc/ModelChecker.hpp
@@ -17,30 +17,42 @@
 #include "mc_page_store.h"
 #include "mc_protocol.h"
 
-SG_BEGIN_DECL()
+namespace simgrid {
+namespace mc {
 
-/** @brief State of the model-checker (global variables for the model checker)
+/** State of the model-checker (global variables for the model checker)
  *
  *  Each part of the state of the model chercker represented as a global
  *  variable prevents some sharing between snapshots and must be ignored.
  *  By moving as much state as possible in this structure allocated
- *  on the model-chercker heap, we avoid those issues.
+ *  on the model-checker heap, we avoid those issues.
  */
-struct s_mc_model_checker {
+class ModelChecker {
   // This is the parent snapshot of the current state:
-  mc_snapshot_t parent_snapshot;
-  mc_pages_store_t pages;
-  int fd_clear_refs;
-  xbt_dynar_t record;
-  s_mc_process_t process;
+  mc_pages_store_t page_store_;
+  int fd_clear_refs_;
+  xbt_dynar_t record_;
+  s_mc_process_t process_;
   /** String pool for host names */
-  xbt_dict_t /* <hostname, NULL> */ hosts;
+  // TODO, use std::unordered_set with heterogeneous comparison lookup (C++14)
+  xbt_dict_t /* <hostname, NULL> */ hostnames_;
+public:
+  ModelChecker(ModelChecker const&) = delete;
+  ModelChecker& operator=(ModelChecker const&) = delete;
+  ModelChecker(pid_t pid, int socket);
+  ~ModelChecker();
+  s_mc_process_t& process()
+  {
+    return process_;
+  }
+  s_mc_pages_store_t& page_store()
+  {
+    return *page_store_;
+  }
+  const char* get_host_name(const char* name);
 };
 
-mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
-void MC_model_checker_delete(mc_model_checker_t mc);
-unsigned long MC_smx_get_maxpid(void);
-
-SG_END_DECL()
+}
+}
 
 #endif
diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 693f4f5d1b..9144932640 100644
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -16,7 +16,7 @@
 
 #ifdef HAVE_MC
 #include "mc_process.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
 #include "mc_protocol.h"
 #include "mc_smx.h"
 #include "mc_server.h"
@@ -30,7 +30,7 @@ void MC_wait_for_requests(void)
 {
 #ifdef HAVE_MC
   if (mc_mode == MC_MODE_SERVER) {
-    MC_server_wait_client(&mc_model_checker->process);
+    MC_server_wait_client(&mc_model_checker->process());
     return;
   }
 #endif
@@ -67,8 +67,8 @@ 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)) {
-      MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+    if (!MC_process_is_self(&mc_model_checker->process())) {
+      MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
         &temp_synchro, act, sizeof(temp_synchro),
         MC_PROCESS_INDEX_ANY);
       act = &temp_synchro;
@@ -92,13 +92,13 @@ int MC_request_is_enabled(smx_simcall_t req)
 #ifdef HAVE_MC
     // Read dynar:
     s_xbt_dynar_t comms;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &comms, simcall_comm_waitany__get__comms(req), sizeof(comms));
     // Read dynar buffer:
     assert(comms.elmsize == sizeof(act));
     size_t buffer_size = comms.elmsize * comms.used;
     char buffer[buffer_size];
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       buffer, comms.data, sizeof(buffer));
 #endif
 
@@ -111,8 +111,8 @@ 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)) {
-        MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+      if (!MC_process_is_self(&mc_model_checker->process())) {
+        MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
           &temp_synchro, act, sizeof(temp_synchro),
           MC_PROCESS_INDEX_ANY);
         act = &temp_synchro;
@@ -129,8 +129,8 @@ 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)) {
-      MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+    if (!MC_process_is_self(&mc_model_checker->process())) {
+      MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
         &temp_mutex, mutex, sizeof(temp_mutex),
         MC_PROCESS_INDEX_ANY);
       mutex = &temp_mutex;
@@ -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_process_is_self(&mc_model_checker->process())) {
     SIMIX_simcall_handle(req, value);
     return;
   }
@@ -218,9 +218,9 @@ void MC_simcall_handle(smx_simcall_t req, int value)
   unsigned i;
   mc_smx_process_info_t pi = NULL;
 
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, pi) {
     if (req == &pi->copy.simcall) {
-      MC_server_simcall_handle(&mc_model_checker->process, pi->copy.pid, value);
+      MC_server_simcall_handle(&mc_model_checker->process(), pi->copy.pid, value);
       return;
     }
   }
diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 473a883de3..1fc08e1875 100644
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -125,7 +125,7 @@ static mc_mem_region_t mc_region_new_dense(
   region->permanent_addr = permanent_addr;
   region->size = size;
   region->flat.data = xbt_malloc(size);
-  MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+  MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
     region->flat.data, permanent_addr, size,
     MC_PROCESS_INDEX_DISABLED);
   XBT_DEBUG("New region : type : %d, data : %p (real addr %p), size : %zu",
@@ -163,12 +163,12 @@ static void MC_region_restore(mc_mem_region_t region)
     break;
 
   case MC_REGION_STORAGE_TYPE_FLAT:
-    MC_process_write(&mc_model_checker->process, region->flat.data,
+    MC_process_write(&mc_model_checker->process(), region->flat.data,
       region->permanent_addr, region->size);
     break;
 
   case MC_REGION_STORAGE_TYPE_CHUNKED:
-    mc_region_restore_sparse(&mc_model_checker->process, region);
+    mc_region_restore_sparse(&mc_model_checker->process(), region);
     break;
 
   case MC_REGION_STORAGE_TYPE_PRIVATIZED:
@@ -198,11 +198,11 @@ static mc_mem_region_t MC_region_new_privatized(
 
   // Read smpi_privatisation_regions from MCed:
   smpi_privatisation_region_t remote_smpi_privatisation_regions;
-  MC_process_read_variable(&mc_model_checker->process,
+  MC_process_read_variable(&mc_model_checker->process(),
     "smpi_privatisation_regions",
     &remote_smpi_privatisation_regions, sizeof(remote_smpi_privatisation_regions));
   s_smpi_privatisation_region_t privatisation_regions[process_count];
-  MC_process_read_simple(&mc_model_checker->process, &privatisation_regions,
+  MC_process_read_simple(&mc_model_checker->process(), &privatisation_regions,
     remote_smpi_privatisation_regions, sizeof(privatisation_regions));
 
   for (size_t i = 0; i < process_count; i++) {
@@ -262,7 +262,7 @@ static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot)
 #ifdef HAVE_SMPI
   if (smpi_privatize_global_variables && MC_smpi_process_count()) {
     // snapshot->privatization_index = smpi_loaded_page
-    MC_process_read_variable(&mc_model_checker->process,
+    MC_process_read_variable(&mc_model_checker->process(),
       "smpi_loaded_page", &snapshot->privatization_index,
       sizeof(snapshot->privatization_index));
   } else
@@ -356,7 +356,7 @@ static bool mc_valid_variable(dw_variable_t var, dw_frame_t scope,
 static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
                                            dw_frame_t scope, int process_index, xbt_dynar_t result)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   void *ip = (void *) stack_frame->ip;
   if (ip < scope->low_pc || ip >= scope->high_pc)
@@ -392,7 +392,7 @@ static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
         current_variable->object_info,
         &(stack_frame->unw_cursor),
         (void *) stack_frame->frame_base,
-        (mc_address_space_t) &mc_model_checker->process, process_index);
+        (mc_address_space_t) &mc_model_checker->process(), process_index);
 
       switch(mc_get_location_type(&location)) {
       case MC_LOCATION_TYPE_ADDRESS:
@@ -443,7 +443,7 @@ static void MC_stack_frame_free_voipd(void *s)
 
 static xbt_dynar_t MC_unwind_stack_frames(mc_unw_context_t stack_context)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   xbt_dynar_t result =
       xbt_dynar_new(sizeof(mc_stack_frame_t), MC_stack_frame_free_voipd);
 
@@ -521,11 +521,11 @@ static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot)
 
     // Read the context from remote process:
     unw_context_t context;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &context, (unw_context_t*) current_stack->context, sizeof(context));
 
     st->context = xbt_new0(s_mc_unw_context_t, 1);
-    if (mc_unw_init_context(st->context, &mc_model_checker->process,
+    if (mc_unw_init_context(st->context, &mc_model_checker->process(),
       &context) < 0) {
       xbt_die("Could not initialise the libunwind context.");
     }
@@ -587,7 +587,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   // Copy the memory:
   unsigned int cursor = 0;
   mc_checkpoint_ignore_region_t region;
-  xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) {
+  xbt_dynar_foreach (mc_model_checker->process().checkpoint_ignore, cursor, region) {
     s_mc_snapshot_ignored_data_t ignored_data;
     ignored_data.start = region->addr;
     ignored_data.size = region->size;
@@ -600,7 +600,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   }
 
   // Zero the memory:
-  xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) {
+  xbt_dynar_foreach (mc_model_checker->process().checkpoint_ignore, cursor, region) {
     MC_process_clear_memory(snapshot->process, region->addr, region->size);
   }
 
@@ -616,25 +616,6 @@ static void MC_snapshot_ignore_restore(mc_snapshot_t snapshot)
   }
 }
 
-/** @brief Can we remove this snapshot?
- *
- * Some snapshots cannot be removed (yet) because we need them
- * at this point.
- *
- * @param snapshot
- */
-int mc_important_snapshot(mc_snapshot_t snapshot)
-{
-  // We need this snapshot in order to know which
-  // pages needs to be stored in the next snapshot.
-  // This field is only non-NULL when using soft-dirty
-  // page tracking.
-  if (snapshot == mc_model_checker->parent_snapshot)
-    return true;
-
-  return false;
-}
-
 static void MC_get_current_fd(mc_snapshot_t snapshot)
 {
 
@@ -725,7 +706,7 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 {
   XBT_DEBUG("Taking snapshot %i", num_state);
 
-  mc_process_t mc_process = &mc_model_checker->process;
+  mc_process_t mc_process = &mc_model_checker->process();
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
   snapshot->process = mc_process;
   snapshot->num_state = num_state;
@@ -817,7 +798,7 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
   if (_sg_mc_snapshot_fds)
     MC_restore_snapshot_fds(snapshot);
   MC_snapshot_ignore_restore(snapshot);
-  mc_model_checker->process.cache_flags = 0;
+  mc_model_checker->process().cache_flags = 0;
 }
 
 mc_snapshot_t simcall_HANDLER_mc_snapshot(smx_simcall_t simcall)
diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp
index 984a221ac0..6109240b25 100644
--- a/src/mc/mc_client.cpp
+++ b/src/mc/mc_client.cpp
@@ -21,7 +21,6 @@
 // We won't need those once the separation MCer/MCed is complete:
 #include "mc_mmalloc.h"
 #include "mc_ignore.h"
-#include "mc_model_checker.h"
 #include "mc_private.h" // MC_deadlock_check()
 #include "mc_smx.h"
 
diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index 192770fe5e..179033ba13 100644
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -12,10 +12,10 @@
 #include "mc_record.h"
 #include "mc_private.h"
 #include "mc_mmalloc.h"
-#include "mc_model_checker.h"
 #include "mc_ignore.h"
 #include "mc_protocol.h"
 #include "mc_client.h"
+#include "ModelChecker.hpp"
 
 extern "C" {
 
@@ -65,7 +65,7 @@ void MC_ignore(void* addr, size_t size)
 
   // TODO, remove this once the migration has been completed
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-  MC_process_ignore_memory(&mc_model_checker->process, addr, size);
+  MC_process_ignore_memory(&mc_model_checker->process(), addr, size);
   mmalloc_set_current_heap(heap);
 }
 
diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index 61b2027390..bede55833d 100644
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -91,7 +91,7 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p
 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
 {
   s_smx_synchro_t comm;
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     &comm, comm_addr, sizeof(comm));
 
   smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
@@ -102,11 +102,11 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co
   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
   if (comm_pattern->data_size == -1 && comm.comm.src_buff != NULL) {
     size_t buff_size;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &buff_size, comm.comm.dst_buff_size, sizeof(buff_size));
     comm_pattern->data_size = buff_size;
     comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       comm_pattern->data, comm.comm.src_buff, comm_pattern->data_size);
   }
 }
@@ -185,20 +185,20 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     pattern->comm_addr = simcall_comm_isend__get__result(request);
 
     s_smx_synchro_t synchro;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &synchro, pattern->comm_addr, sizeof(synchro));
 
     char* remote_name;
-    MC_process_read_simple(&mc_model_checker->process, &remote_name,
+    MC_process_read_simple(&mc_model_checker->process(), &remote_name,
       synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
       sizeof(remote_name));
     pattern->rdv =
-      MC_process_read_string(&mc_model_checker->process, remote_name);
+      MC_process_read_string(&mc_model_checker->process(), remote_name);
     pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
     pattern->src_host = MC_smx_process_get_host_name(issuer);
 
     struct s_smpi_mpi_request mpi_request;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &mpi_request, (MPI_Request) simcall_comm_isend__get__data(request),
       sizeof(mpi_request));
     pattern->tag = mpi_request.tag;
@@ -206,7 +206,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     if(synchro.comm.src_buff != NULL){
       pattern->data_size = synchro.comm.src_buff_size;
       pattern->data = xbt_malloc0(pattern->data_size);
-      MC_process_read_simple(&mc_model_checker->process,
+      MC_process_read_simple(&mc_model_checker->process(),
         pattern->data, synchro.comm.src_buff, pattern->data_size);
     }
     if(mpi_request.detached){
@@ -231,21 +231,21 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 
     struct s_smpi_mpi_request mpi_request;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &mpi_request, (MPI_Request) simcall_comm_irecv__get__data(request),
       sizeof(mpi_request));
     pattern->tag = mpi_request.tag;
 
     s_smx_synchro_t synchro;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &synchro, pattern->comm_addr, sizeof(synchro));
 
     char* remote_name;
-    MC_process_read_simple(&mc_model_checker->process, &remote_name,
+    MC_process_read_simple(&mc_model_checker->process(), &remote_name,
       synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
       sizeof(remote_name));
     pattern->rdv =
-      MC_process_read_string(&mc_model_checker->process, remote_name);
+      MC_process_read_string(&mc_model_checker->process(), remote_name);
     pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
     pattern->dst_host = MC_smx_process_get_host_name(issuer);
   } else {
diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp
index 0141625341..a5b6e49f5e 100644
--- a/src/mc/mc_comm_pattern.cpp
+++ b/src/mc/mc_comm_pattern.cpp
@@ -125,7 +125,7 @@ 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)):
-        MC_process_read_dynar_element(&mc_model_checker->process, &comm_addr,
+        MC_process_read_dynar_element(&mc_model_checker->process(), &comm_addr,
           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);
diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 2d66dbaf61..1cfbd3c1d1 100644
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -104,7 +104,7 @@ static int compare_areas_with_type(struct mc_compare_state& state,
                                    void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2,
                                    dw_type_t type, int pointer_level)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   unsigned int cursor = 0;
   dw_type_t member, subtype, subsubtype;
@@ -387,7 +387,7 @@ static int compare_local_variables(int process_index,
 
 int snapshot_compare(void *state1, void *state2)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   mc_snapshot_t s1, s2;
   int num1, num2;
diff --git a/src/mc/mc_diff.cpp b/src/mc/mc_diff.cpp
index 5b692dcb0a..b8fc44c234 100644
--- a/src/mc/mc_diff.cpp
+++ b/src/mc/mc_diff.cpp
@@ -368,7 +368,7 @@ int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1,
 
   state->heaplimit = ((struct mdesc *) heap1)->heaplimit;
   
-  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process);
+  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process());
 
   state->heapsize1 = heap1->heapsize;
   state->heapsize2 = heap2->heapsize;
@@ -429,7 +429,7 @@ mc_mem_region_t MC_get_heap_region(mc_snapshot_t snapshot)
 
 int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   struct s_mc_diff *state = mc_diff_info;
 
   /* Start comparison */
@@ -784,7 +784,7 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, int process_i
                                           xbt_dynar_t previous, int size,
                                           int check_ignore)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   int i = 0;
   const void *addr_pointed1, *addr_pointed2;
@@ -1139,7 +1139,7 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
                       mc_snapshot_t snapshot2, xbt_dynar_t previous,
                       dw_type_t type, int pointer_level)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   struct s_mc_diff *state = mc_diff_info;
 
@@ -1610,7 +1610,7 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2)
   /* Heap information */
   state->heaplimit = ((struct mdesc *) heap1)->heaplimit;
 
-  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process);
+  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process());
 
   state->heapbase1 = (char *) heap1 + BLOCKSIZE;
   state->heapbase2 = (char *) heap2 + BLOCKSIZE;
diff --git a/src/mc/mc_forward.h b/src/mc/mc_forward.h
index 55a3a751ee..3e3baa1d96 100644
--- a/src/mc/mc_forward.h
+++ b/src/mc/mc_forward.h
@@ -10,21 +10,34 @@
 #include <xbt/misc.h>
 #include <mc/datatypes.h>
 
-SG_BEGIN_DECL()
+#ifdef __cplusplus
+
+namespace simgrid {
+namespace mc {
+  class ModelChecker;
+}
+}
+
+typedef ::simgrid::mc::ModelChecker s_mc_model_checker_t;
+
+#else
+
+typedef struct _s_mc_model_checker s_mc_model_checker_t;
+
+#endif
 
 typedef struct s_mc_object_info s_mc_object_info_t, *mc_object_info_t;
 typedef struct s_dw_type s_dw_type_t, *dw_type_t;
 typedef struct s_memory_map s_memory_map_t, *memory_map_t;
 typedef struct s_dw_variable s_dw_variable_t, *dw_variable_t;
 typedef struct s_dw_frame s_dw_frame_t, *dw_frame_t;
-
 typedef struct s_mc_pages_store s_mc_pages_store_t, *mc_pages_store_t;
 typedef struct s_mc_snapshot s_mc_snapshot_t, *mc_snapshot_t;
-
 typedef struct s_mc_process s_mc_process_t, * mc_process_t;
-typedef struct s_mc_model_checker s_mc_model_checker_t, *mc_model_checker_t;
-extern mc_model_checker_t mc_model_checker;
+typedef s_mc_model_checker_t *mc_model_checker_t;
 
+SG_BEGIN_DECL()
+extern mc_model_checker_t mc_model_checker;
 SG_END_DECL()
 
 #endif
diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 353eb42d07..7a9ebfd057 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -118,12 +118,12 @@ void MC_init_pid(pid_t pid, int socket)
      iteration of the model-checker (in RAW memory) */
 
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-  mc_model_checker = MC_model_checker_new(pid, socket);
+  mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
 
   // 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",
+    MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid",
       &maxpid, sizeof(maxpid));
     simix_process_maxpid = maxpid;
   }
@@ -226,11 +226,11 @@ int MC_deadlock_check()
 {
   if (mc_mode == MC_MODE_SERVER) {
     int res;
-    if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket,
+    if ((res = MC_protocol_send_simple_message(mc_model_checker->process().socket,
       MC_MESSAGE_DEADLOCK_CHECK)))
       xbt_die("Could not check deadlock state");
     s_mc_int_message_t message;
-    ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0);
+    ssize_t s = MC_receive_message(mc_model_checker->process().socket, &message, sizeof(message), 0);
     if (s == -1)
       xbt_die("Could not receive message");
     else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
@@ -709,6 +709,12 @@ void MC_report_assertion_error(void)
   MC_dump_stack_safety(mc_stack);
   MC_print_statistics(mc_stats);
 }
+
+void MC_invalidate_cache(void)
+{
+  if (mc_model_checker)
+    mc_model_checker->process().cache_flags = 0;
+}
 #endif
 
 }
diff --git a/src/mc/mc_hash.cpp b/src/mc/mc_hash.cpp
index 6e11940004..628b2eb6e2 100644
--- a/src/mc/mc_hash.cpp
+++ b/src/mc/mc_hash.cpp
@@ -82,7 +82,7 @@ static void mc_hash_value(mc_hash_t * hash, mc_hashing_state * state,
                           mc_object_info_t info, const void *address,
                           dw_type_t type)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 top:
 
   switch (type->type) {
diff --git a/src/mc/mc_ignore.cpp b/src/mc/mc_ignore.cpp
index 677fb3354e..1c4516bbf1 100644
--- a/src/mc/mc_ignore.cpp
+++ b/src/mc/mc_ignore.cpp
@@ -206,7 +206,7 @@ void MC_remove_ignore_heap(void *address, size_t size)
 // MCer
 void MC_ignore_global_variable(const char *name)
 {
-  mc_process_t process = &mc_model_checker->process;
+  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");
 
@@ -315,7 +315,7 @@ static void MC_ignore_local_variable_in_object(const char *var_name,
 // MCer
 void MC_ignore_local_variable(const char *var_name, const char *frame_name)
 {
-  mc_process_t process = &mc_model_checker->process;
+  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);
diff --git a/src/mc/mc_model_checker.cpp b/src/mc/mc_model_checker.cpp
deleted file mode 100644
index 96a988858b..0000000000
--- a/src/mc/mc_model_checker.cpp
+++ /dev/null
@@ -1,41 +0,0 @@
-/* Copyright (c) 2008-2014. 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_model_checker.h"
-#include "mc_page_store.h"
-
-extern "C" {
-
-mc_model_checker_t mc_model_checker = NULL;
-
-mc_model_checker_t MC_model_checker_new(pid_t pid, int socket)
-{
-  mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1);
-  mc->pages = mc_pages_store_new();
-  mc->fd_clear_refs = -1;
-  MC_process_init(&mc->process, pid, socket);
-  mc->hosts = xbt_dict_new();
-  return mc;
-}
-
-void MC_model_checker_delete(mc_model_checker_t mc)
-{
-  mc_pages_store_delete(mc->pages);
-  if(mc->record)
-    xbt_dynar_free(&mc->record);
-  MC_process_clear(&mc->process);
-  xbt_dict_free(&mc->hosts);
-}
-
-unsigned long MC_smx_get_maxpid(void)
-{
-  unsigned long maxpid;
-  MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
-    &maxpid, sizeof(maxpid));
-  return maxpid;
-}
-
-}
diff --git a/src/mc/mc_page_snapshot.cpp b/src/mc/mc_page_snapshot.cpp
index a1948b2688..bfcbb31c8c 100644
--- a/src/mc/mc_page_snapshot.cpp
+++ b/src/mc/mc_page_snapshot.cpp
@@ -56,7 +56,7 @@ size_t* mc_take_page_snapshot_region(mc_process_t process,
         MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
           temp, page, xbt_pagesize, MC_PROCESS_INDEX_DISABLED);
       }
-      pagenos[i] = mc_model_checker->pages->store_page(page_data);
+      pagenos[i] = mc_model_checker->page_store().store_page(page_data);
 
   }
 
@@ -67,7 +67,7 @@ size_t* mc_take_page_snapshot_region(mc_process_t process,
 void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count)
 {
   for (size_t i=0; i!=page_count; ++i) {
-    mc_model_checker->pages->unref_page(pagenos[i]);
+    mc_model_checker->page_store().unref_page(pagenos[i]);
   }
 }
 
@@ -86,7 +86,7 @@ void mc_restore_page_snapshot_region(mc_process_t process,
   for (size_t i=0; i!=page_count; ++i) {
     // Otherwise, copy the page:
     void* target_page = mc_page_from_number(start_addr, i);
-    const void* source_page = mc_model_checker->pages->get_page(pagenos[i]);
+    const void* source_page = mc_model_checker->page_store().get_page(pagenos[i]);
     MC_process_write(process, source_page, target_page, xbt_pagesize);
   }
 }
@@ -96,7 +96,7 @@ void mc_restore_page_snapshot_region(mc_process_t process,
 mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type,
   void *start_addr, void* permanent_addr, size_t size)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
   region->region_type = region_type;
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index a83d8030ad..85e0f21878 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -144,6 +144,8 @@ void MC_dump_stacks(FILE* file);
 
 void MC_report_assertion_error(void);
 
+void MC_invalidate_cache(void);
+
 SG_END_DECL()
 
 #endif
diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 30ea2e768e..d10a28c744 100644
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -212,6 +212,8 @@ static inline malloc_info* MC_process_get_malloc_info(mc_process_t process)
  */
 dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
 
+void MC_invalidate_cache(void);
+
 SG_END_DECL()
 
 #endif
diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index cfe0cbdd4f..6734597647 100644
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -15,7 +15,6 @@
 
 #ifdef HAVE_MC
 #include "mc_private.h"
-#include "mc_model_checker.h"
 #include "mc_state.h"
 #include "mc_smx.h"
 #endif
diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index 0209effe3b..c3de6850aa 100644
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -275,7 +275,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     // size_t size = size_pointer ? *size_pointer : 0;
     size_t size = 0;
     if (remote_size)
-      MC_process_read_simple(&mc_model_checker->process, &size,
+      MC_process_read_simple(&mc_model_checker->process(), &size,
         remote_size, sizeof(size));
 
     type = "iRecv";
@@ -311,7 +311,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       s_smx_synchro_t synchro;
       smx_synchro_t act;
       if (use_remote_comm) {
-        MC_process_read_simple(&mc_model_checker->process, &synchro,
+        MC_process_read_simple(&mc_model_checker->process(), &synchro,
           remote_act, sizeof(synchro));
         act = &synchro;
       } else
@@ -336,7 +336,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     s_smx_synchro_t synchro;
       smx_synchro_t act;
       if (use_remote_comm) {
-        MC_process_read_simple(&mc_model_checker->process, &synchro,
+        MC_process_read_simple(&mc_model_checker->process(), &synchro,
           remote_act, sizeof(synchro));
         act = &synchro;
       } else
@@ -368,11 +368,11 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
   case SIMCALL_COMM_WAITANY: {
     type = "WaitAny";
     s_xbt_dynar_t comms;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &comms,  simcall_comm_waitany__get__comms(req), sizeof(comms));
     if (!xbt_dynar_is_empty(&comms)) {
       smx_synchro_t remote_sync;
-      MC_process_read_dynar_element(&mc_model_checker->process,
+      MC_process_read_dynar_element(&mc_model_checker->process(),
         &remote_sync, simcall_comm_waitany__get__comms(req), value,
         sizeof(remote_sync));
       char* p = pointer_to_string(remote_sync);
@@ -393,7 +393,7 @@ 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,
-                  MC_process_read_dynar_length(&mc_model_checker->process,
+                  MC_process_read_dynar_length(&mc_model_checker->process(),
                     simcall_comm_testany__get__comms(req)));
     }
     break;
@@ -402,10 +402,10 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     type = "Mutex LOCK";
 
     s_smx_mutex_t mutex;
-    MC_process_read_simple(&mc_model_checker->process, &mutex,
+    MC_process_read_simple(&mc_model_checker->process(), &mutex,
       simcall_mutex_lock__get__mutex(req), sizeof(mutex));
     s_xbt_swag_t mutex_sleeping;
-    MC_process_read_simple(&mc_model_checker->process, &mutex_sleeping,
+    MC_process_read_simple(&mc_model_checker->process(), &mutex_sleeping,
       mutex.sleeping, sizeof(mutex_sleeping));
 
     args = bprintf("locked = %d, owner = %d, sleeping = %d",
@@ -458,13 +458,13 @@ unsigned int MC_request_testany_fail(smx_simcall_t req)
 
   // Read the dynar:
   s_xbt_dynar_t comms;
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     &comms, simcall_comm_testany__get__comms(req), sizeof(comms));
 
   // Read ther dynar buffer:
   size_t buffer_size = comms.elmsize * comms.used;
   char buffer[buffer_size];
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     buffer, comms.data, buffer_size);
 
   // Iterate over the elements:
@@ -478,7 +478,7 @@ unsigned int MC_request_testany_fail(smx_simcall_t req)
 
     // Dereference the pointer:
     s_smx_synchro_t action;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &action, remote_action, sizeof(action));
 
     // Finally so something useful about it:
@@ -501,14 +501,14 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 
   case SIMCALL_COMM_WAITANY: {
     MC_process_read_dynar_element(
-      &mc_model_checker->process, &remote_act, simcall_comm_waitany__get__comms(req),
+      &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
       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),
+      &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
       idx, sizeof(remote_act));
     }
     break;
@@ -518,7 +518,7 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
   }
 
   s_smx_synchro_t synchro;
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     &synchro, remote_act, sizeof(synchro));
   return synchro.comm.src_proc && synchro.comm.dst_proc;
 }
@@ -564,7 +564,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     } else {
       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
       s_smx_synchro_t synchro;
-      MC_process_read_simple(&mc_model_checker->process, &synchro,
+      MC_process_read_simple(&mc_model_checker->process(), &synchro,
         remote_act, sizeof(synchro));
 
       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
@@ -587,7 +587,7 @@ char *MC_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);
     s_smx_synchro_t synchro;
-    MC_process_read_simple(&mc_model_checker->process, &synchro,
+    MC_process_read_simple(&mc_model_checker->process(), &synchro,
       remote_act, sizeof(synchro));
     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
       if (issuer->smx_host)
@@ -609,7 +609,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
   case SIMCALL_COMM_WAITANY: {
     unsigned long comms_size = MC_process_read_dynar_length(
-      &mc_model_checker->process, simcall_comm_waitany__get__comms(req));
+      &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
     if (issuer->smx_host)
       label =
           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index 6cde38d8cb..deffb423b2 100644
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -15,7 +15,7 @@
 
 #include <xbt/log.h>
 
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
 #include "mc_protocol.h"
 #include "mc_server.h"
 #include "mc_private.h"
@@ -92,7 +92,7 @@ void s_mc_server::shutdown()
 {
   XBT_DEBUG("Shuting down model-checker");
 
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   int status = process->status;
   if (process->running) {
     XBT_DEBUG("Killing process");
@@ -107,13 +107,13 @@ void s_mc_server::shutdown()
 void s_mc_server::exit()
 {
   // Finished:
-  int status = mc_model_checker->process.status;
+  int status = mc_model_checker->process().status;
   if (WIFEXITED(status))
     ::exit(WEXITSTATUS(status));
   else if (WIFSIGNALED(status)) {
     // Try to uplicate the signal of the model-checked process.
     // This is a temporary hack so we don't try too hard.
-    kill(mc_model_checker->process.pid, WTERMSIG(status));
+    kill(mc_model_checker->process().pid, WTERMSIG(status));
     abort();
   } else {
     xbt_die("Unexpected status from model-checked process");
@@ -196,7 +196,7 @@ bool s_mc_server::handle_events()
           if (size != sizeof(message))
             xbt_die("Broken messsage");
           memcpy(&message, buffer, sizeof(message));
-          MC_process_ignore_memory(&mc_model_checker->process,
+          MC_process_ignore_memory(&mc_model_checker->process(),
             message.addr, message.size);
           break;
         }
@@ -224,7 +224,7 @@ bool s_mc_server::handle_events()
           XBT_DEBUG("Received symbol: %s", message.name);
 
           struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1);
-          callback->process = &mc_model_checker->process;
+          callback->process = &mc_model_checker->process();
           callback->value   = message.data;
 
           MC_automaton_new_propositional_symbol_callback(message.name,
@@ -270,7 +270,7 @@ bool s_mc_server::handle_events()
 
 void s_mc_server::loop()
 {
-  while (mc_model_checker->process.running)
+  while (mc_model_checker->process().running)
     this->handle_events();
 }
 
@@ -303,7 +303,7 @@ void s_mc_server::handle_waitpid()
     if (pid == -1) {
       if (errno == ECHILD) {
         // No more children:
-        if (mc_model_checker->process.running)
+        if (mc_model_checker->process().running)
           xbt_die("Inconsistent state");
         else
           break;
@@ -313,11 +313,11 @@ void s_mc_server::handle_waitpid()
       }
     }
 
-    if (pid == mc_model_checker->process.pid) {
+    if (pid == mc_model_checker->process().pid) {
       if (WIFEXITED(status) || WIFSIGNALED(status)) {
         XBT_DEBUG("Child process is over");
-        mc_model_checker->process.status = status;
-        mc_model_checker->process.running = false;
+        mc_model_checker->process().status = status;
+        mc_model_checker->process().running = false;
       }
     }
   }
@@ -337,7 +337,7 @@ void s_mc_server::on_signal(const struct signalfd_siginfo* info)
 void MC_server_wait_client(mc_process_t process)
 {
   mc_server->resume(process);
-  while (mc_model_checker->process.running) {
+  while (mc_model_checker->process().running) {
     if (!mc_server->handle_events())
       return;
   }
@@ -350,9 +350,9 @@ void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = pid;
   m.value = value;
-  MC_protocol_send(mc_model_checker->process.socket, &m, sizeof(m));
+  MC_protocol_send(mc_model_checker->process().socket, &m, sizeof(m));
   process->cache_flags = (mc_process_cache_flags_t) 0;
-  while (mc_model_checker->process.running) {
+  while (mc_model_checker->process().running) {
     if (!mc_server->handle_events())
       return;
   }
diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index a10abd588d..12d9216155 100644
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -11,7 +11,7 @@
 #include "simix/smx_private.h"
 
 #include "mc_smx.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
 
 extern "C" {
 
@@ -44,8 +44,8 @@ bool is_in_dynar(smx_process_t p, xbt_dynar_t dynar)
 static inline
 mc_smx_process_info_t MC_smx_process_get_info(smx_process_t p)
 {
-  assert(is_in_dynar(p, mc_model_checker->process.smx_process_infos)
-    || is_in_dynar(p, mc_model_checker->process.smx_old_process_infos));
+  assert(is_in_dynar(p, mc_model_checker->process().smx_process_infos)
+    || is_in_dynar(p, mc_model_checker->process().smx_old_process_infos));
   mc_smx_process_info_t process_info =
     (mc_smx_process_info_t)
       ((char*) p - offsetof(s_mc_smx_process_info_t, copy));
@@ -126,10 +126,10 @@ 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_process_is_self(&mc_model_checker->process()))
     return req->issuer;
 
-  MC_process_smx_refresh(&mc_model_checker->process);
+  MC_process_smx_refresh(&mc_model_checker->process());
 
   // This is the address of the smx_process in the MCed process:
   void* address = req->issuer;
@@ -138,10 +138,10 @@ smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
   mc_smx_process_info_t p;
 
   // Lookup by address:
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, p)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, p)
     if (p->address == address)
       return &p->copy;
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, i, p)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_old_process_infos, i, p)
     if (p->address == address)
       return &p->copy;
 
@@ -152,7 +152,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_process_is_self(&mc_model_checker->process()))
     return process_remote_address;
 
   mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address);
@@ -164,15 +164,15 @@ 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_process_is_self(&mc_model_checker->process()))
     xbt_die("No process_info for local process is not enabled.");
 
   unsigned index;
   mc_smx_process_info_t process_info;
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, index, process_info)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, index, process_info)
     if (process_info->address == process_remote_address)
       return process_info;
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, index, process_info)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_old_process_infos, index, process_info)
     if (process_info->address == process_remote_address)
       return process_info;
   xbt_die("Process info not found");
@@ -180,10 +180,10 @@ 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_process_is_self(&mc_model_checker->process()))
     return SIMIX_host_get_name(p->smx_host);
 
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   // Currently, smx_host_t = xbt_dictelm_t.
   // TODO, add an static_assert on this if switching to C++
@@ -197,25 +197,14 @@ const char* MC_smx_process_get_host_name(smx_process_t p)
     int len = host_copy.key_len + 1;
     char hostname[len];
     MC_process_read_simple(process, hostname, host_copy.key, len);
-
-    // Lookup the host name in the dictionary (or create it):
-    xbt_dictelm_t elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname);
-    if (!elt) {
-      xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-      xbt_dict_set(mc_model_checker->hosts, hostname, NULL, NULL);
-      elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname);
-      assert(elt);
-      mmalloc_set_current_heap(heap);
-    }
-
-    info->hostname = elt->key;
+    info->hostname = mc_model_checker->get_host_name(hostname);
   }
   return info->hostname;
 }
 
 const char* MC_smx_process_get_name(smx_process_t p)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   if (MC_process_is_self(process))
     return p->name;
   if (!p->name)
@@ -232,14 +221,22 @@ 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_process_is_self(&mc_model_checker->process()))
     return smpi_process_count();
   else {
     int res;
-    MC_process_read_variable(&mc_model_checker->process, "process_count",
+    MC_process_read_variable(&mc_model_checker->process(), "process_count",
       &res, sizeof(res));
     return res;
   }
 }
 
+unsigned long MC_smx_get_maxpid(void)
+{
+  unsigned long maxpid;
+  MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid",
+    &maxpid, sizeof(maxpid));
+  return maxpid;
+}
+
 }
diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h
index 5cd2e1d5af..123052c50a 100644
--- a/src/mc/mc_smx.h
+++ b/src/mc/mc_smx.h
@@ -45,7 +45,7 @@ struct s_mc_smx_process_info {
   /** (Flat) Copy of the process data structure */
   struct s_smx_process copy;
   /** Hostname (owned by `mc_modelchecker->hostnames`) */
-  char* hostname;
+  const char* hostname;
   char* name;
 };
 
@@ -68,15 +68,15 @@ 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_process_is_self(&mc_model_checker->process())) { \
     xbt_swag_foreach(process, simix_global->process_list) { \
       code; \
     } \
   } else { \
-    MC_process_smx_refresh(&mc_model_checker->process); \
+    MC_process_smx_refresh(&mc_model_checker->process()); \
     unsigned int _smx_process_index; \
     mc_smx_process_info_t _smx_process_info; \
-    xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \
+    xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, _smx_process_index, _smx_process_info) { \
       smx_process_t process = &_smx_process_info->copy; \
       code; \
     } \
@@ -96,6 +96,8 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
 /** Get the process info structure from the process remote address */
 mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
 
+unsigned long MC_smx_get_maxpid(void);
+
 SG_END_DECL()
 
 #endif
diff --git a/src/mc/mc_snapshot.cpp b/src/mc/mc_snapshot.cpp
index 82b6ab868a..8a2422d9c6 100644
--- a/src/mc/mc_snapshot.cpp
+++ b/src/mc/mc_snapshot.cpp
@@ -211,8 +211,7 @@ static void test_snapshot(bool sparse_checkpoint) {
   _sg_mc_sparse_checkpoint = sparse_checkpoint;
   xbt_assert(xbt_pagesize == getpagesize());
   xbt_assert(1 << xbt_pagebits == xbt_pagesize);
-  mc_model_checker = xbt_new0(s_mc_model_checker_t, 1);
-  mc_model_checker->pages = mc_pages_store_new();
+  mc_model_checker = new ::simgrid::mc::ModelChecker(getpid(), -1);
 
   for(int n=1; n!=256; ++n) {
 
@@ -285,8 +284,7 @@ static void test_snapshot(bool sparse_checkpoint) {
     munmap(source, byte_size);
   }
 
-  mc_pages_store_delete(mc_model_checker->pages);
-  xbt_free(mc_model_checker);
+  delete mc_model_checker;
   mc_model_checker = NULL;
 }
 
diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h
index 589e502793..ceb0ef66be 100644
--- a/src/mc/mc_snapshot.h
+++ b/src/mc/mc_snapshot.h
@@ -16,7 +16,7 @@
 #include <xbt/dynar.h>
 
 #include "mc_forward.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
 #include "mc_page_store.h"
 #include "mc_mmalloc.h"
 #include "mc_address_space.h"
@@ -112,10 +112,11 @@ bool mc_region_contain(mc_mem_region_t region, const void* p)
 static inline __attribute__((always_inline))
 void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
 {
-    size_t pageno = mc_page_number(region->start_addr, (void*) addr);
-    size_t snapshot_pageno = region->chunked.page_numbers[pageno];
-    const void* snapshot_page = mc_page_store_get_page(mc_model_checker->pages, snapshot_pageno);
-    return (char*) snapshot_page + mc_page_offset((void*) addr);
+  size_t pageno = mc_page_number(region->start_addr, (void*) addr);
+  size_t snapshot_pageno = region->chunked.page_numbers[pageno];
+  const void* snapshot_page = mc_page_store_get_page(
+    &mc_model_checker->page_store(), snapshot_pageno);
+  return (char*) snapshot_page + mc_page_offset((void*) addr);
 }
 
 mc_mem_region_t mc_get_snapshot_region(const void* addr, mc_snapshot_t snapshot, int process_index);
@@ -268,8 +269,6 @@ mc_snapshot_t MC_take_snapshot(int num_state);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
-int mc_important_snapshot(mc_snapshot_t snapshot);
-
 size_t* mc_take_page_snapshot_region(mc_process_t process,
   void* data, size_t page_count);
 void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
@@ -301,7 +300,7 @@ const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot)
 {
   if(snapshot==NULL)
       xbt_die("snapshot is NULL");
-  return MC_process_get_heap(&mc_model_checker->process)->breakval;
+  return MC_process_get_heap(&mc_model_checker->process())->breakval;
 }
 
 /** @brief Read memory from a snapshot region
diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index a3f20eee13..0ebde42a8b 100644
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -105,7 +105,7 @@ 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;
-    MC_process_read_dynar_element(&mc_model_checker->process,
+    MC_process_read_dynar_element(&mc_model_checker->process(),
       &state->internal_comm, simcall_comm_waitany__get__comms(req),
       value, sizeof(state->internal_comm));
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
@@ -117,7 +117,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
     state->internal_req.issuer = req->issuer;
 
     if (value > 0)
-        MC_process_read_dynar_element(&mc_model_checker->process,
+        MC_process_read_dynar_element(&mc_model_checker->process(),
           &state->internal_comm, simcall_comm_testany__get__comms(req),
           value, sizeof(state->internal_comm));
 
@@ -127,7 +127,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_COMM_WAIT:
     state->internal_req = *req;
-    MC_process_read_simple(&mc_model_checker->process, &state->internal_comm ,
+    MC_process_read_simple(&mc_model_checker->process(), &state->internal_comm ,
       simcall_comm_wait__get__comm(req), sizeof(state->internal_comm));
     simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
@@ -135,7 +135,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_COMM_TEST:
     state->internal_req = *req;
-    MC_process_read_simple(&mc_model_checker->process, &state->internal_comm,
+    MC_process_read_simple(&mc_model_checker->process(), &state->internal_comm,
       simcall_comm_test__get__comm(req), sizeof(state->internal_comm));
     simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
@@ -190,7 +190,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_COMM_WAITANY:
         *value = -1;
         while (procstate->interleave_count <
-              MC_process_read_dynar_length(&mc_model_checker->process,
+              MC_process_read_dynar_length(&mc_model_checker->process(),
                 simcall_comm_waitany__get__comms(&process->simcall))) {
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
@@ -200,7 +200,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         }
 
         if (procstate->interleave_count >=
-            MC_process_read_dynar_length(&mc_model_checker->process,
+            MC_process_read_dynar_length(&mc_model_checker->process(),
               simcall_comm_waitany__get__comms(&process->simcall)))
           procstate->state = MC_DONE;
 
@@ -213,7 +213,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         unsigned start_count = procstate->interleave_count;
         *value = -1;
         while (procstate->interleave_count <
-                MC_process_read_dynar_length(&mc_model_checker->process,
+                MC_process_read_dynar_length(&mc_model_checker->process(),
                   simcall_comm_testany__get__comms(&process->simcall))) {
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
@@ -223,7 +223,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         }
 
         if (procstate->interleave_count >=
-            MC_process_read_dynar_length(&mc_model_checker->process,
+            MC_process_read_dynar_length(&mc_model_checker->process(),
               simcall_comm_testany__get__comms(&process->simcall)))
           procstate->state = MC_DONE;
 
@@ -236,7 +236,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_COMM_WAIT: {
         smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
         s_smx_synchro_t act;
-        MC_process_read_simple(&mc_model_checker->process,
+        MC_process_read_simple(&mc_model_checker->process(),
           &act, remote_act, sizeof(act));
         if (act.comm.src_proc && act.comm.dst_proc) {
           *value = 0;
diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 3fd5249198..968965f77f 100644
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -55,18 +55,18 @@ void visited_state_free_voidp(void *s)
  */
 static mc_visited_state_t visited_state_new()
 {
-  mc_process_t process = &(mc_model_checker->process);
+  mc_process_t process = &(mc_model_checker->process());
   mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
     MC_process_get_heap(process)->heaplimit,
     MC_process_get_malloc_info(process));
 
-  if (MC_process_is_self(&mc_model_checker->process)) {
+  if (MC_process_is_self(&mc_model_checker->process())) {
     new_state->nb_processes = xbt_swag_size(simix_global->process_list);
   } else {
-    MC_process_smx_refresh(&mc_model_checker->process);
+    MC_process_smx_refresh(&mc_model_checker->process());
     new_state->nb_processes = xbt_dynar_length(
-      mc_model_checker->process.smx_process_infos);
+      mc_model_checker->process().smx_process_infos);
   }
 
   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
@@ -77,7 +77,7 @@ static mc_visited_state_t visited_state_new()
 
 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
 {
-  mc_process_t process = &(mc_model_checker->process);
+  mc_process_t process = &(mc_model_checker->process());
   mc_visited_pair_t pair = NULL;
   pair = xbt_new0(s_mc_visited_pair_t, 1);
   pair->graph_state = graph_state;
@@ -86,12 +86,12 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa
   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
     MC_process_get_heap(process)->heaplimit,
     MC_process_get_malloc_info(process));
-  if (MC_process_is_self(&mc_model_checker->process)) {
+  if (MC_process_is_self(&mc_model_checker->process())) {
     pair->nb_processes = xbt_swag_size(simix_global->process_list);
   } else {
-    MC_process_smx_refresh(&mc_model_checker->process);
+    MC_process_smx_refresh(&mc_model_checker->process());
     pair->nb_processes = xbt_dynar_length(
-      mc_model_checker->process.smx_process_infos);
+      mc_model_checker->process().smx_process_infos);
   }
   pair->automaton_state = automaton_state;
   pair->num = pair_num;
@@ -362,7 +362,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
-        if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
+        if (state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
@@ -485,7 +485,7 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
-        if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
+        if (pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;
         }
diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 1e9d352c5b..29d5fe2093 100644
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -29,7 +29,6 @@
 #include "mc_private.h"
 #include "mc_protocol.h"
 #include "mc_server.h"
-#include "mc_model_checker.h"
 #include "mc_safety.h"
 #include "mc_comm_pattern.h"
 #include "mc_liveness.h"
diff --git a/src/simix/popping_generated.c b/src/simix/popping_generated.c
index c8a3c3ca97..9f8e55c92f 100644
--- a/src/simix/popping_generated.c
+++ b/src/simix/popping_generated.c
@@ -16,7 +16,6 @@
 #include "smx_private.h"
 #ifdef HAVE_MC
 #include "mc/mc_process.h"
-#include "mc/mc_model_checker.h"
 #endif
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
@@ -163,7 +162,7 @@ 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_model_checker->process.cache_flags = 0;
+    MC_invalidate_cache();
   }
   #endif
   SIMCALL_SET_MC_VALUE(simcall, value);
diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py
index efdd044dfe..997a60b67e 100755
--- a/src/simix/simcalls.py
+++ b/src/simix/simcalls.py
@@ -282,7 +282,6 @@ if __name__=='__main__':
   fd.write('#include "smx_private.h"\n');
   fd.write('#ifdef HAVE_MC\n');
   fd.write('#include "mc/mc_process.h"\n');
-  fd.write('#include "mc/mc_model_checker.h"\n');
   fd.write('#endif\n');
   fd.write('\n');
   fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n');
@@ -305,7 +304,7 @@ if __name__=='__main__':
   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_model_checker->process.cache_flags = 0;\n');
+  fd.write('    MC_invalidate_cache();\n');
   fd.write('  }\n');
   fd.write('  #endif\n');
   fd.write('  SIMCALL_SET_MC_VALUE(simcall, value);\n');
diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index d0ba2747a0..43b0787a3b 100644
--- a/src/simix/smx_global.c
+++ b/src/simix/smx_global.c
@@ -18,7 +18,6 @@
 
 #ifdef HAVE_MC
 #include "mc/mc_private.h"
-#include "mc/mc_model_checker.h"
 #include "mc/mc_protocol.h"
 #include "mc/mc_client.h"
 #endif
diff --git a/teshsuite/mc/dwarf/CMakeLists.txt b/teshsuite/mc/dwarf/CMakeLists.txt
index 89dd9ea9f0..00e46e9e96 100644
--- a/teshsuite/mc/dwarf/CMakeLists.txt
+++ b/teshsuite/mc/dwarf/CMakeLists.txt
@@ -3,7 +3,7 @@ cmake_minimum_required(VERSION 2.6)
 if(HAVE_MC)
   set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
 
-  add_executable(dwarf dwarf.c)
+  add_executable(dwarf dwarf.cpp)
   target_link_libraries(dwarf simgrid)
 endif()
 
@@ -14,6 +14,6 @@ set(tesh_files
   )
 set(testsuite_src
   ${testsuite_src}
-  ${CMAKE_CURRENT_SOURCE_DIR}/dwarf.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/dwarf.cpp
   PARENT_SCOPE
   )
diff --git a/teshsuite/mc/dwarf/dwarf.c b/teshsuite/mc/dwarf/dwarf.cpp
similarity index 94%
rename from teshsuite/mc/dwarf/dwarf.c
rename to teshsuite/mc/dwarf/dwarf.cpp
index c7ad31c335..adbe05dc37 100644
--- a/teshsuite/mc/dwarf/dwarf.c
+++ b/teshsuite/mc/dwarf/dwarf.cpp
@@ -17,7 +17,6 @@
 #include "../../src/include/mc/datatypes.h"
 #include "../../src/mc/mc_object_info.h"
 #include "../../src/mc/mc_private.h"
-#include "../../src/mc/mc_model_checker.h"
 
 int test_some_array[4][5][6];
 struct some_struct { int first; int second[4][5]; } test_some_struct;
@@ -87,7 +86,7 @@ static void test_local_variable(mc_object_info_t info, const char* function, con
 }
 
 static dw_variable_t test_global_variable(mc_process_t process, mc_object_info_t info, const char* name, void* address, long byte_size) {
-  
+
   dw_variable_t variable = MC_file_object_info_find_variable_by_name(info, name);
   xbt_assert(variable, "Global variable %s was not found", name);
   xbt_assert(!strcmp(variable->name, name), "Name mismatch for %s", name);
@@ -95,7 +94,7 @@ static dw_variable_t test_global_variable(mc_process_t process, mc_object_info_t
   xbt_assert(variable->address == address,
       "Address mismatch for %s : %p expected but %p found", name, address, variable->address);
 
-  dw_type_t type = xbt_dict_get_or_null(process->binary_info->types, variable->type_origin);
+  dw_type_t type = (dw_type_t) xbt_dict_get_or_null(process->binary_info->types, variable->type_origin);
   xbt_assert(type!=NULL, "Missing type for %s", name);
   xbt_assert(type->byte_size = byte_size, "Byte size mismatch for %s", name);
   return variable;
@@ -125,7 +124,7 @@ int main(int argc, char** argv)
 
   dw_variable_t var;
   dw_type_t type;
-  
+
   s_mc_process_t p;
   mc_process_t process = &p;
   MC_process_init(&p, getpid(), -1);
@@ -133,11 +132,11 @@ int main(int argc, char** argv)
   test_global_variable(process, process->binary_info, "some_local_variable", &some_local_variable, sizeof(int));
 
   var = test_global_variable(process, process->binary_info, "test_some_array", &test_some_array, sizeof(test_some_array));
-  type = xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
+  type = (dw_type_t) xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
   xbt_assert(type->element_count == 6*5*4, "element_count mismatch in test_some_array : %i / %i", type->element_count, 6*5*4);
 
   var = test_global_variable(process, process->binary_info, "test_some_struct", &test_some_struct, sizeof(test_some_struct));
-  type = xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
+  type = (dw_type_t) xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
   assert(find_member(process->binary_info, "first", type)->offset == 0);
   assert(find_member(process->binary_info, "second", type)->offset
       == ((const char*)&test_some_struct.second) - (const char*)&test_some_struct);
-- 
2.20.1