From: Frederic Suter <frederic.suter@cc.in2p3.fr>
Date: Wed, 23 Mar 2016 12:09:30 +0000 (+0100)
Subject: Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid
X-Git-Tag: v3_13~327
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/5787a5c839c1f49fec942290449d18b72b036d98?hp=cfc908020fbf63ece22826542148fa0e01fd4195

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

diff --git a/include/simgrid/s4u/As.hpp b/include/simgrid/s4u/As.hpp
index b79afa45ff..370edfc224 100644
--- a/include/simgrid/s4u/As.hpp
+++ b/include/simgrid/s4u/As.hpp
@@ -38,7 +38,7 @@ protected:
   
 public:
   /** @brief Seal your AS once you're done adding content, and before routing stuff through it */
-  virtual void Seal();
+  virtual void seal();
   char *name();
   As *father();;
   xbt_dict_t children(); // Sub AS
diff --git a/include/xbt/system_error.hpp b/include/xbt/system_error.hpp
index f2aabe7f83..f580e750ce 100644
--- a/include/xbt/system_error.hpp
+++ b/include/xbt/system_error.hpp
@@ -8,6 +8,9 @@
 
 #include <system_error>
 
+#ifndef SIMGRID_MC_SYSTEM_ERROR_HPP
+#define SIMGRID_MC_SYSTEM_ERROR_HPP
+
 namespace simgrid {
 namespace xbt {
 
@@ -31,3 +34,5 @@ std::system_error errno_error(int errnum, const char* what)
 
 }
 }
+
+#endif
diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index d6352f567c..74c6ed8fa2 100644
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -44,7 +44,6 @@ extern XBT_PUBLIC(int) _sg_mc_visited;
 extern XBT_PRIVATE char* _sg_mc_dot_output_file;
 extern XBT_PUBLIC(int) _sg_mc_comms_determinism;
 extern XBT_PUBLIC(int) _sg_mc_send_determinism;
-extern XBT_PRIVATE int _sg_mc_safety;
 extern XBT_PRIVATE int _sg_mc_liveness;
 extern XBT_PRIVATE int _sg_mc_snapshot_fds;
 extern XBT_PRIVATE int _sg_mc_termination;
diff --git a/src/mc/Checker.cpp b/src/mc/Checker.cpp
new file mode 100644
index 0000000000..159e3d5780
--- /dev/null
+++ b/src/mc/Checker.cpp
@@ -0,0 +1,26 @@
+/* Copyright (c) 2016. 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 "src/mc/Checker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+Checker::~Checker()
+{
+}
+
+FunctionalChecker::~FunctionalChecker()
+{
+}
+
+int FunctionalChecker::run()
+{
+  return function_(*session_);
+}
+
+}
+}
diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp
new file mode 100644
index 0000000000..478665a8f9
--- /dev/null
+++ b/src/mc/Checker.hpp
@@ -0,0 +1,58 @@
+/* Copyright (c) 2016. 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. */
+
+#ifndef SIMGRID_MC_CHECKER_HPP
+#define SIMGRID_MC_CHECKER_HPP
+
+#include <functional>
+#include <memory>
+
+#include "src/mc/mc_forward.hpp"
+
+namespace simgrid {
+namespace mc {
+
+/** A model-checking algorithm
+ *
+ *  The goal is to move the data/state/configuration of a model-checking
+ *  algorihms in subclasses. Implementing this interface will probably
+ *  not be really mandatory, you might be able to write your
+ *  model-checking algorithm as plain imperative code instead.
+ *
+ *  It works by manipulating a model-checking Session.
+ */
+// abstract
+class Checker {
+  Session* session_;
+public:
+  Checker(Session& session) : session_(&session) {}
+
+  // No copy:
+  Checker(Checker const&) = delete;
+  Checker& operator=(Checker const&) = delete;
+
+  virtual ~Checker();
+  virtual int run() = 0;
+
+protected:
+  Session& getSession() { return *session_; }
+};
+
+/** Adapt a std::function to a checker */
+class FunctionalChecker : public Checker {
+  Session* session_;
+  std::function<int(Session& session)> function_;
+public:
+  FunctionalChecker(Session& session, std::function<int(Session& session)> f)
+    : Checker(session), function_(std::move(f)) {}
+  ~FunctionalChecker();
+  int run() override;
+};
+
+}
+}
+
+#endif
diff --git a/src/mc/mc_safety.cpp b/src/mc/SafetyChecker.cpp
similarity index 90%
rename from src/mc/mc_safety.cpp
rename to src/mc/SafetyChecker.cpp
index 4b214ffef7..442b871eed 100644
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2015. The SimGrid Team.
+/* Copyright (c) 2016. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -22,6 +22,8 @@
 #include "src/mc/mc_smx.h"
 #include "src/mc/Client.hpp"
 #include "src/mc/mc_exit.h"
+#include "src/mc/Checker.hpp"
+#include "src/mc/SafetyChecker.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
@@ -45,12 +47,10 @@ static int is_exploration_stack_state(mc_state_t current_state){
   return 0;
 }
 
-static void modelcheck_safety_init(void);
-
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
-static void pre_modelcheck_safety()
+void SafetyChecker::pre()
 {
   simgrid::mc::visited_states.clear();
 
@@ -66,20 +66,16 @@ static void pre_modelcheck_safety()
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy)) {
       MC_state_interleave_process(initial_state, &p.copy);
-      if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
+      if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
 
   xbt_fifo_unshift(mc_stack, initial_state);
 }
 
-
-/** \brief Model-check the application using a DFS exploration
- *         with DPOR (Dynamic Partial Order Reductions)
- */
-int modelcheck_safety(void)
+int SafetyChecker::run()
 {
-  modelcheck_safety_init();
+  this->init();
 
   char *req_str = nullptr;
   int value;
@@ -132,13 +128,13 @@ int modelcheck_safety(void)
           return SIMGRID_MC_EXIT_NON_TERMINATION;
       }
 
-      if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
+      if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
           if (simgrid::mc::process_is_enabled(&p.copy)) {
             MC_state_interleave_process(next_state, &p.copy);
-            if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
+            if (reductionMode_ != simgrid::mc::ReductionMode::none)
               break;
           }
 
@@ -192,14 +188,15 @@ int modelcheck_safety(void)
          state that executed that previous request. */
 
       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
-        if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::dpor) {
+        if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
           req = MC_state_get_internal_request(state);
           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
             xbt_die("Mutex is currently not supported with DPOR, "
               "use --cfg=model-check/reduction:none");
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
-            if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
+            if (reductionMode_ != simgrid::mc::ReductionMode::none
+                && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
                 XBT_DEBUG("Dependent Transitions:");
                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
@@ -257,13 +254,14 @@ int modelcheck_safety(void)
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
-static void modelcheck_safety_init(void)
+void SafetyChecker::init()
 {
-  if(_sg_mc_termination)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
-  else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
-  _sg_mc_safety = 1;
+  reductionMode_ = simgrid::mc::reduction_mode;
+  if( _sg_mc_termination)
+    reductionMode_ = simgrid::mc::ReductionMode::none;
+  else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
+    reductionMode_ = simgrid::mc::ReductionMode::dpor;
+
   if (_sg_mc_termination)
     XBT_INFO("Check non progressive cycles");
   else
@@ -272,17 +270,23 @@ static void modelcheck_safety_init(void)
 
   XBT_DEBUG("Starting the safety algorithm");
 
-  _sg_mc_safety = 1;
-
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
-  pre_modelcheck_safety();
+  this->pre();
 
   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 }
 
+SafetyChecker::SafetyChecker(Session& session) : Checker(session)
+{
+}
+
+SafetyChecker::~SafetyChecker()
+{
+}
+  
 }
 }
diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
new file mode 100644
index 0000000000..3c559a73f7
--- /dev/null
+++ b/src/mc/SafetyChecker.hpp
@@ -0,0 +1,31 @@
+/* Copyright (c) 2008-2016. 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. */
+
+#ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
+#define SIMGRID_MC_SAFETY_CHECKER_HPP
+
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/Checker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class SafetyChecker : public Checker {
+  simgrid::mc::ReductionMode reductionMode_ = simgrid::mc::ReductionMode::unset;
+public:
+  SafetyChecker(Session& session);
+  ~SafetyChecker();
+  int run() override;
+private:
+  // Temp
+  void init();
+  void pre();
+};
+
+}
+}
+
+#endif
diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
new file mode 100644
index 0000000000..223bfc0ff6
--- /dev/null
+++ b/src/mc/Session.cpp
@@ -0,0 +1,150 @@
+/* Copyright (c) 2015-2016. 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 <fcntl.h>
+#include <signal.h>
+
+#include <functional>
+
+#include <xbt/system_error.hpp>
+#include <simgrid/sg_config.h>
+#include <simgrid/modelchecker.h>
+
+#include "src/mc/Session.hpp"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
+
+namespace simgrid {
+namespace mc {
+
+static void setup_child_environment(int socket)
+{
+#ifdef __linux__
+  // Make sure we do not outlive our parent:
+  sigset_t mask;
+  sigemptyset (&mask);
+  if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
+    throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
+  if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
+    throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
+#endif
+
+  int res;
+
+  // Remove CLOEXEC in order to pass the socket to the exec-ed program:
+  int fdflags = fcntl(socket, F_GETFD, 0);
+  if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
+    throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
+
+  // Set environment:
+  setenv(MC_ENV_VARIABLE, "1", 1);
+
+  // Disable lazy relocation in the model-checked process.
+  // We don't want the model-checked process to modify its .got.plt during
+  // snapshot.
+  setenv("LC_BIND_NOW", "1", 1);
+
+  char buffer[64];
+  res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
+  if ((size_t) res >= sizeof(buffer) || res == -1)
+    std::abort();
+  setenv(MC_ENV_SOCKET_FD, buffer, 1);
+}
+
+/** Execute some code in a forked process */
+template<class F>
+static inline
+pid_t do_fork(F code)
+{
+  pid_t pid = fork();
+  if (pid < 0)
+    throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
+  if (pid != 0)
+    return pid;
+
+  // Child-process:
+  try {
+    code();
+    _exit(EXIT_SUCCESS);
+  }
+  catch(...) {
+    // The callback should catch exceptions:
+    std::terminate();
+  }
+}
+
+Session::Session(pid_t pid, int socket)
+{
+  std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(pid, socket));
+  // TODO, automatic detection of the config from the process
+  process->privatized(
+    sg_cfg_get_boolean("smpi/privatize_global_variables"));
+  modelChecker_ = std::unique_ptr<ModelChecker>(
+    new simgrid::mc::ModelChecker(std::move(process)));
+  xbt_assert(mc_model_checker == nullptr);
+  mc_model_checker = modelChecker_.get();
+  mc_model_checker->start();
+}
+
+Session::~Session()
+{
+  this->close();
+}
+
+// static
+Session* Session::fork(std::function<void(void)> code)
+{
+  // Create a AF_LOCAL socketpair used for exchanging messages
+  // bewteen the model-checker process (ourselves) and the model-checked
+  // process:
+  int res;
+  int sockets[2];
+  res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
+  if (res == -1)
+    throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
+
+  pid_t pid = do_fork([&] {
+    ::close(sockets[1]);
+    setup_child_environment(sockets[0]);
+    code();
+    xbt_die("The model-checked process failed to exec()");
+  });
+
+  // Parent (model-checker):
+  ::close(sockets[0]);
+
+  return new Session(pid, sockets[1]);
+}
+
+// static
+Session* Session::spawnv(const char *path, char *const argv[])
+{
+  return Session::fork([&] {
+    execv(path, argv);
+  });
+}
+
+// static
+Session* Session::spawnvp(const char *path, char *const argv[])
+{
+  return Session::fork([&] {
+    execvp(path, argv);
+  });
+}
+
+void Session::close()
+{
+  if (modelChecker_) {
+    modelChecker_->shutdown();
+    modelChecker_ = nullptr;
+    mc_model_checker = nullptr;
+  }
+}
+
+simgrid::mc::Session* session;
+
+}
+}
\ No newline at end of file
diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
new file mode 100644
index 0000000000..f53d94816f
--- /dev/null
+++ b/src/mc/Session.hpp
@@ -0,0 +1,73 @@
+/* Copyright (c) 2016. 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. */
+
+#ifndef SIMGRID_MC_SESSION_HPP
+#define SIMGRID_MC_SESSION_HPP
+
+#ifdef __linux__
+#include <sys/prctl.h>
+#endif
+
+#include <sys/types.h>
+#include <sys/socket.h>
+#include <xbt/sysdep.h>
+#include <xbt/system_error.hpp>
+
+#include <functional>
+
+#include <xbt/log.h>
+
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/ModelChecker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+/** A model-checking session
+ *
+ *  This is expected to become the interface used by model-checking
+ *  algorithms to control the execution of the model-checked process
+ *  and the exploration of the execution graph. Model-checking
+ *  algorithms should be able to be written in high-level languages
+ *  (e.g. Python) using bindings on this interface.
+ */
+class Session {
+private:
+  std::unique_ptr<ModelChecker> modelChecker_;
+
+private: //
+  Session(pid_t pid, int socket);
+
+  // No copy:
+  Session(Session const&) = delete;
+  Session& operator=(Session const&) = delete;
+
+public:
+  ~Session();
+  void close();
+
+public: // static constructors
+
+  /** Create a new session by forking
+   *
+   *  The code is expected to `exec` the model-checker program.
+   */
+  static Session* fork(std::function<void(void)> code);
+
+  /** Create a session using `execv` */
+  static Session* spawnv(const char *path, char *const argv[]);
+
+  /** Create a session using `execvp` */
+  static Session* spawnvp(const char *path, char *const argv[]);
+};
+
+// Temporary
+extern simgrid::mc::Session* session;
+
+}
+}
+
+#endif
diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index d16cd27dcf..54fe76e0f8 100644
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -337,6 +337,20 @@ static void MC_pre_modelcheck_comm_determinism(void)
   xbt_fifo_unshift(mc_stack, initial_state);
 }
 
