From: Martin Quinson <martin.quinson@loria.fr>
Date: Fri, 9 Oct 2015 19:25:23 +0000 (+0200)
Subject: Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
X-Git-Tag: v3_12~10
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ac679d5e69b1eb25e3f82be198607593407e7fc5?hp=47a22ba74687bf963bf797d72745e9f1e6f40dd9

Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
---

diff --git a/contrib/psg/tutorial.odt b/contrib/psg/tutorial.odt
index e2633d1a37..9a1f50dd6d 100644
Binary files a/contrib/psg/tutorial.odt and b/contrib/psg/tutorial.odt differ
diff --git a/contrib/psg/tutorial.pdf b/contrib/psg/tutorial.pdf
index faf141bbf1..df0ef22282 100644
Binary files a/contrib/psg/tutorial.pdf and b/contrib/psg/tutorial.pdf differ
diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc
index 450c71095e..539c43ff4b 100644
--- a/doc/doxygen/options.doc
+++ b/doc/doxygen/options.doc
@@ -776,10 +776,10 @@ Here, MAX_BANDWIDTH denotes the bandwidth of the link.
 
 \b Default: 0 (false)
 
-Most of the time, you run MPI code through SMPI to compute the time it
-would take to run it on a platform that you don't have. But since the
+Most of the time, you run MPI code with SMPI to compute the time it
+would take to run it on a platform. But since the
 code is run through the \c smpirun script, you don't have any control
-on the launcher code, making difficult to report the simulated time
+on the launcher code, making it difficult to report the simulated time
 when the simulation ends. If you set the \b smpi/display_timing item
 to 1, \c smpirun will display this information when the simulation ends. \verbatim
 Simulation time: 1e3 seconds.
diff --git a/src/mc/AddressSpace.hpp b/src/mc/AddressSpace.hpp
index b498665284..e23e9ac2e3 100644
--- a/src/mc/AddressSpace.hpp
+++ b/src/mc/AddressSpace.hpp
@@ -7,13 +7,12 @@
 #ifndef SIMGRID_MC_ADDRESS_SPACE_H
 #define SIMGRID_MC_ADDRESS_SPACE_H
 
+#include <cstddef>
 #include <cstdint>
 #include <type_traits>
 
 #include <xbt/misc.h>
 
-#include <stdint.h>
-
 #include "mc_forward.hpp"
 
 namespace simgrid {
@@ -128,6 +127,8 @@ const int ProcessIndexDisabled = -2;
 const int ProcessIndexAny = 0;
 
 class AddressSpace {
+private:
+  Process* process_;
 public:
   enum ReadMode {
     Normal,
@@ -136,7 +137,10 @@ public:
      */
     Lazy
   };
+  AddressSpace(Process* process) : process_(process) {}
   virtual ~AddressSpace();
+
+  simgrid::mc::Process* process() { return process_; }
   virtual const void* read_bytes(void* buffer, std::size_t size,
     remote_ptr<void> address, int process_index = ProcessIndexAny,
     ReadMode mode = Normal) const = 0;
diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 846ea2ba96..f8b0982139 100644
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -14,8 +14,8 @@
 #include <xbt/base.h>
 
 #include "mc_forward.hpp"
-#include "mc_process.h"
-#include "PageStore.hpp"
+#include "mc/Process.hpp"
+#include "mc/PageStore.hpp"
 #include "mc_protocol.h"
 
 namespace simgrid {
@@ -52,6 +52,11 @@ public:
     return page_store_;
   }
   const char* get_host_name(const char* name);
+
+  bool is_important_snapshot(Snapshot const& snapshot) const
+  {
+    return &snapshot == mc_model_checker->parent_snapshot_;
+  }
 };
 
 }
diff --git a/src/mc/mc_process.cpp b/src/mc/Process.cpp
similarity index 89%
rename from src/mc/mc_process.cpp
rename to src/mc/Process.cpp
index 2a70cb52c9..78f4b45738 100644
--- a/src/mc/mc_process.cpp
+++ b/src/mc/Process.cpp
@@ -27,7 +27,6 @@
 
 #include <xbt/mmalloc.h>
 
-#include "mc_process.h"
 #include "mc_object_info.h"
 #include "mc_unw.h"
 #include "mc_snapshot.h"
@@ -35,6 +34,7 @@
 #include "mc_smx.h"
 #include "mc_server.h"
 
+#include "mc/Process.hpp"
 #include "mc/AddressSpace.hpp"
 #include "mc/ObjectInformation.hpp"
 #include "mc/Variable.hpp"