+static inline
+bool all_communications_are_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 false;
+    }
+  }
+  return true;
+}
+
 static int MC_modelcheck_comm_determinism_main(void)
 {
 
@@ -392,7 +406,14 @@ static int MC_modelcheck_comm_determinism_main(void)
       /* Create the new expanded state */
       next_state = MC_state_new();
 
-      if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
+      /* 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. */
+      bool compare_snapshots = all_communications_are_finished()
+        && initial_global_state->initial_communications_pattern_done;
+
+      if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
@@ -462,7 +483,6 @@ static int MC_modelcheck_comm_determinism_main(void)
 int MC_modelcheck_comm_determinism(void)
 {
   XBT_INFO("Check communication determinism");
-  simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
   mc_model_checker->wait_for_requests();
 
   if (mc_mode == MC_MODE_CLIENT)
diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 22dbfaf170..6d208ddbd4 100644
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -64,8 +64,6 @@ struct ComparisonState {
 
 using simgrid::mc::ComparisonState;
 
-extern "C" {
-
 /************************** Snapshot comparison *******************************/
 /******************************************************************************/
 
@@ -348,31 +346,13 @@ static int compare_local_variables(int process_index,
     return 0;
 }
 
-int snapshot_compare(void *state1, void *state2)
+namespace simgrid {
+namespace mc {
+
+int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();
 
-  simgrid::mc::Snapshot* s1;
-  simgrid::mc::Snapshot* s2;
-  int num1, num2;
-
-  if (_sg_mc_liveness) {        /* Liveness MC */
-    s1 = ((simgrid::mc::VisitedPair*) state1)->graph_state->system_state;
-    s2 = ((simgrid::mc::VisitedPair*) state2)->graph_state->system_state;
-    num1 = ((simgrid::mc::VisitedPair*) state1)->num;
-    num2 = ((simgrid::mc::VisitedPair*) state2)->num;
-  }else if (_sg_mc_termination) { /* Non-progressive cycle MC */
-    s1 = ((mc_state_t) state1)->system_state;
-    s2 = ((mc_state_t) state2)->system_state;
-    num1 = ((mc_state_t) state1)->num;
-    num2 = ((mc_state_t) state2)->num;
-  } else {                      /* Safety or comm determinism MC */
-    s1 = ((simgrid::mc::VisitedState*) state1)->system_state;
-    s2 = ((simgrid::mc::VisitedState*) state2)->system_state;
-    num1 = ((simgrid::mc::VisitedState*) state1)->num;
-    num2 = ((simgrid::mc::VisitedState*) state2)->num;
-  }
-
   int errors = 0;
   int res_init;
 
@@ -560,7 +540,25 @@ int snapshot_compare(void *state1, void *state2)
 #endif
 
   return errors > 0 || hash_result;
+}
+
+int snapshot_compare(mc_state_t state1, mc_state_t state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->system_state;
+  simgrid::mc::Snapshot* s2 = state2->system_state;
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
+}
 
+int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->system_state;
+  simgrid::mc::Snapshot* s2 = state2->system_state;
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
 }
 
 }
+}
diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 58a6b3146a..eadc3704cc 100644
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -61,7 +61,6 @@ int _sg_mc_visited = 0;
 char *_sg_mc_dot_output_file = nullptr;
 int _sg_mc_comms_determinism = 0;
 int _sg_mc_send_determinism = 0;
-int _sg_mc_safety = 0;
 int _sg_mc_liveness = 0;
 int _sg_mc_snapshot_fds = 0;
 int _sg_mc_termination = 0;
diff --git a/src/mc/mc_forward.hpp b/src/mc/mc_forward.hpp
index b71caabc3f..5b0cc70278 100644
--- a/src/mc/mc_forward.hpp
+++ b/src/mc/mc_forward.hpp
@@ -28,6 +28,10 @@ class Variable;
 class Frame;
 class SimixProcessInformation;
 
+class Session;
+class Checker;
+class FunctionalChecker;
+
 }
 }
 
diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index e92fcaf53b..090fe456b9 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -223,73 +223,6 @@ void MC_replay(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
-void MC_replay_liveness(xbt_fifo_t stack)
-{
-  xbt_fifo_item_t item;
-  simgrid::mc::Pair* pair = nullptr;
-  mc_state_t state = nullptr;
-  smx_simcall_t req = nullptr, saved_req = NULL;
-  int value, depth = 1;
-  char *req_str;
-
-  XBT_DEBUG("**** Begin Replay ****");
-
-  /* Intermediate backtracking */
-  if(_sg_mc_checkpoint > 0) {
-    item = xbt_fifo_get_first_item(stack);
-    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-    if(pair->graph_state->system_state){
-      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
-      return;
-    }
-  }
-
-  /* Restore the initial state */
-  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
-
-    /* Traverse the stack from the initial state and re-execute the transitions */
-    for (item = xbt_fifo_get_last_item(stack);
-         item != xbt_fifo_get_first_item(stack);
-         item = xbt_fifo_get_prev_item(item)) {
-
-      pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-
-      state = (mc_state_t) pair->graph_state;
-
-      if (pair->exploration_started) {
-
-        saved_req = MC_state_get_executed_request(state, &value);
-
-        if (saved_req != nullptr) {
-          /* because we got a copy of the executed request, we have to fetch the
-             real one, pointed by the request field of the issuer process */
-          const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
-          req = &issuer->simcall;
-
-          /* Debug information */
-          if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
-            req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-            xbt_free(req_str);
-          }
-
-        }
-
-        simgrid::mc::handle_simcall(req, value);
-        mc_model_checker->wait_for_requests();
-      }
-
-      /* Update statistics */
-      mc_stats->visited_pairs++;
-      mc_stats->executed_transitions++;
-
-      depth++;
-      
-    }
-
-  XBT_DEBUG("**** End Replay ****");
-}
-
 /**
  * \brief Dumps the contents of a model-checker's stack and shows the actual
  *        execution trace
@@ -350,39 +283,6 @@ void MC_show_non_termination(void){
   MC_print_statistics(mc_stats);
 }
 
-namespace simgrid {
-namespace mc {
-
-void show_stack_liveness(xbt_fifo_t stack)
-{
-  int value;
-  simgrid::mc::Pair* pair;
-  xbt_fifo_item_t item;
-  smx_simcall_t req;
-  char *req_str = nullptr;
-
-  for (item = xbt_fifo_get_last_item(stack);
-       item; item = xbt_fifo_get_prev_item(item)) {
-    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-    req = MC_state_get_executed_request(pair->graph_state, &value);
-    if (req && req->call != SIMCALL_NONE) {
-      req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
-    }
-  }
-}
-
-void dump_stack_liveness(xbt_fifo_t stack)
-{
-  simgrid::mc::Pair* pair;
-  while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
-    delete pair;
-}
-
-}
-}
-
 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {
diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index c9202f5c9a..254a130604 100644
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -6,11 +6,15 @@
 
 #include <cstring>
 
+#include <algorithm>
+#include <memory>
+
 #include <unistd.h>
 #include <sys/wait.h>
 
 #include <xbt/automaton.h>
 #include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
 #include <xbt/fifo.h>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
@@ -21,6 +25,7 @@
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_smx.h"
 #include "src/mc/Client.hpp"
+#include "src/mc/mc_private.h"
 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_exit.h"
@@ -37,6 +42,8 @@ xbt_dynar_t acceptance_pairs;
 namespace simgrid {
 namespace mc {
 
+static xbt_dynar_t visited_pairs;
+
 Pair::Pair() : num(++mc_stats->expanded_pairs),
   visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
 {}
@@ -46,6 +53,33 @@ Pair::~Pair() {
     MC_state_delete(this->graph_state, 1);
 }
 
+static  void show_stack_liveness(xbt_fifo_t stack)
+{
+  int value;
+  simgrid::mc::Pair* pair;
+  xbt_fifo_item_t item;
+  smx_simcall_t req;
+  char *req_str = nullptr;
+
+  for (item = xbt_fifo_get_last_item(stack);
+       item; item = xbt_fifo_get_prev_item(item)) {
+    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+    req = MC_state_get_executed_request(pair->graph_state, &value);
+    if (req && req->call != SIMCALL_NONE) {
+      req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
+      XBT_INFO("%s", req_str);
+      xbt_free(req_str);
+    }
+  }
+}
+
+static void dump_stack_liveness(xbt_fifo_t stack)
+{
+  simgrid::mc::Pair* pair;
+  while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
+    delete pair;
+}
+
 static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
 {
   unsigned int cursor = 0;
@@ -58,58 +92,49 @@ static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
   return std::move(values);
 }
 
+static int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->graph_state->system_state;
+  simgrid::mc::Snapshot* s2 = state2->graph_state->system_state;
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
+}
+
 static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
 {
-  simgrid::mc::VisitedPair* new_pair = new VisitedPair(
-    pair->num, pair->automaton_state, pair->atomic_propositions.get(),
-    pair->graph_state);
+  auto acceptance_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(::acceptance_pairs);
+  auto new_pair =
+    std::unique_ptr<simgrid::mc::VisitedPair>(new VisitedPair(
+      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+      pair->graph_state));
   new_pair->acceptance_pair = 1;
 
-  if (xbt_dynar_is_empty(acceptance_pairs))
-    xbt_dynar_push(acceptance_pairs, &new_pair);
-  else {
-
-    int min = -1, max = -1, index;
-    //int res;
-    simgrid::mc::VisitedPair* pair_test;
-    int cursor;
-
-    index = get_search_interval(acceptance_pairs, new_pair, &min, &max);
-
-    if (min != -1 && max != -1) {       // Acceptance pair with same number of processes and same heap bytes used exists
-
-      cursor = min;
-      if(pair->search_cycle == 1){
-        while (cursor <= max) {
-          pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, cursor, simgrid::mc::VisitedPair*);
-          if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
-            if (xbt_automaton_propositional_symbols_compare_value(
-                pair_test->atomic_propositions.get(),
-                new_pair->atomic_propositions.get()) == 0) {
-              if (snapshot_compare(pair_test, new_pair) == 0) {
-                XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
-                xbt_fifo_shift(mc_stack);
-                if (dot_output != nullptr)
-                  fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
-                return nullptr;
-              }
-            }
+  auto res = std::equal_range(acceptance_pairs.begin(), acceptance_pairs.end(),
+    new_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+  if (pair->search_cycle == 1)
+    for (auto i = res.first; i != res.second; ++i) {
+      simgrid::mc::VisitedPair* pair_test = *i;
+      if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
+        if (xbt_automaton_propositional_symbols_compare_value(
+            pair_test->atomic_propositions.get(),
+            new_pair->atomic_propositions.get()) == 0) {
+          if (snapshot_compare(pair_test, new_pair.get()) == 0) {
+            XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
+            xbt_fifo_shift(mc_stack);
+            if (dot_output != nullptr)
+              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
+            return nullptr;
           }
-          cursor++;
         }
       }
-      xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
-    } else {
-      pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, index, simgrid::mc::VisitedPair*);
-      if (pair_test->nb_processes < new_pair->nb_processes)
-        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
-        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      else
-        xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
     }
-  }
-  return new_pair;
+
+  auto new_raw_pair = new_pair.release();
+  xbt_dynar_insert_at(
+    ::acceptance_pairs, res.first - acceptance_pairs.begin(), &new_raw_pair);
+  return new_raw_pair;
 }
 
 static void remove_acceptance_pair(int pair_num)
@@ -207,6 +232,146 @@ static void MC_pre_modelcheck_liveness(void)
   }
 }
 
+static void MC_replay_liveness(xbt_fifo_t stack)
+{
+  xbt_fifo_item_t item;
+  simgrid::mc::Pair* pair = nullptr;
+  mc_state_t state = nullptr;
+  smx_simcall_t req = nullptr, saved_req = NULL;
+  int value, depth = 1;
+  char *req_str;
+
+  XBT_DEBUG("**** Begin Replay ****");
+
+  /* Intermediate backtracking */
+  if(_sg_mc_checkpoint > 0) {
+    item = xbt_fifo_get_first_item(stack);
+    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+    if(pair->graph_state->system_state){
+      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+      return;
+    }
+  }
+
+  /* Restore the initial state */
+  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+
+    /* Traverse the stack from the initial state and re-execute the transitions */
+    for (item = xbt_fifo_get_last_item(stack);
+         item != xbt_fifo_get_first_item(stack);
+         item = xbt_fifo_get_prev_item(item)) {
+
+      pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+
+      state = (mc_state_t) pair->graph_state;
+
+      if (pair->exploration_started) {
+
+        saved_req = MC_state_get_executed_request(state, &value);
+
+        if (saved_req != nullptr) {
+          /* because we got a copy of the executed request, we have to fetch the
+             real one, pointed by the request field of the issuer process */
+          const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+          req = &issuer->simcall;
+
+          /* Debug information */
+          if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
+            req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }
+
+        }
+
+        simgrid::mc::handle_simcall(req, value);
+        mc_model_checker->wait_for_requests();
+      }
+
+      /* Update statistics */
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
+
+      depth++;
+
+    }
+
+  XBT_DEBUG("**** End Replay ****");
+}
+
+/**
+ * \brief Checks whether a given pair has already been visited by the algorithm.
+ */
+static
+int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+{
+  if (_sg_mc_visited == 0)
+    return -1;
+
+  simgrid::mc::VisitedPair* new_visited_pair = nullptr;
+  if (visited_pair == nullptr)
+    new_visited_pair = new simgrid::mc::VisitedPair(
+      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+      pair->graph_state);
+  else
+    new_visited_pair = visited_pair;
+
+  auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(simgrid::mc::visited_pairs);
+
+  auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
+    new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+  for (auto i = range.first; i != range.second; ++i) {
+    simgrid::mc::VisitedPair* pair_test = *i;
+    std::size_t cursor = i - visited_pairs.begin();
+    if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+      if (xbt_automaton_propositional_symbols_compare_value(
+          pair_test->atomic_propositions.get(),
+          new_visited_pair->atomic_propositions.get()) == 0) {
+        if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+          if (pair_test->other_num == -1)
+            new_visited_pair->other_num = pair_test->num;
+          else
+            new_visited_pair->other_num = pair_test->other_num;
+          if (dot_output == nullptr)
+            XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+          else
+            XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+          xbt_dynar_remove_at(simgrid::mc::visited_pairs, cursor, &pair_test);
+          xbt_dynar_insert_at(simgrid::mc::visited_pairs, cursor, &new_visited_pair);
+          pair_test->visited_removed = 1;
+          if (!pair_test->acceptance_pair
+              || pair_test->acceptance_removed == 1)
+            delete pair_test;
+          return new_visited_pair->other_num;
+        }
+      }
+    }
+  }
+
+  xbt_dynar_insert_at(simgrid::mc::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+
+  if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+    int min2 = mc_stats->expanded_pairs;
+    unsigned int index2 = 0;
+    for (std::size_t i = 0; i != visited_pairs.size(); ++i) {
+      simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
+      if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+          && pair_test->num < min2) {
+        index2 = i;
+        min2 = pair_test->num;
+      }
+    }
+    simgrid::mc::VisitedPair* pair_test = nullptr;
+    xbt_dynar_remove_at(simgrid::mc::visited_pairs, index2, &pair_test);
+    pair_test->visited_removed = 1;
+    if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+      delete pair_test;
+  }
+
+  return -1;
+}
+
 static int MC_modelcheck_liveness_main(void)
 {
   simgrid::mc::Pair* current_pair = nullptr;
@@ -373,8 +538,6 @@ static int MC_modelcheck_liveness_main(void)
 
 int modelcheck_liveness(void)
 {
-  if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
   MC_automaton_load(_sg_mc_property_file);
   mc_model_checker->wait_for_requests();
diff --git a/src/mc/mc_liveness.h b/src/mc/mc_liveness.h
index b8fbd019f0..c722183695 100644
--- a/src/mc/mc_liveness.h
+++ b/src/mc/mc_liveness.h
@@ -61,11 +61,6 @@ struct XBT_PRIVATE VisitedPair {
 };
 
 int modelcheck_liveness(void);
-XBT_PRIVATE void show_stack_liveness(xbt_fifo_t stack);
-XBT_PRIVATE void dump_stack_liveness(xbt_fifo_t stack);
-
-XBT_PRIVATE extern xbt_dynar_t visited_pairs;
-XBT_PRIVATE int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair);
 
 }
 }
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 869042cdf6..e41f8c0ad7 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -37,6 +37,23 @@
 
 #include "src/mc/mc_protocol.h"
 
+#ifdef __cplusplus
+namespace simgrid {
+namespace mc {
+
+struct DerefAndCompareByNbProcessesAndUsedHeap {
+  template<class X, class Y>
+  bool operator()(X const& a, Y const& b)
+  {
+    return std::make_pair(a->nb_processes, a->heap_bytes_used) <
+      std::make_pair(b->nb_processes, b->heap_bytes_used);
+  }
+};
+
+}
+}
+#endif
+
 SG_BEGIN_DECL()
 
 /********************************* MC Global **********************************/
@@ -48,7 +65,6 @@ XBT_PRIVATE extern FILE *dot_output;
 XBT_PRIVATE extern int user_max_depth_reached;
 
 XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
-XBT_PRIVATE void MC_replay_liveness(xbt_fifo_t stack);
 XBT_PRIVATE void MC_show_deadlock(smx_simcall_t req);
 XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
 XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);
@@ -61,9 +77,6 @@ XBT_PRIVATE void MC_show_non_termination(void);
  */
 XBT_PRIVATE extern xbt_fifo_t mc_stack;
 