@@ -206,15 +206,11 @@ int open_vm(pid_t pid, int flags)
 namespace simgrid {
 namespace mc {
 
-Process::Process(pid_t pid, int sockfd)
+Process::Process(pid_t pid, int sockfd) : AddressSpace(this)
 {
   Process* process = this;
-
-  process->process_flags = MC_PROCESS_NO_FLAG;
   process->socket_ = sockfd;
   process->pid_ = pid;
-  if (pid==getpid())
-    process->process_flags |= MC_PROCESS_SELF_FLAG;
   process->running_ = true;
   process->status_ = 0;
   process->memory_map_ = get_memory_map(pid);
@@ -225,15 +221,10 @@ Process::Process(pid_t pid, int sockfd)
   process->clear_refs_fd_ = -1;
   process->pagemap_fd_ = -1;
 
-  // Open the memory file
-  if (process->is_self())
-    process->memory_file = -1;
-  else {
-    int fd = open_vm(process->pid_, O_RDWR);
-    if (fd<0)
-      xbt_die("Could not open file for process virtual address space");
-    process->memory_file = fd;
-  }
+  int fd = open_vm(process->pid_, O_RDWR);
+  if (fd<0)
+    xbt_die("Could not open file for process virtual address space");
+  process->memory_file = fd;
 
   // Read std_heap (is a struct mdesc*):
   simgrid::mc::Variable* std_heap_var = process->find_variable("__mmalloc_default_mdp");
@@ -247,15 +238,9 @@ Process::Process(pid_t pid, int sockfd)
 
   process->smx_process_infos = MC_smx_process_info_list_new();
   process->smx_old_process_infos = MC_smx_process_info_list_new();
-
   process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors  , __BYTE_ORDER);
-  if (process->process_flags & MC_PROCESS_SELF_FLAG) {
-    process->unw_underlying_addr_space = unw_local_addr_space;
-    process->unw_underlying_context = NULL;
-  } else {
-    process->unw_underlying_addr_space = unw_create_addr_space(&mc_unw_vmread_accessors, __BYTE_ORDER);
-    process->unw_underlying_context = _UPT_create(pid);
-  }
+  process->unw_underlying_addr_space = unw_create_addr_space(&mc_unw_vmread_accessors, __BYTE_ORDER);
+  process->unw_underlying_context = _UPT_create(pid);
 }
 
 Process::~Process()
@@ -265,7 +250,6 @@ Process::~Process()
   if (this->socket_ >= 0 && close(this->socket_) < 0)
     xbt_die("Could not close communication socket");
 
-  process->process_flags = MC_PROCESS_NO_FLAG;
   process->pid_ = 0;
 
   process->maestro_stack_start_ = nullptr;
@@ -310,7 +294,6 @@ Process::~Process()
 void Process::refresh_heap()
 {
   xbt_assert(mc_mode == MC_MODE_SERVER);
-  xbt_assert(!this->is_self());
   // Read/dereference/refresh the std_heap pointer:
   if (!this->heap) {
     this->heap = (struct mdesc*) malloc(sizeof(struct mdesc));
@@ -328,7 +311,6 @@ void Process::refresh_heap()
 void Process::refresh_malloc_info()
 {
   xbt_assert(mc_mode == MC_MODE_SERVER);
-  xbt_assert(!this->is_self());
   if (!(this->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP))
     this->refresh_heap();
   // Refresh process->heapinfo:
@@ -503,8 +485,6 @@ char* Process::read_string(remote_ptr<void> address) const
 {
   if (!address)
     return NULL;
-  if (this->is_self())
-    return xbt_strdup((char*) address.address());
 
   off_t len = 128;
   char* res = (char*) malloc(len);
@@ -564,18 +544,9 @@ const void *Process::read_bytes(void* buffer, std::size_t size,
 #endif
   }
 
-  if (this->is_self()) {
-    if (mode == simgrid::mc::AddressSpace::Lazy)
-      return (void*)address.address();
-    else {
-      memcpy(buffer, (void*)address.address(), size);
-      return buffer;
-    }
-  } else {
-    if (pread_whole(this->memory_file, buffer, size, address.address()) < 0)
-      xbt_die("Read from process %lli failed", (long long) this->pid_);
-    return buffer;
-  }
+  if (pread_whole(this->memory_file, buffer, size, address.address()) < 0)
+    xbt_die("Read from process %lli failed", (long long) this->pid_);
+  return buffer;
 }
 
 /** Write data to a process memory
@@ -587,26 +558,18 @@ const void *Process::read_bytes(void* buffer, std::size_t size,
  */
 void Process::write_bytes(const void* buffer, size_t len, remote_ptr<void> address)
 {
-  if (this->is_self()) {
-    memcpy((void*)address.address(), buffer, len);
-  } else {
-    if (pwrite_whole(this->memory_file, buffer, len, address.address()) < 0)
-      xbt_die("Write to process %lli failed", (long long) this->pid_);
-  }
+  if (pwrite_whole(this->memory_file, buffer, len, address.address()) < 0)
+    xbt_die("Write to process %lli failed", (long long) this->pid_);
 }
 
 void Process::clear_bytes(remote_ptr<void> address, size_t len)
 {
-  if (this->is_self()) {
-    memset((void*)address.address(), 0, len);
-  } else {
-    pthread_once(&zero_buffer_flag, MC_zero_buffer_init);
-    while (len) {
-      size_t s = len > zero_buffer_size ? zero_buffer_size : len;
-      this->write_bytes(zero_buffer, s, address);
-      address = remote((char*) address.address() + s);
-      len -= s;
-    }
+  pthread_once(&zero_buffer_flag, MC_zero_buffer_init);
+  while (len) {
+    size_t s = len > zero_buffer_size ? zero_buffer_size : len;
+    this->write_bytes(zero_buffer, s, address);
+    address = remote((char*) address.address() + s);
+    len -= s;
   }
 }
 
diff --git a/src/mc/mc_process.h b/src/mc/Process.hpp
similarity index 95%
rename from src/mc/mc_process.h
rename to src/mc/Process.hpp
index 4c21485e82..af42a12653 100644
--- a/src/mc/mc_process.h
+++ b/src/mc/Process.hpp
@@ -35,10 +35,6 @@
 #include "AddressSpace.hpp"
 #include "mc_protocol.h"
 
-typedef int mc_process_flags_t;
-#define MC_PROCESS_NO_FLAG 0
-#define MC_PROCESS_SELF_FLAG 1
-
 // Those flags are used to track down which cached information
 // is still up to date and which information needs to be updated.
 typedef int mc_process_cache_flags_t;
@@ -47,8 +43,6 @@ typedef int mc_process_cache_flags_t;
 #define MC_PROCESS_CACHE_FLAG_MALLOC_INFO 2
 #define MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES 4
 
-typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
-
 namespace simgrid {
 namespace mc {
 
@@ -59,16 +53,15 @@ struct IgnoredRegion {
 
 /** Representation of a process
  */
-class Process : public AddressSpace {
+class Process final : public AddressSpace {
 public:
   Process(pid_t pid, int sockfd);
   ~Process();
 
-
-  bool is_self() const
-  {
-    return this->process_flags & MC_PROCESS_SELF_FLAG;
-  }
+  Process(Process const&) = delete;
+  Process(Process &&) = delete;
+  Process& operator=(Process const&) = delete;
+  Process& operator=(Process &&) = delete;
 
   // Read memory:
   const void* read_bytes(void* buffer, std::size_t size,
@@ -166,7 +159,6 @@ private:
   void refresh_heap();
   void refresh_malloc_info();
 private:
-  mc_process_flags_t process_flags;
   pid_t pid_;
   int socket_;
   int status_;
diff --git a/src/mc/Type.hpp b/src/mc/Type.hpp
index bc3cc45e61..540bf4ca37 100644
--- a/src/mc/Type.hpp
+++ b/src/mc/Type.hpp
@@ -18,33 +18,17 @@
 namespace simgrid {
 namespace mc {
 
-/** Represents a type in the program
- *
- *  It is currently used to represent members of structs and unions as well.
- */
-class Type {
+/** Represent a member of  a structure (or inheritance) */
+class Member {
 public:
-  Type();
-  Type(Type const& type) = default;
-  Type& operator=(Type const&) = default;
-  Type(Type&& type) = default;
-  Type& operator=(Type&&) = default;
-
-  /** The DWARF TAG of the type (e.g. DW_TAG_array_type) */
-  int type;
-  unsigned id; /* Offset in the section (in hexadecimal form) */
-  std::string name; /* Name of the type */
-  int byte_size; /* Size in bytes */
-  int element_count; /* Number of elements for array type */
-  unsigned type_id; /* DW_AT_type id */
-  std::vector<Type> members; /* if DW_TAG_structure_type, DW_TAG_class_type, DW_TAG_union_type*/
-  int is_pointer_type;
+  Member() : inheritance(false), byte_size(0), type_id(0) {}
 
-  // Location (for members) is either of:
+  bool inheritance;
+  std::string name;
   simgrid::mc::DwarfExpression location_expression;
-
-  simgrid::mc::Type* subtype; // DW_AT_type
-  simgrid::mc::Type* full_type; // The same (but more complete) type
+  std::size_t byte_size; // Do we really need this?
+  unsigned type_id;
+  simgrid::mc::Type* type;
 
   bool has_offset_location() const
   {
@@ -68,6 +52,32 @@ public:
   }
 };
 
+/** Represents a type in the program
+ *
+ *  It is currently used to represent members of structs and unions as well.
+ */
+class Type {
+public:
+  Type();
+  Type(Type const& type) = default;
+  Type& operator=(Type const&) = default;
+  Type(Type&& type) = default;
+  Type& operator=(Type&&) = default;
+
+  /** The DWARF TAG of the type (e.g. DW_TAG_array_type) */
+  int type;
+  unsigned id; /* Offset in the section (in hexadecimal form) */
+  std::string name; /* Name of the type */
+  int byte_size; /* Size in bytes */
+  int element_count; /* Number of elements for array type */
+  unsigned type_id; /* DW_AT_type id */
+  std::vector<Member> members; /* if DW_TAG_structure_type, DW_TAG_class_type, DW_TAG_union_type*/
+  int is_pointer_type;
+
+  simgrid::mc::Type* subtype; // DW_AT_type
+  simgrid::mc::Type* full_type; // The same (but more complete) type
+};
+
 inline
 Type::Type()
 {
diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 74c8268aaf..f38cf7bf91 100644
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -16,8 +16,8 @@
 #include "mc_protocol.h"
 
 #ifdef HAVE_MC
-#include "mc_process.h"
-#include "ModelChecker.hpp"
+#include "mc/Process.hpp"
+#include "mc/ModelChecker.hpp"
 #include "mc_smx.h"
 #include "mc_server.h"
 #endif
diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 97ddc26b0f..763e116109 100644
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -50,18 +50,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
 /************************************  Free functions **************************************/
 /*****************************************************************************************/
 
-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;
-}
-
 /** @brief Restore a region from a snapshot
  *
  *  @param reg     Target region
@@ -210,7 +198,7 @@ static void MC_get_memory_regions(simgrid::mc::Process* process, mc_snapshot_t s
 void MC_find_object_address(
   std::vector<simgrid::mc::VmMap> const& maps, simgrid::mc::ObjectInformation* result)
 {
-  const char* file_name = xbt_strdup(result->file_name.c_str());
+  char* file_name = xbt_strdup(result->file_name.c_str());
   const char *name = basename(file_name);
   for (size_t i = 0; i < maps.size(); ++i) {
     simgrid::mc::VmMap const& reg = maps[i];
@@ -258,6 +246,7 @@ void MC_find_object_address(
 
   xbt_assert(result->start_rw);
   xbt_assert(result->start_exec);
+  free(file_name);
 }
 
 /************************************* Take Snapshot ************************************/
@@ -486,7 +475,7 @@ static std::vector<s_mc_heap_ignore_region_t> MC_take_snapshot_ignore()
 
 static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
 {
-  xbt_assert(snapshot->process);
+  xbt_assert(snapshot->process());
   
   // Copy the memory:
   for (auto const& region : mc_model_checker->process().ignored_regions()) {
@@ -494,7 +483,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
     ignored_data.start = (void*)region.addr;
     ignored_data.data.resize(region.size);
     // TODO, we should do this once per privatization segment:
-    snapshot->process->read_bytes(
+    snapshot->process()->read_bytes(
       ignored_data.data.data(), region.size, remote(region.addr),
       simgrid::mc::ProcessIndexDisabled);
     snapshot->ignored_data.push_back(std::move(ignored_data));
@@ -502,7 +491,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
 
   // Zero the memory:
   for(auto const& region : mc_model_checker->process().ignored_regions()) {
-    snapshot->process->clear_bytes(remote(region.addr), region.size);
+    snapshot->process()->clear_bytes(remote(region.addr), region.size);
   }
 
 }
@@ -510,7 +499,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
 static void MC_snapshot_ignore_restore(mc_snapshot_t snapshot)
 {
   for (auto const& ignored_data : snapshot->ignored_data)
-    snapshot->process->write_bytes(
+    snapshot->process()->write_bytes(
       ignored_data.data.data(), ignored_data.data.size(),
       remote(ignored_data.start));
 }
@@ -600,9 +589,8 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 
   simgrid::mc::Process* mc_process = &mc_model_checker->process();
 
-  mc_snapshot_t snapshot = new simgrid::mc::Snapshot();
+  mc_snapshot_t snapshot = new simgrid::mc::Snapshot(mc_process);
 
-  snapshot->process = mc_process;
   snapshot->num_state = num_state;
 
   smx_process_t process;
@@ -626,7 +614,7 @@ mc_snapshot_t MC_take_snapshot(int num_state)
   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
     snapshot->stacks =
         MC_take_snapshot_stacks(&snapshot);
-    if (_sg_mc_hash && !snapshot->stacks.empty()) {
+    if (_sg_mc_hash) {
       snapshot->hash = simgrid::mc::hash(*snapshot);
     } else {
       snapshot->hash = 0;
diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp
index 6109240b25..5ed0cf3cd9 100644
--- a/src/mc/mc_client.cpp
+++ b/src/mc/mc_client.cpp
@@ -4,9 +4,8 @@
 /* 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 <stdlib.h>
-#include <errno.h>
-#include <error.h>
+#include <cstdlib>
+#include <cerrno>
 
 #include <sys/types.h>
 #include <sys/socket.h>
@@ -37,7 +36,7 @@ void MC_client_init(void)
     return;
   }
 
-  char* fd_env = getenv(MC_ENV_SOCKET_FD);
+  char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
   if (!fd_env)
     xbt_die("MC socket not found");
 
diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h
index 1a340df740..5b2215bcc1 100644
--- a/src/mc/mc_comm_pattern.h
+++ b/src/mc/mc_comm_pattern.h
@@ -7,7 +7,7 @@
 #ifndef SIMGRID_MC_COMM_PATTERN_H
 #define SIMGRID_MC_COMM_PATTERN_H
 
-#include <stdint.h>
+#include <stddef.h>
 
 #include <simgrid_config.h>
 #include <xbt/dynar.h>
diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 2d04cb8672..49ca9778e3 100644
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -16,6 +16,7 @@
 #include "mc_liveness.h"
 #include "mc_private.h"
 #include "mc_smx.h"
+#include "mc_dwarf.hpp"
 
 #include "mc/Frame.hpp"
 #include "mc/ObjectInformation.hpp"
@@ -236,7 +237,7 @@ static int compare_areas_with_type(struct mc_compare_state& state,
   }
   case DW_TAG_structure_type:
   case DW_TAG_class_type:
-    for(simgrid::mc::Type& member : type->members) {
+    for(simgrid::mc::Member& member : type->members) {
       void *member1 =
         mc_member_resolve(real_area1, type, &member, snapshot1, process_index);
       void *member2 =
@@ -247,7 +248,7 @@ static int compare_areas_with_type(struct mc_compare_state& state,
           compare_areas_with_type(state, process_index,
                                   member1, snapshot1, subregion1,
                                   member2, snapshot2, subregion2,
-                                  member.subtype, pointer_level);
+                                  member.type, pointer_level);
       if (res == 1)
         return res;
     }
diff --git a/src/mc/mc_diff.cpp b/src/mc/mc_diff.cpp
index 0887737206..c942bdd658 100644
--- a/src/mc/mc_diff.cpp
+++ b/src/mc/mc_diff.cpp
@@ -14,6 +14,7 @@
 #include "mc/datatypes.h"
 #include "mc/mc_private.h"
 #include "mc/mc_snapshot.h"
+#include "mc/mc_dwarf.hpp"
 #include "mc/Type.hpp"
 
 using simgrid::mc::remote;
@@ -26,119 +27,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
 xbt_dynar_t mc_heap_comparison_ignore;
 xbt_dynar_t stacks_areas;
 
-
-
-/********************************* Backtrace ***********************************/
-/******************************************************************************/
-
-static void mmalloc_backtrace_block_display(void *heapinfo, int block)
-{
-
-  /* xbt_ex_t e; */
-
-  /* if (((malloc_info *)heapinfo)[block].busy_block.bt_size == 0) { */
-  /*   fprintf(stderr, "No backtrace available for that block, sorry.\n"); */
-  /*   return; */
-  /* } */
-
-  /* memcpy(&e.bt,&(((malloc_info *)heapinfo)[block].busy_block.bt),sizeof(void*)*XBT_BACKTRACE_SIZE); */
-  /* e.used = ((malloc_info *)heapinfo)[block].busy_block.bt_size; */
-
-  /* xbt_ex_setup_backtrace(&e); */
-  /* if (e.used == 0) { */
-  /*   fprintf(stderr, "(backtrace not set)\n"); */
-  /* } else if (e.bt_strings == NULL) { */
-  /*   fprintf(stderr, "(backtrace not ready to be computed. %s)\n",xbt_binary_name?"Dunno why":"xbt_binary_name not setup yet"); */
-  /* } else { */
-  /*   int i; */
-
-  /*   fprintf(stderr, "Backtrace of where the block %d was malloced (%d frames):\n", block ,e.used); */
-  /*   for (i = 0; i < e.used; i++)       /\* no need to display "xbt_backtrace_display" *\/{ */
-  /*     fprintf(stderr, "%d ---> %s\n",i, e.bt_strings[i] + 4); */
-  /*   } */
-  /* } */
-}
-
-static void mmalloc_backtrace_fragment_display(void *heapinfo, int block,
-                                               int frag)
-{
-
-  /* xbt_ex_t e; */
-
-  /* memcpy(&e.bt,&(((malloc_info *)heapinfo)[block].busy_frag.bt[frag]),sizeof(void*)*XBT_BACKTRACE_SIZE); */
-  /* e.used = XBT_BACKTRACE_SIZE; */
-
-  /* xbt_ex_setup_backtrace(&e); */
-  /* if (e.used == 0) { */
-  /*   fprintf(stderr, "(backtrace not set)\n"); */
-  /* } else if (e.bt_strings == NULL) { */
-  /*   fprintf(stderr, "(backtrace not ready to be computed. %s)\n",xbt_binary_name?"Dunno why":"xbt_binary_name not setup yet"); */
-  /* } else { */
-  /*   int i; */
-
-  /*   fprintf(stderr, "Backtrace of where the fragment %d in block %d was malloced (%d frames):\n", frag, block ,e.used); */
-  /*   for (i = 0; i < e.used; i++)       /\* no need to display "xbt_backtrace_display" *\/{ */
-  /*     fprintf(stderr, "%d ---> %s\n",i, e.bt_strings[i] + 4); */
-  /*   } */
-  /* } */
-
-}
-
-static void mmalloc_backtrace_display(void *addr)
-{
-
-  /* size_t block, frag_nb; */
-  /* int type; */
-
-  /* block = (((char*) (addr) - (char*) heap -> heapbase) / BLOCKSIZE + 1); */
-
-  /* type = heap->heapinfo[block].type; */
-
-  /* switch(type){ */
-  /* case MMALLOC_TYPE_HEAPINFO :  */
-  /* case MMALLOC_TYPE_FREE : /\* Free block *\/ */
-  /*   fprintf(stderr, "Asked to display the backtrace of a block that is free. I'm puzzled\n"); */
-  /*   xbt_abort(); */
-  /*   break;  */
-  /* case 0: /\* Large block *\/ */
-  /*   mmalloc_backtrace_block_display(heap->heapinfo, block); */
-  /*   break; */
-  /* default: /\* Fragmented block *\/ */
-  /*   frag_nb = RESIDUAL(addr, BLOCKSIZE) >> type; */
-  /*   if(heap->heapinfo[block].busy_frag.frag_size[frag_nb] == -1){ */
-  /*     fprintf(stderr , "Asked to display the backtrace of a fragment that is free. I'm puzzled\n"); */
-  /*     xbt_abort(); */
-  /*   } */
-  /*   mmalloc_backtrace_fragment_display(heap->heapinfo, block, frag_nb); */
-  /*   break; */
-  /* } */
-}
-
-
-static int compare_backtrace(int b1, int f1, int b2, int f2)
-{
-  /*int i = 0;
-     if(f1 != -1){
-     for(i=0; i< XBT_BACKTRACE_SIZE; i++){
-     if(heapinfo1[b1].busy_frag.bt[f1][i] != heapinfo2[b2].busy_frag.bt[f2][i]){
-     //mmalloc_backtrace_fragment_display((void*)heapinfo1, b1, f1);
-     //mmalloc_backtrace_fragment_display((void*)heapinfo2, b2, f2);
-     return 1;
-     }
-     }
-     }else{
-     for(i=0; i< heapinfo1[b1].busy_block.bt_size; i++){
-     if(heapinfo1[b1].busy_block.bt[i] != heapinfo2[b2].busy_block.bt[i]){
-     //mmalloc_backtrace_block_display((void*)heapinfo1, b1);
-     //mmalloc_backtrace_block_display((void*)heapinfo2, b2);
-     return 1;
-     }
-     }
-     } */
-  return 0;
-}
-
-
 /*********************************** Heap comparison ***********************************/
 /***************************************************************************************/
 
@@ -461,7 +349,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   const malloc_info* heapinfos2 = snapshot2->read<malloc_info*>(
     (std::uint64_t)heapinfo_address, simgrid::mc::ProcessIndexMissing);
 
-  while (i1 <= state->heaplimit) {
+  while (i1 < state->heaplimit) {
 
     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
@@ -525,7 +413,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 
       }
 
-      while (i2 <= state->heaplimit && !equal) {
+      while (i2 < state->heaplimit && !equal) {
 
         addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
                        (char *) state->std_heap_copy.heapbase;
@@ -610,7 +498,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 
         }
 
-        while (i2 <= state->heaplimit && !equal) {
+        while (i2 < state->heaplimit && !equal) {
 
           const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
             heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
@@ -684,7 +572,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   /* All blocks/fragments are equal to another block/fragment ? */
   size_t i = 1, j = 0;
 
-  for(i = 1; i <= state->heaplimit; i++) {
+  for(i = 1; i < state->heaplimit; i++) {
     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
       heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {
@@ -726,7 +614,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   if (i1 == state->heaplimit)
     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 
-  for (i=1; i <= state->heaplimit; i++) {
+  for (i=1; i < state->heaplimit; i++) {
     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
       heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
     if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
@@ -1042,7 +930,7 @@ top:
         return -1;
       }
     } else {
-      for(simgrid::mc::Type& member : type->members) {
+      for(simgrid::mc::Member& member : type->members) {
         // TODO, optimize this? (for the offset case)
         void *real_member1 =
             mc_member_resolve(real_area1, type, &member, (simgrid::mc::AddressSpace*) snapshot1, process_index);
@@ -1051,7 +939,7 @@ top:
         res =
             compare_heap_area_with_type(state, process_index, real_member1, real_member2,
                                         snapshot1, snapshot2,
-                                        previous, member.subtype, -1,
+                                        previous, member.type, -1,
                                         check_ignore, 0);
         if (res == 1) {
           return res;
@@ -1103,18 +991,18 @@ static simgrid::mc::Type* get_offset_type(void *real_base_address, simgrid::mc::
       else
         return NULL;
     } else {
-      for(simgrid::mc::Type& member : type->members) {
+      for(simgrid::mc::Member& member : type->members) {
 
         if (member.has_offset_location()) {
           // We have the offset, use it directly (shortcut):
           if (member.offset() == offset)
-            return member.subtype;
+            return member.type;
         } else {
           void *real_member =
             mc_member_resolve(real_base_address, type, &member,
               snapshot, process_index);
           if ((char*) real_member - (char *) real_base_address == offset)
-            return member.subtype;
+            return member.type;
         }
 
       }
diff --git a/src/mc/mc_dwarf.cpp b/src/mc/mc_dwarf.cpp
index b806b0e00a..4d1aef5147 100644
--- a/src/mc/mc_dwarf.cpp
+++ b/src/mc/mc_dwarf.cpp
@@ -10,7 +10,7 @@
 #include <algorithm>
 #include <memory>
 
-#include <stdlib.h>
+#include <cstdlib>
 #define DW_LANG_Objc DW_LANG_ObjC       /* fix spelling error in older dwarf.h */
 #include <dwarf.h>
 #include <elfutils/libdw.h>
@@ -24,8 +24,8 @@
 
 #include "mc_object_info.h"
 #include "mc_private.h"
-#include "mc_process.h"
 
+#include "mc/Process.hpp"
 #include "mc/ObjectInformation.hpp"
 #include "mc/Variable.hpp"
 
@@ -475,8 +475,8 @@ static bool MC_compare_variable(
  *  \param  member the member of the type
  *  \param  child  DIE of the member (DW_TAG_member)
  */
-static void MC_dwarf_fill_member_location(simgrid::mc::Type* type, simgrid::mc::Type* member,
-                                          Dwarf_Die * child)
+static void MC_dwarf_fill_member_location(
+  simgrid::mc::Type* type, simgrid::mc::Member* member, Dwarf_Die * child)
 {
   if (dwarf_hasattr(child, DW_AT_data_bit_offset))
     xbt_die("Can't groke DW_AT_data_bit_offset.");
@@ -506,7 +506,7 @@ static void MC_dwarf_fill_member_location(simgrid::mc::Type* type, simgrid::mc::
             ("Could not read location expression DW_AT_data_member_location in DW_TAG_member %s of type <%"
              PRIx64 ">%s", MC_dwarf_attr_integrate_string(child, DW_AT_name),
              (uint64_t) type->id, type->name.c_str());
-      simgrid::mc::DwarfExpression(expr, expr+len);
+      member->location_expression = simgrid::mc::DwarfExpression(expr, expr+len);
       break;
     }
   case MC_DW_CLASS_CONSTANT:
@@ -561,18 +561,14 @@ static void MC_dwarf_add_members(simgrid::mc::ObjectInformation* info, Dwarf_Die
         continue;
 
       // TODO, we should use another type (because is is not a type but a member)
-      simgrid::mc::Type member;
-      member.type = tag;
-
-      // Global Offset:
-      member.id = dwarf_dieoffset(&child);
+      simgrid::mc::Member member;
+      member.inheritance = tag == DW_TAG_inheritance;
 
       const char *name = MC_dwarf_attr_integrate_string(&child, DW_AT_name);
       if (name)
         member.name = name;
       member.byte_size =
           MC_dwarf_attr_integrate_uint(&child, DW_AT_byte_size, 0);
-      member.element_count = -1;
       member.type_id = MC_dwarf_at_type(&child);
 
       if (dwarf_hasattr(&child, DW_AT_data_bit_offset))
@@ -1082,34 +1078,40 @@ static void mc_post_process_scope(simgrid::mc::ObjectInformation* info, simgrid:
 
 }
 
-/** \brief Fill/lookup the "subtype" field.
- */
-static void MC_resolve_subtype(simgrid::mc::ObjectInformation* info, simgrid::mc::Type* type)
+static
+simgrid::mc::Type* MC_resolve_type(
+  simgrid::mc::ObjectInformation* info, unsigned type_id)
 {
-  if (!type->type_id)
-    return;
-  type->subtype = simgrid::util::find_map_ptr(info->types, type->type_id);
-  if (type->subtype == nullptr)
-    return;
-  if (type->subtype->byte_size != 0)
-    return;
-  if (type->subtype->name.empty())
-    return;
+  if (!type_id)
+    return nullptr;
+  simgrid::mc::Type* type = simgrid::util::find_map_ptr(info->types, type_id);
+  if (type == nullptr)
+    return nullptr;
+
+  // We already have the information on the type:
+  if (type->byte_size != 0)
+    return type;
+
+  // Don't have a name, we can't find a more complete version:
+  if (type->name.empty())
+    return type;
+
   // Try to find a more complete description of the type:
   // We need to fix in order to support C++.
   simgrid::mc::Type** subtype = simgrid::util::find_map_ptr(
-    info->full_types_by_name, type->subtype->name);
+    info->full_types_by_name, type->name);
   if (subtype)
-    type->subtype = *subtype;
+    type = *subtype;
+  return type;
 }
 
 static void MC_post_process_types(simgrid::mc::ObjectInformation* info)
 {
   // Lookup "subtype" field:
   for(auto& i : info->types) {
-    MC_resolve_subtype(info, &(i.second));
-    for (simgrid::mc::Type& member : i.second.members)
-      MC_resolve_subtype(info, &member);
+    i.second.subtype = MC_resolve_type(info, i.second.type_id);
+    for (simgrid::mc::Member& member : i.second.members)
+      member.type = MC_resolve_type(info, member.type_id);
   }
 }
 
diff --git a/src/mc/mc_dwarf.hpp b/src/mc/mc_dwarf.hpp
index 192c68a69c..41d4841d7f 100644
--- a/src/mc/mc_dwarf.hpp
+++ b/src/mc/mc_dwarf.hpp
@@ -210,7 +210,7 @@ XBT_PRIVATE const char* MC_dwarf_attrname(int attr);
 XBT_PRIVATE const char* MC_dwarf_tagname(int tag);
 
 XBT_PRIVATE void* mc_member_resolve(
-  const void* base, simgrid::mc::Type* type, simgrid::mc::Type* member,
+  const void* base, simgrid::mc::Type* type, simgrid::mc::Member* member,
   simgrid::mc::AddressSpace* snapshot, int process_index);
 
 #endif
diff --git a/src/mc/mc_dwarf_expression.cpp b/src/mc/mc_dwarf_expression.cpp
index 7bf23355d3..cc9b6a6731 100644
--- a/src/mc/mc_dwarf_expression.cpp
+++ b/src/mc/mc_dwarf_expression.cpp
@@ -4,8 +4,8 @@
 /* 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 <stdint.h>
-#include <stdarg.h>
+#include <cstdint>
+#include <cstdarg>
 
 #include <dwarf.h>
 #include <elfutils/libdw.h>
@@ -107,7 +107,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
   for (size_t i = 0; i != n; ++i) {
     int error = 0;
     const Dwarf_Op *op = ops + i;
-    uint8_t atom = op->atom;
+    std::uint8_t atom = op->atom;
 
     switch (atom) {
 
@@ -181,7 +181,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       {
         if (!state->frame_base)
           return MC_EXPRESSION_E_MISSING_FRAME_BASE;
-        uintptr_t fb = ((uintptr_t) state->frame_base) + op->number;
+        std::uintptr_t fb = ((std::uintptr_t) state->frame_base) + op->number;
         error = mc_dwarf_push_value(state, fb);
         break;
       }
@@ -233,7 +233,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
         return MC_EXPRESSION_E_NO_BASE_ADDRESS;
       if (state->stack_size == MC_EXPRESSION_STACK_SIZE)
         return MC_EXPRESSION_E_STACK_OVERFLOW;
-      Dwarf_Off addr = (Dwarf_Off) (uintptr_t)
+      Dwarf_Off addr = (Dwarf_Off) (std::uintptr_t)
         state->object_info->base_address() + op->number;
       error = mc_dwarf_push_value(state, addr);
       break;
@@ -279,7 +279,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t temp = state->stack[state->stack_size - 2];
+        std::uintptr_t temp = state->stack[state->stack_size - 2];
         state->stack[state->stack_size - 2] =
             state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 1] = temp;
@@ -302,7 +302,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t result =
+        std::uintptr_t result =
             state->stack[state->stack_size - 2] +
             state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 2] = result;
@@ -314,7 +314,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t result =
+        std::uintptr_t result =
             state->stack[state->stack_size - 2] -
             state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 2] = result;
@@ -350,7 +350,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t result =
+        std::uintptr_t result =
             state->stack[state->stack_size - 2] -
             state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 2] = result;
@@ -362,7 +362,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t result =
+        std::uintptr_t result =
             state->stack[state->stack_size -
                          2] & state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 2] = result;
@@ -374,7 +374,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t result =
+        std::uintptr_t result =
             state->stack[state->stack_size -
                          2] | state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 2] = result;
@@ -386,7 +386,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
       if (state->stack_size < 2)
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
-        uintptr_t result =
+        std::uintptr_t result =
             state->stack[state->stack_size -
                          2] ^ state->stack[state->stack_size - 1];
         state->stack[state->stack_size - 2] = result;
@@ -407,7 +407,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
         return MC_EXPRESSION_E_STACK_UNDERFLOW;
       {
         // Computed address:
-        uintptr_t address = (uintptr_t) state->stack[state->stack_size - 1];
+        std::uintptr_t address = (std::uintptr_t) state->stack[state->stack_size - 1];
         if (!state->address_space)
           xbt_die("Missing address space");
         state->address_space->read_bytes(
@@ -546,10 +546,10 @@ void mc_dwarf_location_list_init(
 {
   list->clear();
 
-  ptrdiff_t offset = 0;
+  std::ptrdiff_t offset = 0;
   Dwarf_Addr base, start, end;
   Dwarf_Op *ops;
-  size_t len;
+  std::size_t len;
 
   while (1) {
 
diff --git a/src/mc/mc_forward.hpp b/src/mc/mc_forward.hpp
index f3b032bc83..5c704d495e 100644
--- a/src/mc/mc_forward.hpp
+++ b/src/mc/mc_forward.hpp
@@ -21,6 +21,7 @@ class AddressSpace;
 class Process;
 class Snapshot;
 class ObjectInformation;
+class Member;
 class Type;
 class Variable;
 class Frame;
diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index d9680d80be..ccda078138 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -6,9 +6,10 @@
 
 #include <cinttypes>
 
-#include <assert.h>
-#include <string.h>
-#include <stdint.h>
+#include <cassert>
+#include <cstddef>
+#include <cstdint>
+#include <cstring>
 
 #include "mc_base.h"
 
@@ -542,7 +543,7 @@ void MC_dump_stacks(FILE* file)
       unw_get_reg(&c, UNW_X86_64_RIP, &rip);
       unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
       fprintf(file, "  %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
-        nframe, name, rip, rsp);
+        nframe, name, (std::uint64_t) rip, (std::uint64_t) rsp);
 #else
       fprintf(file, "  %i: %s\n", nframe, name);
 #endif
diff --git a/src/mc/mc_hash.cpp b/src/mc/mc_hash.cpp
index eac6cc933f..7a0249db13 100644
--- a/src/mc/mc_hash.cpp
+++ b/src/mc/mc_hash.cpp
@@ -6,352 +6,47 @@
 
 #include <cinttypes>
 
-#include <stdint.h>
-#include <stdbool.h>
+#include <cstdint>
 
 #include "mc_private.h"
 #include "mc/datatypes.h"
-#include <mc/mc.h>
 #include "mc_hash.hpp"
+#include <mc/mc.h>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_hash, mc, "Logging specific to mc_hash");
 
 namespace simgrid {
 namespace mc {
 
-// This is djb2:
-#define MC_HASH_INIT ((simgrid::mc::hash_type)5381)
-
-template<class T>
-static void hash_update(hash_type& hash, T const& value)
-{
-  hash = (hash << 5) + hash + (uint64_t) value;
-}
-
-// ***** Hash state
-
-#if 0
-typedef struct s_mc_hashing_state {
-  // Set of pointers/addresses already processed (avoid loops):
-  mc_address_set_t handled_addresses;
-} mc_hashing_state;
-
-void mc_hash_state_init(mc_hashing_state * state);
-void mc_hash_state_destroy(mc_hashing_state * state);
-
-void mc_hash_state_init(mc_hashing_state * state)
-{
-  state->handled_addresses = mc_address_set_new();
-}
+namespace {
 
-void mc_hash_state_destroy(mc_hashing_state * state)
-{
-  mc_address_set_free(&state->handled_addresses);
-}
-
-// TODO, detect and avoid loops
-
-static bool mc_ignored(const void *address, size_t size)
-{
-  mc_heap_ignore_region_t region;
-  unsigned int cursor = 0;
-  const void *end = (char *) address + size;
-  xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, region) {
-    void *istart = region->address;
-    void *iend = (char *) region->address + region->size;
-
-    if (address >= istart && address < iend && end >= istart && end < iend)
-      return true;
+class djb_hash {
+  hash_type state_ = 5381ll;
+public:
+  template<class T>
+  void update(T& x)
+  {
+    state_ = (state_ << 5) + state_ + (std::uint64_t) value;
   }
-
-  return false;
-}
-
-static void mc_hash_binary(hash_type * hash, const void *s, size_t len)
-{
-  const char *p = (const char*) s;
-  for (size_t i = 0; i != len; ++i) {
-    hash_update(*hash, p[i]);
+  hash_type value()
+  {
+    return state_;
   }
-}
-
-/** \brief Compute a hash for a given value of a given type
- *
- *  We try to be very conservative (do not hash too ambiguous things).
- *
- *  \param address address of the variable
- *  \param type type of the variable
- * */
-static void mc_hash_value(hash_type * hash, mc_hashing_state * state,
-                          simgrid::mc::ObjectInformation* info, const void *address,
-                          simgrid::mc::Type* type)
-{
-  simgrid::mc::Process* process = &mc_model_checker->process();
-top:
-
-  switch (type->type) {
-
-    // Not relevant, do nothing:
-  case DW_TAG_unspecified_type:
-    return;
-
-    // Simple case, hash this has binary:
-  case DW_TAG_base_type:
-  case DW_TAG_enumeration_type:
-    {
-      if (mc_ignored(address, 1))
-        return;
-      mc_hash_binary(hash, address, type->byte_size);
-      return;
-    }
-
-  case DW_TAG_array_type:
-    {
-      if (mc_ignored(address, type->byte_size))
-        return;
-
-      long element_count = type->element_count;
-      simgrid::mc::Type* subtype = type->subtype;
-      if (subtype == NULL) {
-        XBT_DEBUG("Hash array without subtype");
-        return;
-      }
-      int i;
-      for (i = 0; i != element_count; ++i) {
-        XBT_DEBUG("Hash array element %i", i);
-        void *subaddress = ((char *) address) + i * subtype->byte_size;
-        mc_hash_value(hash, state, info, subaddress, subtype);
-      }
-      return;
-    }
-
-    // Get the raw type:
-  case DW_TAG_typedef:
-  case DW_TAG_volatile_type:
-  case DW_TAG_const_type:
-  case DW_TAG_restrict_type:
-    {
-      type = type->subtype;
-      if (type == NULL)
-        return;
-      else
-        goto top;
-    }
-
-  case DW_TAG_structure_type:
-  case DW_TAG_class_type:
-    {
-      if (mc_ignored(address, type->byte_size))
-        return;
-
-      unsigned int cursor = 0;
-      simgrid::mc::Type* member;
-      xbt_dynar_foreach(type->members, cursor, member) {
-        XBT_DEBUG("Hash struct member %s", member->name);
-        if (type->subtype == NULL)
-          return;
-        void *member_variable = mc_member_resolve(address, type, member, NULL);
-        mc_hash_value(hash, state, info, member_variable, type->subtype);
-      }
-      return;
-    }
-
-    // Pointer, we hash a single value but it might be an array.
-  case DW_TAG_pointer_type:
-  case DW_TAG_reference_type:
-  case DW_TAG_rvalue_reference_type:
-    {
-      if (mc_ignored(address, 1))
-        return;
-
-      void *pointed = *(void **) address;
-      if (pointed == NULL) {
-        XBT_DEBUG("Hashed pinter is NULL");
-        return;
-      }
-      // Avoid loops:
-      if (mc_address_test(state->handled_addresses, pointed)) {
-        XBT_DEBUG("Hashed pointed data %p already hashed", pointed);
-        return;
-      }
-      mc_address_add(state->handled_addresses, pointed);
-
-      // Anything outside the R/W segments and the heap is not hashed:
-      bool valid_pointer = (pointed >= (void *) binary_info->start_rw
-                            && pointed <= (void *) binary_info->end_rw)
-          || (pointed >= (void *) libsimgrid_info->start_rw
-              && pointed <= (void *) libsimgrid_info->end_rw)
-          || (pointed >= process->heap_address
-              && pointed < (void *) ((const char *) process->heap_address + STD_HEAP_SIZE));
-      if (!valid_pointer) {
-        XBT_DEBUG("Hashed pointed data %p is in an ignored range", pointed);
-        return;
-      }
-
-      if (type->subtype == NULL) {
-        XBT_DEBUG("Missing type for %p (type=%s)",
-          pointed, type->type_id.c_str());
-        return;
-      }
-
-      address = pointed;
-      type = type->subtype;
-      goto top;
-    }
-
-    // Skip this:
-  case DW_TAG_union_type:
-  case DW_TAG_subroutine_type:
-  default:
-    return;
-  }
-}
-
-static void mc_hash_object_globals(hash_type * hash, mc_hashing_state * state,
-                                   simgrid::mc::ObjectInformation* info)
-{
-  unsigned int cursor = 0;
-  simgrid::mc::Variable* variable;
-  xbt_dynar_foreach(info->global_variables, cursor, variable) {
-    XBT_DEBUG("Hash global variable %s", variable->name);
-
-    if (variable->type_id == NULL) {
-      // Nothing
-      continue;
-    }
-
-    simgrid::mc::Type* type = variable->type;
-    if (type == NULL) {
-      // Nothing
-      continue;
-    }
-
-    const char *address = variable->address;
-    bool valid_pointer = (address >= binary_info->start_rw
-                          && address <= binary_info->end_rw)
-        || (address >= libsimgrid_info->start_rw
-            && address <= libsimgrid_info->end_rw)
-        || (address >= (const char *) process->heap_address
-            && address < (const char *) process->heap_address + STD_HEAP_SIZE);
-    if (!valid_pointer)
-      continue;
-
-    mc_hash_value(hash, state, info, variable->address, type);
-  }
-}
-
-static void mc_hash_stack_frame(mc_hash_t * hash,
-                                simgrid::mc::ObjectInformation* info,
-                                unw_cursor_t * unw_cursor, simgrid::mc::Frame* frame,
-                                char *frame_pointer, mc_hashing_state * state)
-{
-
-  // return; // TEMP
-
-  unsigned int cursor = 0;
-  simgrid::mc::Variable* variable;
-  xbt_dynar_foreach(frame->variables, cursor, variable) {
-
-    if (variable->type_id == NULL) {
-      XBT_DEBUG("Hash local variable %s without type", variable->name);
-      continue;
-    }
-    if (variable->locations.size == 0) {
-      XBT_DEBUG("Hash local variable %s without location", variable->name);
-      continue;
-    }
-
-    XBT_DEBUG("Hash local variable %s", variable->name);
-
-    void *variable_address =
-        (void *) mc_dwarf_resolve_locations(&variable->locations,
-                                            variable->object_info, unw_cursor,
-                                            frame_pointer, NULL);
-
-    simgrid::mc::Type* type = variable->type;
-    if (type == NULL) {
-      XBT_DEBUG("Hash local variable %s without loctypeation", variable->name);
-      continue;
-    }
-
-    mc_hash_value(hash, state, info, variable_address, type);
-  }
-
-  // TODO, handle nested scopes
-}
-
-static void mc_hash_stack(mc_hash_t * hash, mc_snapshot_stack_t stack,
-                          mc_hashing_state * state)
-{
-
-  unsigned cursor = 0;
-  mc_stack_frame_t stack_frame;
-
-  for(s_mc_stack_frame_t const& stack_frame : stack->stack_frames) {
-
-    hash_update(*hash, stack_frame.ip);
-
-    simgrid::mc::ObjectInformation* info;
-    if (stack_frame.ip >= (unw_word_t) libsimgrid_info->start_exec
-        && stack_frame.ip < (unw_word_t) libsimgrid_info->end_exec)
-      info = libsimgrid_info;
-    else if (stack_frame.ip >= (unw_word_t) binary_info->start_exec
-             && stack_frame.ip < (unw_word_t) binary_info->end_exec)
-      info = binary_info;
-    else
-      continue;
-
-    mc_hash_stack_frame(hash, info, &(stack_frame.unw_cursor),
-                        stack_frame.frame, (void *) stack_frame.frame_base,
-                        state);
-
-  }
-}
-
-static void mc_hash_stacks(mc_hash_t * hash, mc_hashing_state * state,
-                           xbt_dynar_t stacks)
-{
-  unsigned int cursor = 0;
-  mc_snapshot_stack_t current_stack;
-
-  hash_update(*hash, xbt_dynar_length(stacks_areas));
-
-  int i = 0;
-  xbt_dynar_foreach(stacks, cursor, current_stack) {
-    XBT_DEBUG("Stack %i", i);
-    mc_hash_stack(hash, current_stack, state);
-    ++i;
-  }
-}
-#endif
-
-static hash_type hash(std::vector<s_mc_snapshot_stack_t> const& stacks)
-{
-#if 0
-  mc_hashing_state state;
-  mc_hash_state_init(&state);
-#endif
-
-  hash_type hash = MC_HASH_INIT;
-
-  hash_update(hash, xbt_swag_size(simix_global->process_list));
-#if 0
-  // mc_hash_object_globals(&hash, &state, binary_info);
-  // mc_hash_object_globals(&hash, &state, libsimgrid_info);
-  // mc_hash_stacks(&hash, &state, stacks);
-  mc_hash_state_destroy(&state);
-#endif
-
+};
 
-  return hash;
 }
 
 hash_type hash(Snapshot const& snapshot)
 {
   XBT_DEBUG("START hash %i", snapshot.num_state);
-  hash_type res = simgrid::mc::hash(snapshot.stacks);
+  djb_hash hash;
+  // TODO, nb_processes
+  // TODO, heap_bytes_used
+  // TODO, root variables
+  // TODO, basic stack frame information
+  // TODO, stack frame local variables
   XBT_DEBUG("END hash %i", snapshot.num_state);
-  return res;
+  return hash.value();
 }
 
 }
diff --git a/src/mc/mc_hash.hpp b/src/mc/mc_hash.hpp
index 67505c5da0..4a8dd6ab5c 100644
--- a/src/mc/mc_hash.hpp
+++ b/src/mc/mc_hash.hpp
@@ -17,6 +17,7 @@ namespace simgrid {
 namespace mc {
 
 typedef std::uint64_t hash_type;
+
 XBT_PRIVATE hash_type hash(simgrid::mc::Snapshot const& snapshot);
 
 }
diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h
index f789493124..a9b134de13 100644
--- a/src/mc/mc_ignore.h
+++ b/src/mc/mc_ignore.h
@@ -10,7 +10,7 @@
 #include <xbt/dynar.h>
 
 #include "mc/datatypes.h"
-#include "mc_process.h"
+#include "mc/Process.hpp"
 
 #include "xbt/misc.h"           /* SG_BEGIN_DECL */
 
diff --git a/src/mc/mc_member.cpp b/src/mc/mc_member.cpp
index 29fe1f5193..2dc276b690 100644
--- a/src/mc/mc_member.cpp
+++ b/src/mc/mc_member.cpp
@@ -18,8 +18,9 @@
  * @param snapshot Snapshot (or NULL)
  * @return Process address of the given member of the 'object' struct/class
  */
-void *mc_member_resolve(const void *base, simgrid::mc::Type* type, simgrid::mc::Type* member,
-                        simgrid::mc::AddressSpace* address_space, int process_index)
+void *mc_member_resolve(
+    const void *base, simgrid::mc::Type* type, simgrid::mc::Member* member,
+    simgrid::mc::AddressSpace* address_space, int process_index)
 {
   // TODO, get rid of this?
   if (!member->has_offset_location())
diff --git a/src/mc/mc_object_info.h b/src/mc/mc_object_info.h
index 1da12e81a6..019c758ece 100644
--- a/src/mc/mc_object_info.h
+++ b/src/mc/mc_object_info.h
@@ -25,8 +25,4 @@ XBT_PRIVATE  void MC_dwarf_get_variables_libdw(simgrid::mc::ObjectInformation* i
 XBT_PRIVATE  const char* MC_dwarf_attrname(int attr);
 XBT_PRIVATE  const char* MC_dwarf_tagname(int tag);
 
-XBT_PRIVATE  void* mc_member_resolve(
-  const void* base, simgrid::mc::Type* type, simgrid::mc::Type* member,
-  simgrid::mc::AddressSpace* snapshot, int process_index);
-
 #endif
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index f88c5c4414..bbd2a64823 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -118,8 +118,6 @@ XBT_PRIVATE void MC_report_assertion_error(void);
 
 XBT_PRIVATE void MC_invalidate_cache(void);
 
-XBT_PRIVATE int MC_important_snapshot(mc_snapshot_t snapshot);
-
 SG_END_DECL()
 
 #endif
diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index d6f1097f86..53fe65421c 100644
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -4,8 +4,9 @@
 /* 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 <stdio.h>
-#include <stdlib.h>
+#include <cstring>
+#include <cstdio>
+#include <cstdlib>
 
 #include <xbt.h>
 #include <simgrid/simix.h>
@@ -26,9 +27,9 @@ extern "C" {
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
   " Logging specific to MC record/replay facility");
 
-char* MC_record_path = NULL;
+char* MC_record_path = nullptr;
 
-void MC_record_replay(mc_record_item_t start, size_t len)
+void MC_record_replay(mc_record_item_t start, std::size_t len)
 {
   MC_wait_for_requests();
   mc_record_item_t end = start + len;
@@ -62,9 +63,9 @@ xbt_dynar_t MC_record_from_string(const char* data)
 {
   XBT_INFO("path=%s", data);
   if (!data || !data[0])
-    return NULL;
+    return nullptr;
 
-  xbt_dynar_t dynar = xbt_dynar_new(sizeof(s_mc_record_item_t), NULL);
+  xbt_dynar_t dynar = xbt_dynar_new(sizeof(s_mc_record_item_t), nullptr);
 
   const char* current = data;
   while (*current) {
@@ -76,8 +77,8 @@ xbt_dynar_t MC_record_from_string(const char* data)
     xbt_dynar_push(dynar, &item);
 
     // Find next chunk:
-    const char* end = strchr(current, ';');
-    if(end==NULL)
+    const char* end = std::strchr(current, ';');
+    if(end == nullptr)
       break;
     else
       current = end + 1;
@@ -87,15 +88,15 @@ xbt_dynar_t MC_record_from_string(const char* data)
 
 fail:
   xbt_dynar_free(&dynar);
-  return NULL;
+  return nullptr;
 }
 
 #ifdef HAVE_MC
 static char* MC_record_stack_to_string_liveness(xbt_fifo_t stack)
 {
   char* buffer;
-  size_t size;
-  FILE* file = open_memstream(&buffer, &size);
+  std::size_t size;
+  std::FILE* file = open_memstream(&buffer, &size);
 
   xbt_fifo_item_t item;
   xbt_fifo_item_t start = xbt_fifo_get_last_item(stack);
@@ -110,13 +111,13 @@ static char* MC_record_stack_to_string_liveness(xbt_fifo_t stack)
       // Serialization the (pid, value) pair:
       const char* sep = (item!=start) ? ";" : "";
       if (value)
-        fprintf(file, "%s%u/%u", sep, pid, value);
+        std::fprintf(file, "%s%u/%u", sep, pid, value);
       else
-        fprintf(file, "%s%u", sep, pid);
+        std::fprintf(file, "%s%u", sep, pid);
     }
   }
 
-  fclose(file);
+  std::fclose(file);
   return buffer;
 }
 
@@ -134,8 +135,8 @@ char* MC_record_stack_to_string(xbt_fifo_t stack)
   }
 
   char* buffer;
-  size_t size;
-  FILE* file = open_memstream(&buffer, &size);
+  std::size_t size;
+  std::FILE* file = open_memstream(&buffer, &size);
 
   xbt_fifo_item_t item;
   for (item = start; item; item = xbt_fifo_get_prev_item(item)) {
@@ -150,12 +151,12 @@ char* MC_record_stack_to_string(xbt_fifo_t stack)
     // Serialization the (pid, value) pair:
     const char* sep = (item!=start) ? ";" : "";
     if (value)
-      fprintf(file, "%s%u/%u", sep, pid, value);
+      std::fprintf(file, "%s%u/%u", sep, pid, value);
     else
-      fprintf(file, "%s%u", sep, pid);
+      std::fprintf(file, "%s%u", sep, pid);
   }
 
-  fclose(file);
+  std::fclose(file);
   return buffer;
 }
 
@@ -164,7 +165,7 @@ void MC_record_dump_path(xbt_fifo_t stack)
   if (MC_record_is_active()) {
     char* path = MC_record_stack_to_string(stack);
     XBT_INFO("Path = %s", path);
-    free(path);
+    std::free(path);
   }
 }
 #endif
diff --git a/src/mc/mc_server.h b/src/mc/mc_server.h
index a620d17383..f5457e174c 100644
--- a/src/mc/mc_server.h
+++ b/src/mc/mc_server.h
@@ -9,7 +9,6 @@
 
 #include <poll.h>
 
-#include <stdint.h>
 #include <stdbool.h>
 
 #include <sys/signalfd.h>
@@ -18,7 +17,7 @@
 #include <xbt/misc.h>
 #include <xbt/base.h>
  
-#include "mc_process.h"
+#include "mc/Process.hpp"
 #include "mc_exit.h"
 
 SG_BEGIN_DECL()
diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index 7b760772c2..7ef07f57fe 100644
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -87,7 +87,6 @@ static void MC_process_refresh_simix_process_list(
 void MC_process_smx_refresh(simgrid::mc::Process* process)
 {
   xbt_assert(mc_mode == MC_MODE_SERVER);
-  xbt_assert(!process->is_self());
   if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
     return;
 
diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h
index 887249816a..827634d150 100644
--- a/src/mc/mc_smx.h
+++ b/src/mc/mc_smx.h
@@ -14,7 +14,7 @@
 
 #include "smpi/private.h"
 
-#include "mc_process.h"
+#include "mc/Process.hpp"
 #include "mc_protocol.h"
 
 /** @file
@@ -49,6 +49,8 @@ struct s_mc_smx_process_info {
   char* name;
 };
 
+typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
+
 XBT_PRIVATE xbt_dynar_t MC_smx_process_info_list_new(void);
 
 XBT_PRIVATE void MC_process_smx_refresh(simgrid::mc::Process* process);
diff --git a/src/mc/mc_snapshot.cpp b/src/mc/mc_snapshot.cpp
index c4662eccfd..324c6eae15 100644
--- a/src/mc/mc_snapshot.cpp
+++ b/src/mc/mc_snapshot.cpp
@@ -153,8 +153,8 @@ int MC_snapshot_memcmp(
 namespace simgrid {
 namespace mc {
 
-Snapshot::Snapshot() :
-  process(nullptr),
+Snapshot::Snapshot(Process* process) :
+  AddressSpace(process),
   num_state(0),
   heap_bytes_used(0),
   enabled_processes(),
diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h
index 72965f4c67..cf2dc5aecb 100644
--- a/src/mc/mc_snapshot.h
+++ b/src/mc/mc_snapshot.h
@@ -140,15 +140,14 @@ typedef struct s_mc_global_t {
 namespace simgrid {
 namespace mc {
 
-class XBT_PRIVATE Snapshot : public AddressSpace {
+class XBT_PRIVATE Snapshot final : public AddressSpace {
 public:
-  Snapshot();
+  Snapshot(Process* process);
   ~Snapshot();
   const void* read_bytes(void* buffer, std::size_t size,
     remote_ptr<void> address, int process_index = ProcessIndexAny,
     ReadMode mode = Normal) const override;
 public: // To be private
-  simgrid::mc::Process* process;
   int num_state;
   size_t heap_bytes_used;
   std::vector<std::unique_ptr<s_mc_mem_region_t>> snapshot_regions;
diff --git a/src/mc/mc_unw.cpp b/src/mc/mc_unw.cpp
index 899b4039e2..c53785000c 100644
--- a/src/mc/mc_unw.cpp
+++ b/src/mc/mc_unw.cpp
@@ -19,7 +19,7 @@
 #include <libunwind.h>
 
 #include "mc_object_info.h"
-#include "mc_process.h"
+#include "mc/Process.hpp"
 #include "mc_unw.h"
 #include "mc/Frame.hpp"
 
@@ -224,12 +224,6 @@ int mc_unw_init_cursor(unw_cursor_t *cursor, mc_unw_context_t context)
 {
   if (!context->process || !context->address_space)
     return -UNW_EUNSPEC;
-  simgrid::mc::AddressSpace* as = context->address_space;
-
-  simgrid::mc::Process* process = dynamic_cast<simgrid::mc::Process*>(as);
-  if (process && process->is_self())
-    return unw_init_local(cursor, &context->context);
-
   return unw_init_remote(cursor, context->process->unw_addr_space, context);
 }
 
diff --git a/src/mc/mc_unw.h b/src/mc/mc_unw.h
index 1a22b84376..915c445324 100644
--- a/src/mc/mc_unw.h
+++ b/src/mc/mc_unw.h
@@ -28,7 +28,7 @@
 
 #include <xbt/base.h>
 
-#include "mc_process.h"
+#include "mc/Process.hpp"
 
 SG_BEGIN_DECL()
 
diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 104576b93e..40db5aad8a 100644
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -11,7 +11,7 @@
 #include "mc_safety.h"
 #include "mc_liveness.h"
 #include "mc_private.h"
-#include "mc_process.h"
+#include "mc/Process.hpp"
 #include "mc_smx.h"
 
 extern "C" {
@@ -60,13 +60,9 @@ static mc_visited_state_t visited_state_new()
     process->get_heap()->heaplimit,
     process->get_malloc_info());
 
-  if (mc_model_checker->process().is_self()) {
-    new_state->nb_processes = xbt_swag_size(simix_global->process_list);
-  } else {
-    MC_process_smx_refresh(&mc_model_checker->process());
-    new_state->nb_processes = xbt_dynar_length(
-      mc_model_checker->process().smx_process_infos);
-  }
+  MC_process_smx_refresh(&mc_model_checker->process());
+  new_state->nb_processes = xbt_dynar_length(
+    mc_model_checker->process().smx_process_infos);
 
   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
   new_state->num = mc_stats->expanded_states;
@@ -85,13 +81,11 @@ 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(
     process->get_heap()->heaplimit,
     process->get_malloc_info());
-  if (mc_model_checker->process().is_self()) {
-    pair->nb_processes = xbt_swag_size(simix_global->process_list);
-  } else {
-    MC_process_smx_refresh(&mc_model_checker->process());
-    pair->nb_processes = xbt_dynar_length(
-      mc_model_checker->process().smx_process_infos);
-  }
+
+  MC_process_smx_refresh(&mc_model_checker->process());
+  pair->nb_processes = xbt_dynar_length(
+    mc_model_checker->process().smx_process_infos);
+
   pair->automaton_state = automaton_state;
   pair->num = pair_num;
   pair->other_num = -1;
@@ -222,6 +216,45 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
   return cursor;
 }
 
+static
+void replace_state(
+  mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor)
+{
+  if (state_test->other_num == -1)
+    new_state->other_num = state_test->num;
+  else
+    new_state->other_num = state_test->other_num;
+
+  if (dot_output == NULL)
+    XBT_DEBUG("State %d already visited ! (equal to state %d)",
+      new_state->num, state_test->num);
+  else
+    XBT_DEBUG(
+      "State %d already visited ! (equal to state %d (state %d in dot_output))",
+      new_state->num, state_test->num, new_state->other_num);
+
+  /* Replace the old state with the new one (with a bigger num)
+     (when the max number of visited states is reached,  the oldest
+     one is removed according to its number (= with the min number) */
+  xbt_dynar_remove_at(visited_states, cursor, NULL);
+  xbt_dynar_insert_at(visited_states, cursor, &new_state);
+  XBT_DEBUG("Replace visited state %d with the new visited state %d",
+    state_test->num, new_state->num);
+}
+
+static
+bool some_dommunications_are_not_finished()
+{
+  for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
+    xbt_dynar_t pattern = xbt_dynar_get_as(
+      incomplete_communications_pattern, current_process, xbt_dynar_t);
+    if (!xbt_dynar_is_empty(pattern)) {
+      XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
+      return true;
+    }
+  }
+  return false;
+}
 
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
@@ -233,22 +266,11 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   if (_sg_mc_visited == 0)
     return NULL;
 
-  int partial_comm = 0;
-
   /* If comm determinism verification, we cannot stop the exploration if some 
      communications are not finished (at least, data are transfered). These communications 
      are incomplete and they cannot be analyzed and compared with the initial pattern. */
-  if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    size_t current_process = 1;
-    while (current_process < MC_smx_get_maxpid()) {
-      if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
-        XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
-        partial_comm = 1;
-        break;
-      }
-      current_process++;
-    }
-  }
+  int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
+    some_dommunications_are_not_finished();
 
   mc_visited_state_t new_state = visited_state_new();
   graph_state->system_state = new_state->system_state;
@@ -263,9 +285,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   } else {
 
     int min = -1, max = -1, index;
-    //int res;
-    mc_visited_state_t state_test;
-    int cursor;
 
     index = get_search_interval(visited_states, new_state, &min, &max);
 
@@ -274,7 +293,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       // Parallell implementation
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
          if(res != -1){
-         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
+         mc_visited_state_t state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
          if(state_test->other_num == -1)
          new_state->other_num = state_test->num;
          else
@@ -291,28 +310,13 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       if (_sg_mc_safety || (!partial_comm
         && initial_global_state->initial_communications_pattern_done)) {
 
-        cursor = min;
+        int cursor = min;
         while (cursor <= max) {
-          state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
+          mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
           if (snapshot_compare(state_test, new_state) == 0) {
             // The state has been visited:
 
-            if (state_test->other_num == -1)
-              new_state->other_num = state_test->num;
-            else
-              new_state->other_num = state_test->other_num;
-            if (dot_output == NULL)
-              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
-            else
-              XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
-
-            /* Replace the old state with the new one (with a bigger num) 
-               (when the max number of visited states is reached,  the oldest 
-               one is removed according to its number (= with the min number) */
-            xbt_dynar_remove_at(visited_states, cursor, NULL);
-            xbt_dynar_insert_at(visited_states, cursor, &new_state);
-            XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
-
+            replace_state(state_test, new_state, cursor);
             return state_test;
           }
           cursor++;
@@ -325,7 +329,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
     } else {
 
       // The state has not been visited: insert the state in the dynamic array.
-      state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
+      mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
       if (state_test->nb_processes < new_state->nb_processes) {
         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
       } else {
@@ -348,8 +352,11 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       int min2 = mc_stats->expanded_states;
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
+
+      mc_visited_state_t state_test;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
-        if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) {
+        if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
+            && state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
@@ -466,7 +473,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)
+        if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
             && pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;
diff --git a/src/mc/mcer_ignore.h b/src/mc/mcer_ignore.h
index db3840038e..d5f5529877 100644
--- a/src/mc/mcer_ignore.h
+++ b/src/mc/mcer_ignore.h
@@ -10,7 +10,7 @@
 #include <xbt/dynar.h>
 
 #include "mc/datatypes.h"
-#include "mc/mc_process.h"
+#include "mc/Process.hpp"
 
 #include "xbt/misc.h"           /* SG_BEGIN_DECL */
 
diff --git a/src/smpi/smpi_global.c b/src/smpi/smpi_global.c
index 61a34379b5..263b191439 100644
--- a/src/smpi/smpi_global.c
+++ b/src/smpi/smpi_global.c
@@ -676,7 +676,7 @@ int smpi_main(int (*realmain) (int argc, char *argv[]), int argc, char *argv[])
     xbt_os_walltimer_stop(global_timer);
     if (sg_cfg_get_boolean("smpi/display_timing")){
       double global_time = xbt_os_timer_elapsed(global_timer);
-      XBT_INFO("Simulated time: %g seconds. \n "
+      XBT_INFO("Simulated time: %g seconds. \n\n"
           "The simulation took %g seconds (after parsing and platform setup)\n"
           "%g seconds were actual computation of the application"
           , SIMIX_get_clock(), global_time , smpi_total_benched_time);
diff --git a/src/xbt/mmalloc/mm_module.c b/src/xbt/mmalloc/mm_module.c
index 8490906407..621ff10e5c 100644
--- a/src/xbt/mmalloc/mm_module.c
+++ b/src/xbt/mmalloc/mm_module.c
@@ -359,7 +359,7 @@ void mmalloc_postexit(void)
 size_t mmalloc_get_bytes_used_remote(size_t heaplimit, const malloc_info* heapinfo)
 {
   int bytes = 0;
-  for (size_t i=0; i<=heaplimit; ++i){
+  for (size_t i=0; i < heaplimit; ++i){
     if (heapinfo[i].type == MMALLOC_TYPE_UNFRAGMENTED){
       if (heapinfo[i].busy_block.busy_size > 0)
         bytes += heapinfo[i].busy_block.busy_size;
diff --git a/teshsuite/mc/dwarf/dwarf.cpp b/teshsuite/mc/dwarf/dwarf.cpp
index ee7138cfaa..91693d3853 100644
--- a/teshsuite/mc/dwarf/dwarf.cpp
+++ b/teshsuite/mc/dwarf/dwarf.cpp
@@ -17,8 +17,8 @@
 #include "mc/datatypes.h"
 #include "mc/mc_object_info.h"
 #include "mc/mc_private.h"
-#include "mc/mc_process.h"
 
+#include "mc/Process.hpp"
 #include "mc/Type.hpp"
 #include "mc/ObjectInformation.hpp"
 #include "mc/Variable.hpp"
@@ -100,9 +100,9 @@ static simgrid::mc::Variable* test_global_variable(simgrid::mc::Process* process
   return variable;
 }
 
-static simgrid::mc::Type* find_member(simgrid::mc::ObjectInformation* info, const char* name, simgrid::mc::Type* type)
+static simgrid::mc::Member* find_member(simgrid::mc::Type& type, const char* name)
 {
-  for (simgrid::mc::Type& member : type->members)
+  for (simgrid::mc::Member& member : type.members)
     if(member.name == name)
       return &member;
   return nullptr;
@@ -146,8 +146,10 @@ int main(int argc, char** argv)
   i = process->binary_info->types.find(var->type_id);
   xbt_assert(i != process->binary_info->types.end(), "Missing type");
   type = &i->second;
-  assert(find_member(process->binary_info.get(), "first", type)->offset() == 0);
-  assert(find_member(process->binary_info.get(), "second", type)->offset()
+
+  assert(type);
+  assert(find_member(*type, "first")->offset() == 0);
+  assert(find_member(*type, "second")->offset()
       == ((const char*)&test_some_struct.second) - (const char*)&test_some_struct);
 
   unw_context_t context;
diff --git a/teshsuite/mc/dwarf_expression/dwarf_expression.cpp b/teshsuite/mc/dwarf_expression/dwarf_expression.cpp
index 32798ad382..98ce2076ce 100644
--- a/teshsuite/mc/dwarf_expression/dwarf_expression.cpp
+++ b/teshsuite/mc/dwarf_expression/dwarf_expression.cpp
@@ -12,10 +12,10 @@
 #include <assert.h>
 #include <stdlib.h>
 
-#include "mc/mc_process.h"
 #include "mc/mc_private.h"
 #include "mc/mc_object_info.h"
 
+#include "mc/Process.hpp"
 #include "mc/Type.hpp"
 #include "mc/ObjectInformation.hpp"
 #include "mc/Variable.hpp"
diff --git a/teshsuite/smpi/isp/umpire/CMakeLists.txt b/teshsuite/smpi/isp/umpire/CMakeLists.txt
index 947aa9e197..65532e450c 100644
--- a/teshsuite/smpi/isp/umpire/CMakeLists.txt
+++ b/teshsuite/smpi/isp/umpire/CMakeLists.txt
@@ -1,10 +1,6 @@
 # See http://formalverification.cs.utah.edu/ISP_Tests/
 
 set(umpire_tests_passing
-  any_src-can-deadlock
-  any_src-can-deadlock2
-  any_src-can-deadlock3
-  any_src-deadlock
   change-send-buffer
   comm-dup-no-error
   comm-dup-no-free
@@ -35,12 +31,21 @@ set(umpire_tests_passing
   partial-recv
   sendrecv-deadlock
   send-recv-ok
-  waitall-deadlock
-  waitany-deadlock
-  wait-deadlock
+  irecv-isend-ok
+  irecv-isend-ok2
+  lost-request-waitall
  ) # Passing (no deadlock) tests
- 
-set(umpire_tests_failing
+
+# These are supposed to deadlock but ISP does not find deadlock
+# and we don't either. What should be test here?
+set(umpire_tests_missed_deadlock
+  any_src-deadlock
+  any_src-can-deadlock
+  any_src-can-deadlock2
+  any_src-can-deadlock3
+  )
+
+set(umpire_tests_deadlock
   any_src-can-deadlock10
   any_src-can-deadlock10_mod
   any_src-can-deadlock11
@@ -74,10 +79,9 @@ set(umpire_tests_failing
   dropped-req
   finalize-deadlock
   irecv-deadlock
-  irecv-isend-ok
-  irecv-isend-ok2
-  lost-request-waitall
-
+  waitall-deadlock
+  waitany-deadlock
+  wait-deadlock
  ) # failing (deadlocking) tests
  
 set(umpire_tests_problematic
@@ -169,7 +173,6 @@ set(umpire_src_other
   type-no-free-exhaustive.c
   )
 
-
 # Build the tests
 #################
 
@@ -184,7 +187,7 @@ if(enable_smpi AND enable_smpi_ISP_testsuite)
 
   include_directories(BEFORE "${CMAKE_HOME_DIRECTORY}/include/smpi")
 
-  foreach (test ${umpire_tests_passing} ${umpire_tests_failing} ${umpire_tests_problematic} )
+  foreach (test ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_problematic} )
     add_executable(${test} ${test}.c)
     target_link_libraries(${test} simgrid)
     set_source_files_properties(${test}.c PROPERTIES COMPILE_FLAGS "-Wno-error")
@@ -192,13 +195,15 @@ if(enable_smpi AND enable_smpi_ISP_testsuite)
     set(files_to_clean ${files_to_clean} ${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh)
   endforeach(test)
   
-  foreach (test ${umpire_tests_passing} )
+  # TODO, what should we do about ${umpire_tests_missed_deadlock}?
+
+  foreach (test ${umpire_tests_passing})
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30")
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display" APPEND)
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "\$ \${bindir:=.}/../../../../bin/smpirun -wrapper \"\${bindir:=.}/../../../../bin/simgrid-mc\" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich \${bindir:=.}/${test} --log=smpi_coll.thresh:error" APPEND)
   endforeach()
 
-  foreach (test ${umpire_tests_failing} ${umpire_tests_problematic} )
+  foreach (test ${umpire_tests_deadlock} ${umpire_tests_problematic} )
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30"     )
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! expect return 3" APPEND)
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display"  APPEND)
@@ -214,7 +219,7 @@ else()
     set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file})
   endforeach()
 
-  foreach(file ${umpire_tests_passing} ${umpire_tests_failing} ${umpire_tests_problematic}  ) 
+  foreach(file ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_missed_deadlock} ${umpire_tests_problematic}  ) 
     set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file}.c)
   endforeach()
 
diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 6daa09f8e7..52ab426af2 100644
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -616,8 +616,8 @@ set(MC_SRC
 
   src/mc/mc_forward.h
   src/mc/mc_forward.hpp
-  src/mc/mc_process.h
-  src/mc/mc_process.cpp
+  src/mc/Process.hpp
+  src/mc/Process.cpp
   src/mc/mc_unw.h
   src/mc/mc_unw.cpp
   src/mc/mc_unw_vmread.cpp