-XBT_PRIVATE int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
-
-
 /****************************** Statistics ************************************/
 
 typedef struct mc_stats {
@@ -81,8 +94,6 @@ XBT_PRIVATE void MC_print_statistics(mc_stats_t stats);
 
 /********************************** Snapshot comparison **********************************/
 
-XBT_PRIVATE int snapshot_compare(void *state1, void *state2);
-
 //#define MC_DEBUG 1
 #define MC_VERBOSE 1
 
@@ -91,6 +102,8 @@ XBT_PRIVATE int snapshot_compare(void *state1, void *state2);
 XBT_PRIVATE void MC_report_assertion_error(void);
 XBT_PRIVATE void MC_report_crash(int status);
 
+SG_END_DECL()
+
 #ifdef __cplusplus
 
 namespace simgrid {
@@ -99,11 +112,12 @@ namespace mc {
 XBT_PRIVATE void find_object_address(
   std::vector<simgrid::xbt::VmMap> const& maps, simgrid::mc::ObjectInformation* result);
 
+XBT_PRIVATE
+int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2);
+
 }
 }
 
 #endif
 
-SG_END_DECL()
-
 #endif
diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index 91f02ccbf2..1404c21e6f 100644
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -136,9 +136,6 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
 // Those are MC_state_get_internal_request(state)
 bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
 {
-  if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::none)
-    return true;
-
   if (r1->issuer == r2->issuer)
     return false;
 
diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h
index 25eb06a0d1..4ee245f647 100644
--- a/src/mc/mc_safety.h
+++ b/src/mc/mc_safety.h
@@ -31,8 +31,6 @@ enum class ReductionMode {
 
 extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
 
-int modelcheck_safety(void);
-
 struct XBT_PRIVATE VisitedState {
   simgrid::mc::Snapshot* system_state = nullptr;
   size_t heap_bytes_used = 0;
@@ -45,7 +43,8 @@ struct XBT_PRIVATE VisitedState {
 };
 
 extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
-XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state);
+XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots);
+XBT_PRIVATE int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2);
 
 }
 }
diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index 292d15ceb2..93b350ffee 100644
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -68,4 +68,12 @@ XBT_PRIVATE void MC_state_remove_interleave_process(mc_state_t state, smx_proces
 
 SG_END_DECL()
 
+namespace simgrid {
+namespace mc {
+
+XBT_PRIVATE int snapshot_compare(mc_state_t state1, mc_state_t state2);
+
+}
+}
+
 #endif
diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 19a9e2ec4d..6f136ec18d 100644
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -8,11 +8,13 @@
 #include <sys/wait.h>
 
 #include <memory>
+#include <algorithm>
 
 #include <xbt/automaton.h>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 #include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
 #include <xbt/fifo.h>
 
 #include "src/mc/mc_comm_pattern.h"
@@ -28,7 +30,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
 namespace simgrid {
 namespace mc {
 
-xbt_dynar_t visited_pairs;
 std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
 
 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
@@ -115,180 +116,27 @@ VisitedPair::~VisitedPair()
     MC_state_delete(this->graph_state, 1);
 }
 
-}
-}
-
-/**
- *  \brief Find a suitable subrange of candidate duplicates for a given state
- *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
- *  \param ref current state/pair;
- *  \param min (output) index of the beginning of the the subrange
- *  \param max (output) index of the enf of the subrange
- *
- *  Given a suitably ordered array of states/pairs, this function extracts a subrange
- *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
- *  This function uses only fast discriminating criterions and does not use the
- *  full state/pair comparison algorithms.
- *
- *  The states/pairs in list MUST be ordered using a (given) weak order
- *  (based on nb_processes and heap_bytes_used).
- *  The subrange is the subrange of "equivalence" of the given state/pair.
- */
-int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
-{
-  int cursor = 0, previous_cursor;
-  int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
-  void *ref_test;
-
-  if (_sg_mc_liveness) {
-    nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes;
-    heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used;
-  } else {
-    nb_processes = ((simgrid::mc::VisitedState*) ref)->nb_processes;
-    heap_bytes_used = ((simgrid::mc::VisitedState*) ref)->heap_bytes_used;
-  }
-
-  int start = 0;
-  int end = xbt_dynar_length(list) - 1;
-
-  while (start <= end) {
-    cursor = (start + end) / 2;
-    if (_sg_mc_liveness) {
-      ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*);
-      nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
-      heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
-    } else {
-      ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*);
-      nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
-      heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
-    }
-    if (nb_processes_test < nb_processes)
-      start = cursor + 1;
-    else if (nb_processes_test > nb_processes)
-      end = cursor - 1;
-    else if (heap_bytes_used_test < heap_bytes_used)
-      start = cursor + 1;
-    else if (heap_bytes_used_test > heap_bytes_used)
-      end = cursor - 1;
-    else {
-        *min = *max = cursor;
-        previous_cursor = cursor - 1;
-        while (previous_cursor >= 0) {
-          if (_sg_mc_liveness) {
-            ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*);
-            nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
-            heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
-          } else {
-            ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*);
-            nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
-            heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
-          }
-          if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
-            break;
-          *min = previous_cursor;
-          previous_cursor--;
-        }
-        size_t next_cursor = cursor + 1;
-        while (next_cursor < xbt_dynar_length(list)) {
-          if (_sg_mc_liveness) {
-            ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*);
-            nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
-            heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
-          } else {
-            ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*);
-            nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
-            heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
-          }
-          if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
-            break;
-          *max = next_cursor;
-          next_cursor++;
-        }
-        return -1;
-    }
-  }
-  return cursor;
-}
-
-// TODO, it would make sense to use std::set instead
-template<class T>
-int get_search_interval(std::vector<std::unique_ptr<T>> const& list, T *ref, int *min, int *max)
-{
-  int nb_processes = ref->nb_processes;
-  int heap_bytes_used = ref->heap_bytes_used;
-
-  int cursor = 0;
-  int start = 0;
-  int end = list.size() - 1;
-  while (start <= end) {
-    cursor = (start + end) / 2;
-    int nb_processes_test = list[cursor]->nb_processes;
-    int heap_bytes_used_test = list[cursor]->heap_bytes_used;
-
-    if (nb_processes_test < nb_processes)
-      start = cursor + 1;
-    else if (nb_processes_test > nb_processes)
-      end = cursor - 1;
-    else if (heap_bytes_used_test < heap_bytes_used)
-      start = cursor + 1;
-    else if (heap_bytes_used_test > heap_bytes_used)
-      end = cursor - 1;
-    else {
-        *min = *max = cursor;
-        int previous_cursor = cursor - 1;
-        while (previous_cursor >= 0) {
-          nb_processes_test = list[previous_cursor]->nb_processes;
-          heap_bytes_used_test = list[previous_cursor]->heap_bytes_used;
-          if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
-            break;
-          *min = previous_cursor;
-          previous_cursor--;
-        }
-        size_t next_cursor = cursor + 1;
-        while (next_cursor < list.size()) {
-          nb_processes_test = list[next_cursor]->nb_processes;
-          heap_bytes_used_test = list[next_cursor]->heap_bytes_used;
-          if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
-            break;
-          *max = next_cursor;
-          next_cursor++;
-        }
-        return -1;
-    }
-  }
-  return cursor;
-}
-
-static
-bool some_communications_are_not_finished()
+static void prune_visited_states()
 {
-  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;
-    }
+  while (visited_states.size() > (std::size_t) _sg_mc_visited) {
+    XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
+    auto min_element = std::min_element(visited_states.begin(), visited_states.end(),
+      [](std::unique_ptr<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& b) {
+        return a->num < b->num;
+      });
+    xbt_assert(min_element != visited_states.end());
+    // and drop it:
+    visited_states.erase(min_element);
+    XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
   }
-  return false;
 }
 
-namespace simgrid {
-namespace mc {
-
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
-std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state)
+std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots)
 {
-  if (_sg_mc_visited == 0)
-    return nullptr;
 
-  /* 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. */
-  int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
-    some_communications_are_not_finished();
 
   std::unique_ptr<simgrid::mc::VisitedState> new_state =
     std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
@@ -296,27 +144,18 @@ std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_sta
   graph_state->in_visited_states = 1;
   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 
-  if (visited_states.empty()) {
-    visited_states.push_back(std::move(new_state));
-    return nullptr;
-  }
-
-    int min = -1, max = -1, index;
-
-    index = get_search_interval(visited_states, new_state.get(), &min, &max);
-
-    if (min != -1 && max != -1) {
+  auto range = std::equal_range(visited_states.begin(), visited_states.end(),
+    new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
-      if (_sg_mc_safety || (!partial_comm
-        && initial_global_state->initial_communications_pattern_done)) {
+      if (compare_snpashots) {
 
-        int cursor = min;
-        while (cursor <= max) {
-          if (snapshot_compare(visited_states[cursor].get(), new_state.get()) == 0) {
+        for (auto i = range.first; i != range.second; ++i) {
+          auto& visited_state = *i;
+          if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
             // The state has been visited:
 
             std::unique_ptr<simgrid::mc::VisitedState> old_state =
-              std::move(visited_states[cursor]);
+              std::move(visited_state);
 
             if (old_state->other_num == -1)
               new_state->other_num = old_state->num;
@@ -337,145 +176,16 @@ std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_sta
             XBT_DEBUG("Replace visited state %d with the new visited state %d",
               old_state->num, new_state->num);
 
-            simgrid::mc::visited_states[cursor] = std::move(new_state);
+            visited_state = std::move(new_state);
             return std::move(old_state);
           }
-          cursor++;
         }
       }
-      
-      XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
-      visited_states.insert(visited_states.begin() + min, std::move(new_state));
-
-    } else {
-
-      // The state has not been visited: insert the state in the dynamic array.
-      simgrid::mc::VisitedState* state_test = &*visited_states[index];
-      std::size_t position;
-      if (state_test->nb_processes < new_state->nb_processes)
-        position = index + 1;
-      else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
-        position = index + 1;
-      else
-        position = index;
-      visited_states.insert(visited_states.begin() + position, std::move(new_state));
-      XBT_DEBUG("Insert new visited state %d (total : %lu)",
-        visited_states[index]->num,
-        (unsigned long) visited_states.size());
-
-    }
-
-  if (visited_states.size() <= (std::size_t) _sg_mc_visited)
-    return nullptr;
 
-  // We have reached the maximum number of stored states;
-
-      XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
-
-      // Find the (index of the) older state (with the smallest num):
-      int min2 = mc_stats->expanded_states;
-      unsigned int index2 = 0;
-
-      for (std::size_t cursor2 = 0; cursor2 != visited_states.size(); ++cursor2)
-        if (!mc_model_checker->is_important_snapshot(
-              *visited_states[cursor2]->system_state)
-            && visited_states[cursor2]->num < min2) {
-          index2 = cursor2;
-          min2 = visited_states[cursor2]->num;
-        }
-
-      // and drop it:
-      visited_states.erase(visited_states.begin() + index2);
-      XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
-
-    return nullptr;
-}
-
-/**
- * \brief Checks whether a given pair has already been visited by the algorithm.
- */
-int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
-
-  if (_sg_mc_visited == 0)
-    return -1;
-
-  simgrid::mc::VisitedPair* new_visited_pair = nullptr;
-  if (visited_pair == nullptr)
-    new_visited_pair = new simgrid::mc::VisitedPair(
-      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
-      pair->graph_state);
-  else
-    new_visited_pair = visited_pair;
-
-  if (xbt_dynar_is_empty(visited_pairs)) {
-    xbt_dynar_push(visited_pairs, &new_visited_pair);
-    return -1;
-  }
-
-    int min = -1, max = -1, index;
-    //int res;
-    simgrid::mc::VisitedPair* pair_test;
-    int cursor;
-
-    index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
-
-    if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
-      cursor = min;
-      while (cursor <= max) {
-        pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
-        if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
-          if (xbt_automaton_propositional_symbols_compare_value(
-              pair_test->atomic_propositions.get(),
-              new_visited_pair->atomic_propositions.get()) == 0) {
-            if (snapshot_compare(pair_test, new_visited_pair) == 0) {
-              if (pair_test->other_num == -1)
-                new_visited_pair->other_num = pair_test->num;
-              else
-                new_visited_pair->other_num = pair_test->other_num;
-              if (dot_output == nullptr)
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
-              else
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
-              xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
-              xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
-              pair_test->visited_removed = 1;
-              if (!pair_test->acceptance_pair
-                  || pair_test->acceptance_removed == 1)
-                delete pair_test;
-              return new_visited_pair->other_num;
-            }
-          }
-        }
-        cursor++;
-      }
-      xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
-    } else {
-      pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
-      if (pair_test->nb_processes < new_visited_pair->nb_processes)
-        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-      else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
-        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-      else
-        xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
-    }
-
-    if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
-      int min2 = mc_stats->expanded_pairs;
-      unsigned int cursor2 = 0;
-      unsigned int index2 = 0;
-      xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
-        if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
-            && pair_test->num < min2) {
-          index2 = cursor2;
-          min2 = pair_test->num;
-        }
-      }
-      xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
-      pair_test->visited_removed = 1;
-      if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
-        delete pair_test;
-    }
-  return -1;
+  XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
+  visited_states.insert(range.first, std::move(new_state));
+  prune_visited_states();
+  return nullptr;
 }
 
 }
diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 0c3a6f481e..b8b4b08e76 100644
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -12,24 +12,9 @@
 
 #include <utility>
 
-#include <fcntl.h>
-#include <signal.h>
-#include <poll.h>
-
 #include <unistd.h>
 
-#include <sys/types.h>
-#include <sys/socket.h>
-#include <sys/wait.h>
-#include <sys/ptrace.h>
-
-#ifdef __linux__
-#include <sys/prctl.h>
-#endif
-
 #include <xbt/log.h>
-#include <xbt/sysdep.h>
-#include <xbt/system_error.hpp>
 
 #include "simgrid/sg_config.h"
 #include "src/xbt_modinter.h"
@@ -41,99 +26,13 @@
 #include "src/mc/mc_comm_pattern.h"
 #include "src/mc/mc_liveness.h"
 #include "src/mc/mc_exit.h"
+#include "src/mc/Session.hpp"
+#include "src/mc/Checker.hpp"
+#include "src/mc/SafetyChecker.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 
-/** Execute some code in a forked process */
-template<class F>
 static inline
-pid_t do_fork(F f)
-{
-  pid_t pid = fork();
-  if (pid < 0)
-    throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
-  if (pid != 0)
-    return pid;
-
-  // Child-process:
-  try {
-    f();
-    _exit(EXIT_SUCCESS);
-  }
-  catch(...) {
-    // The callback should catch exceptions:
-    abort();
-  }
-}
-
-static
-int exec_model_checked(int socket, char** argv)
-{
-  XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
-
-#ifdef __linux__
-  // Make sure we do not outlive our parent:
-  sigset_t mask;
-  sigemptyset (&mask);
-  if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
-    throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
-  if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
-    throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
-#endif
-
-  int res;
-
-  // Remove CLOEXEC in order to pass the socket to the exec-ed program:
-  int fdflags = fcntl(socket, F_GETFD, 0);
-  if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
-    throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
-
-  // Set environment:
-  setenv(MC_ENV_VARIABLE, "1", 1);
-
-  // Disable lazy relocation in the model-checked process.
-  // We don't want the model-checked process to modify its .got.plt during
-  // snapshot.
-  setenv("LC_BIND_NOW", "1", 1);
-
-  char buffer[64];
-  res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
-  if ((size_t) res >= sizeof(buffer) || res == -1)
-    std::abort();
-  setenv(MC_ENV_SOCKET_FD, buffer, 1);
-
-  execvp(argv[1], argv+1);
-
-  XBT_ERROR("Could not run the model-checked program");
-  // This is the value used by system() and popen() in this case:
-  return 127;
-}
-
-static
-std::pair<pid_t, int> create_model_checked(char** argv)
-{
-  // Create a AF_LOCAL socketpair used for exchanging messages
-  // bewteen the model-checker process (ourselves) and the model-checked
-  // process:
-  int res;
-  int sockets[2];
-  res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
-  if (res == -1)
-    throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
-
-  pid_t pid = do_fork([&] {
-    close(sockets[1]);
-    int res = exec_model_checked(sockets[0], argv);
-    XBT_DEBUG("Error in the child process creation");
-    _exit(res);
-  });
-
-  // Parent (model-checker):
-  close(sockets[0]);
-  return std::make_pair(pid, sockets[1]);
-}
-
-static
 char** argvdup(int argc, char** argv)
 {
   char** argv_copy = xbt_new(char*, argc+1);
@@ -142,42 +41,54 @@ char** argvdup(int argc, char** argv)
   return argv_copy;
 }
 
+static
+std::unique_ptr<simgrid::mc::Checker> createChecker(simgrid::mc::Session& session)
+{
+  using simgrid::mc::Session;
+  using simgrid::mc::FunctionalChecker;
+
+  std::function<int(Session& session)> code;
+  if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+    code = [](Session& session) {
+      return MC_modelcheck_comm_determinism(); };
+  else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
+    return std::unique_ptr<simgrid::mc::Checker>(
+      new simgrid::mc::SafetyChecker(session));
+  else
+    code = [](Session& session) {
+      return simgrid::mc::modelcheck_liveness(); };
+
+  return std::unique_ptr<simgrid::mc::Checker>(
+    new FunctionalChecker(session, std::move(code)));
+}
+
 int main(int argc, char** argv)
 {
+  using simgrid::mc::Session;
+
   try {
     if (argc < 2)
       xbt_die("Missing arguments.\n");
 
+    // Currently, we need this before sg_config_init:
     _sg_do_model_check = 1;
+    mc_mode = MC_MODE_SERVER;
 
     // The initialisation function can touch argv.
-    // We need to keep the original parameters in order to pass them to the
-    // model-checked process so we make a copy of them:
-    int argc_copy = argc;
+    // We make a copy of argv before modifying it in order to pass the original
+    // value to the model-checked:
     char** argv_copy = argvdup(argc, argv);
-    xbt_log_init(&argc_copy, argv_copy);
-    sg_config_init(&argc_copy, argv_copy);
+    xbt_log_init(&argc, argv);
+    sg_config_init(&argc, argv);
 
-    int sock;
-    pid_t model_checked_pid;
-    std::tie(model_checked_pid, sock) = create_model_checked(argv);
-    XBT_DEBUG("Inside the parent process");
-    if (mc_model_checker)
-      xbt_die("MC server already present");
+    std::unique_ptr<Session> session =
+      std::unique_ptr<Session>(Session::spawnvp(argv_copy[1], argv_copy+1));
+    free(argv_copy);
 
-    mc_mode = MC_MODE_SERVER;
-    std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(model_checked_pid, sock));
-    process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
-    mc_model_checker = new simgrid::mc::ModelChecker(std::move(process));
-    mc_model_checker->start();
-    int res = 0;
-    if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
-      res = MC_modelcheck_comm_determinism();
-    else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
-      res = simgrid::mc::modelcheck_safety();
-    else
-      res = simgrid::mc::modelcheck_liveness();
-    mc_model_checker->shutdown();
+    simgrid::mc::session = session.get();
+    std::unique_ptr<simgrid::mc::Checker> checker = createChecker(*session);
+    int res = checker->run();
+    session->close();
     return res;
   }
   catch(std::exception& e) {
diff --git a/src/s4u/s4u_as.cpp b/src/s4u/s4u_as.cpp
index 60459e6d73..b0f760f50e 100644
--- a/src/s4u/s4u_as.cpp
+++ b/src/s4u/s4u_as.cpp
@@ -19,7 +19,7 @@ namespace simgrid {
     : name_(xbt_strdup(name))
     {
     }
-    void As::Seal()
+    void As::seal()
     {
       sealed_ = true;
     }
diff --git a/src/surf/AsDijkstra.cpp b/src/surf/AsDijkstra.cpp
index 3d542a510b..f18a2c517b 100644
--- a/src/surf/AsDijkstra.cpp
+++ b/src/surf/AsDijkstra.cpp
@@ -38,7 +38,7 @@ static void graph_edge_data_free(void *e) // FIXME: useless code duplication
 
 namespace simgrid {
 namespace surf {
-void AsDijkstra::Seal()
+void AsDijkstra::seal()
 {
   xbt_node_t node = NULL;
   unsigned int cursor2, cursor;
diff --git a/src/surf/AsDijkstra.hpp b/src/surf/AsDijkstra.hpp
index 346e20aa0c..081bffd9a1 100644
--- a/src/surf/AsDijkstra.hpp
+++ b/src/surf/AsDijkstra.hpp
@@ -33,7 +33,7 @@ namespace surf {
 class XBT_PRIVATE AsDijkstra : public AsRoutedGraph {
 public:
   AsDijkstra(const char*name, bool cached);
-  void Seal() override;
+  void seal() override;
 
   ~AsDijkstra();
   xbt_node_t routeGraphNewNode(int id, int graph_id);
diff --git a/src/surf/AsFloyd.cpp b/src/surf/AsFloyd.cpp
index 891675af67..960b039f34 100644
--- a/src/surf/AsFloyd.cpp
+++ b/src/surf/AsFloyd.cpp
@@ -149,7 +149,7 @@ void AsFloyd::addRoute(sg_platf_route_cbarg_t route)
   }
 }
 
-void AsFloyd::Seal(){
+void AsFloyd::seal(){
 
   /* set the size of table routing */
   size_t table_size = xbt_dynar_length(vertices_);
diff --git a/src/surf/AsFloyd.hpp b/src/surf/AsFloyd.hpp
index 39ba4371ec..4c04f39289 100644
--- a/src/surf/AsFloyd.hpp
+++ b/src/surf/AsFloyd.hpp
@@ -19,7 +19,7 @@ public:
 
   void getRouteAndLatency(NetCard *src, NetCard *dst, sg_platf_route_cbarg_t into, double *latency) override;
   void addRoute(sg_platf_route_cbarg_t route) override;
-  void Seal() override;
+  void seal() override;
 
 private:
   /* vars to compute the Floyd algorithm. */
diff --git a/src/surf/AsFull.cpp b/src/surf/AsFull.cpp
index 9f757613d5..37d3ff7709 100644
--- a/src/surf/AsFull.cpp
+++ b/src/surf/AsFull.cpp
@@ -17,7 +17,7 @@ namespace surf {
   {
   }
 
-void AsFull::Seal() {
+void AsFull::seal() {
   int i;
   sg_platf_route_cbarg_t e_route;
 
diff --git a/src/surf/AsFull.hpp b/src/surf/AsFull.hpp
index df5fee55ba..f91b021d91 100644
--- a/src/surf/AsFull.hpp
+++ b/src/surf/AsFull.hpp
@@ -16,7 +16,7 @@ class XBT_PRIVATE AsFull: public AsRoutedGraph {
 public:
 
   AsFull(const char*name);
-  void Seal() override;
+  void seal() override;
   ~AsFull();
 
   void getRouteAndLatency(NetCard *src, NetCard *dst, sg_platf_route_cbarg_t into, double *latency) override;
diff --git a/src/surf/network_ns3.cpp b/src/surf/network_ns3.cpp
index 6ede3c79de..99ca278708 100644
--- a/src/surf/network_ns3.cpp
+++ b/src/surf/network_ns3.cpp
@@ -189,17 +189,15 @@ static void create_ns3_topology(void)
 
   //get the onelinks from the parsed platform
   xbt_dynar_t onelink_routes = routing_platf->getOneLinkRoutes();
-  if (!onelink_routes)
-    xbt_die("There is no routes!");
-  XBT_DEBUG("Have get_onelink_routes, found %ld routes",onelink_routes->used);
+
+  XBT_DEBUG("There is %ld one-link routes",onelink_routes->used);
   //save them in trace file
   simgrid::surf::Onelink *onelink;
   unsigned int iter;
   xbt_dynar_foreach(onelink_routes, iter, onelink) {
     char *src = onelink->src_->name();
     char *dst = onelink->dst_->name();
-    simgrid::surf::LinkNS3 *link =
-      static_cast<simgrid::surf::LinkNS3 *>(onelink->link_);
+    simgrid::surf::LinkNS3 *link = static_cast<simgrid::surf::LinkNS3 *>(onelink->link_);
 
     if (strcmp(src,dst) && link->m_created){
       XBT_DEBUG("Route from '%s' to '%s' with link '%s'", src, dst, link->getName());
@@ -229,43 +227,15 @@ static void create_ns3_topology(void)
   }
 }
 
-static void parse_ns3_end_platform(void)
-{
-  ns3_end_platform();
-}
-
-static void define_callbacks_ns3(void)
-{
-  simgrid::s4u::Host::onCreation.connect(simgrid_ns3_add_host);
-  simgrid::surf::netcardCreatedCallbacks.connect(simgrid_ns3_add_router);
-  simgrid::surf::on_link.connect (parse_ns3_add_link);
-  simgrid::surf::on_cluster.connect (&parse_ns3_add_cluster);
-  simgrid::surf::asCreatedCallbacks.connect(parse_ns3_add_AS);
-  simgrid::surf::on_postparse.connect(&create_ns3_topology); //get_one_link_routes
-  simgrid::surf::on_postparse.connect(&parse_ns3_end_platform); //InitializeRoutes
-}
-
 /*********
  * Model *
  *********/
-static void free_ns3_link(void * elmts)
-{
-  delete static_cast<simgrid::surf::LinkNS3*>(elmts);
-}
-
-static void free_ns3_host(void * elmts)
-{
-  ns3_node_t host = static_cast<ns3_node_t>(elmts);
-  free(host);
-}
-
 void surf_network_model_init_NS3()
 {
   if (surf_network_model)
     return;
 
   surf_network_model = new simgrid::surf::NetworkNS3Model();
-
   xbt_dynar_push(all_existing_models, &surf_network_model);
 }
 
@@ -277,10 +247,16 @@ NetworkNS3Model::NetworkNS3Model() : NetworkModel() {
     xbt_die("Impossible to initialize NS3 interface");
   }
   routing_model_create(NULL);
-  define_callbacks_ns3();
+  simgrid::s4u::Host::onCreation.connect(simgrid_ns3_add_host);
+  simgrid::surf::netcardCreatedCallbacks.connect(simgrid_ns3_add_router);
+  simgrid::surf::on_link.connect (parse_ns3_add_link);
+  simgrid::surf::on_cluster.connect (&parse_ns3_add_cluster);
+  simgrid::surf::asCreatedCallbacks.connect(parse_ns3_add_AS);
+  simgrid::surf::on_postparse.connect(&create_ns3_topology); //get_one_link_routes
+  simgrid::surf::on_postparse.connect(&ns3_end_platform); //InitializeRoutes
 
-  NS3_EXTENSION_ID = simgrid::s4u::Host::extension_create(free_ns3_host);
-  NS3_ASR_LEVEL  = xbt_lib_add_level(as_router_lib, free_ns3_host);
+  NS3_EXTENSION_ID = simgrid::s4u::Host::extension_create(xbt_free_f);
+  NS3_ASR_LEVEL  = xbt_lib_add_level(as_router_lib, xbt_free_f);
 }
 
 NetworkNS3Model::~NetworkNS3Model() {
diff --git a/src/surf/sg_platf.cpp b/src/surf/sg_platf.cpp
index 51315f589a..e3898d17b7 100644
--- a/src/surf/sg_platf.cpp
+++ b/src/surf/sg_platf.cpp
@@ -948,7 +948,7 @@ void sg_platf_new_AS_begin(sg_platf_AS_cbarg_t AS)
 void sg_platf_new_AS_end()
 {
   xbt_assert(current_routing, "Cannot seal the current AS: none under construction");
-  current_routing->Seal();
+  current_routing->seal();
   current_routing = static_cast<simgrid::surf::AsImpl*>(current_routing->father());
 
   if (TRACE_is_enabled())
diff --git a/src/xbt/automaton/automatonparse_promela.c b/src/xbt/automaton/automatonparse_promela.c
index d62c20dabd..b86bf6e470 100644
--- a/src/xbt/automaton/automatonparse_promela.c
+++ b/src/xbt/automaton/automatonparse_promela.c
@@ -19,8 +19,8 @@ char* state_id_src;
 
 static void new_state(char* id, int src){
 
-  char* id_state = xbt_strdup(id);
-  char* first_part = strtok(id,"_");
+  char* id_copy = xbt_strdup(id);
+  char* first_part = strtok(id_copy,"_");
   int type = 0 ; // -1=initial state; 0=intermediate state; 1=final state
 
   if(strcmp(first_part,"accept")==0){
@@ -31,27 +31,29 @@ static void new_state(char* id, int src){
       type = -1;
     }
   }
+  free(id_copy);
 
   xbt_automaton_state_t state = NULL;
-  state = xbt_automaton_state_exists(parsed_automaton, id_state);
+  state = xbt_automaton_state_exists(parsed_automaton, id);
   if(state == NULL){
-    state = xbt_automaton_state_new(parsed_automaton, type, id_state);
+    state = xbt_automaton_state_new(parsed_automaton, type, id);
   }
 
   if(type==-1)
     parsed_automaton->current_state = state;
 
-  if(src)
-    state_id_src = xbt_strdup(id_state);
-    
+  if(src) {
+    if (state_id_src)
+      free(state_id_src);
+    state_id_src = xbt_strdup(id);
+  }
 }
 
-static void new_transition(char* id, xbt_automaton_exp_label_t label){
-
-  char* id_state = xbt_strdup(id);
+static void new_transition(char* id, xbt_automaton_exp_label_t label)
+{
   xbt_automaton_state_t state_dst = NULL;
   new_state(id, 0);
-  state_dst = xbt_automaton_state_exists(parsed_automaton, id_state);
+  state_dst = xbt_automaton_state_exists(parsed_automaton, id);
   xbt_automaton_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);
   
   //xbt_transition_t trans = NULL;
diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index e61786de28..bb79408e80 100644
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -550,6 +550,8 @@ set(MC_SRC
   src/mc/AddressSpace.cpp
   src/mc/Channel.cpp
   src/mc/Channel.hpp
+  src/mc/Checker.cpp
+  src/mc/Checker.hpp
   src/mc/Client.cpp
   src/mc/Client.hpp
   src/mc/Frame.hpp
@@ -560,6 +562,8 @@ set(MC_SRC
   src/mc/ObjectInformation.cpp
   src/mc/PageStore.hpp
   src/mc/PageStore.cpp
+  src/mc/SafetyChecker.cpp
+  src/mc/SafetyChecker.hpp
   src/mc/ChunkedData.hpp
   src/mc/ChunkedData.cpp
   src/mc/RegionSnapshot.cpp
@@ -570,6 +574,8 @@ set(MC_SRC
   src/mc/mc_forward.hpp
   src/mc/Process.hpp
   src/mc/Process.cpp
+  src/mc/Session.cpp
+  src/mc/Session.hpp
   src/mc/mc_unw.h
   src/mc/mc_unw.cpp
   src/mc/mc_unw_vmread.cpp
@@ -604,7 +610,6 @@ set(MC_SRC
   src/mc/mc_request.h
   src/mc/mc_request.cpp
   src/mc/mc_safety.h
-  src/mc/mc_safety.cpp
   src/mc/mc_state.h
   src/mc/mc_state.cpp
   src/mc/mc_visited.cpp