Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
cosmetics to make the SafetyChecker even easier to read
[simgrid.git] / src / mc / CommunicationDeterminismChecker.cpp
index 6b6a331..2449b6c 100644 (file)
@@ -22,6 +22,7 @@
 #include "src/mc/CommunicationDeterminismChecker.hpp"
 #include "src/mc/mc_exit.h"
 #include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
 
 using simgrid::mc::remote;
 
@@ -35,7 +36,8 @@ xbt_dynar_t incomplete_communications_pattern;
 
 /********** Static functions ***********/
 
-static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) {
+static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
+{
   if(comm1->type != comm2->type)
     return TYPE_DIFF;
   if (comm1->rdv != comm2->rdv)
@@ -56,7 +58,7 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternC
 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
   char *type, *res;
 
-  if(comm->type == SIMIX_COMM_SEND)
+  if (comm->type == simgrid::mc::PatternCommunicationType::send)
     type = bprintf("The send communications pattern of the process %d is different!", process - 1);
   else
     type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
@@ -91,30 +93,38 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p
   return res;
 }
 
-static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
+static void update_comm_pattern(
+  simgrid::mc::PatternCommunication* comm_pattern,
+  simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
 {
-  s_smx_synchro_t comm;
-  mc_model_checker->process().read(&comm, remote(comm_addr));
+  // HACK, type punning
+  simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+  mc_model_checker->process().read(temp_comm, comm_addr);
+  simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
 
-  smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
-  smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
+  smx_actor_t src_proc   = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
+  smx_actor_t dst_proc   = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
   comm_pattern->src_proc = src_proc->pid;
   comm_pattern->dst_proc = dst_proc->pid;
-  comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
-  comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
-  if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
+  comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
+  comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
+  if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
     size_t buff_size;
     mc_model_checker->process().read(
-      &buff_size, remote(comm.comm.dst_buff_size));
+      &buff_size, remote(comm->dst_buff_size));
     comm_pattern->data.resize(buff_size);
     mc_model_checker->process().read_bytes(
       comm_pattern->data.data(), comm_pattern->data.size(),
-      remote(comm.comm.src_buff));
+      remote(comm->src_buff));
   }
 }
 
-static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
+namespace simgrid {
+namespace mc {
 
+void CommunicationDeterminismChecker::deterministic_comm_pattern(
+  int process, simgrid::mc::PatternCommunication* comm, int backtracking)
+{
   simgrid::mc::PatternCommunicationList* list =
     xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
 
@@ -123,39 +133,38 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic
       compare_comm_pattern(list->list[list->index_comm].get(), comm);
 
     if (diff != NONE_DIFF) {
-      if (comm->type == SIMIX_COMM_SEND){
-        simgrid::mc::initial_global_state->send_deterministic = 0;
-        if(simgrid::mc::initial_global_state->send_diff != nullptr)
-          xbt_free(simgrid::mc::initial_global_state->send_diff);
-        simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
-      }else{
-        simgrid::mc::initial_global_state->recv_deterministic = 0;
-        if(simgrid::mc::initial_global_state->recv_diff != nullptr)
-          xbt_free(simgrid::mc::initial_global_state->recv_diff);
-        simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+      if (comm->type == simgrid::mc::PatternCommunicationType::send) {
+        this->send_deterministic = 0;
+        if (this->send_diff != nullptr)
+          xbt_free(this->send_diff);
+        this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+      } else {
+        this->recv_deterministic = 0;
+        if (this->recv_diff != nullptr)
+          xbt_free(this->recv_diff);
+        this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
       }
-      if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
+      if(_sg_mc_send_determinism && !this->send_deterministic){
         XBT_INFO("*********************************************************");
         XBT_INFO("***** Non-send-deterministic communications pattern *****");
         XBT_INFO("*********************************************************");
-        XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
-        xbt_free(simgrid::mc::initial_global_state->send_diff);
-        simgrid::mc::initial_global_state->send_diff = nullptr;
-        MC_print_statistics(mc_stats);
+        XBT_INFO("%s", this->send_diff);
+        xbt_free(this->send_diff);
+        this->send_diff = nullptr;
+        simgrid::mc::session->logState();
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       }else if(_sg_mc_comms_determinism
-          && (!simgrid::mc::initial_global_state->send_deterministic
-            && !simgrid::mc::initial_global_state->recv_deterministic)) {
+          && (!this->send_deterministic && !this->recv_deterministic)) {
         XBT_INFO("****************************************************");
         XBT_INFO("***** Non-deterministic communications pattern *****");
         XBT_INFO("****************************************************");
-        XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
-        XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
-        xbt_free(simgrid::mc::initial_global_state->send_diff);
-        simgrid::mc::initial_global_state->send_diff = nullptr;
-        xbt_free(simgrid::mc::initial_global_state->recv_diff);
-        simgrid::mc::initial_global_state->recv_diff = nullptr;
-        MC_print_statistics(mc_stats);
+        XBT_INFO("%s", this->send_diff);
+        XBT_INFO("%s", this->recv_diff);
+        xbt_free(this->send_diff);
+        this->send_diff = nullptr;
+        xbt_free(this->recv_diff);
+        this->recv_diff = nullptr;
+        simgrid::mc::session->logState();
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       }
     }
@@ -164,9 +173,9 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic
 
 /********** Non Static functions ***********/
 
-void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
+void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 {
-  const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
+  const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
   simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
     initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
   xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
@@ -180,31 +189,34 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
 
   if (call_type == MC_CALL_TYPE_SEND) {
     /* Create comm pattern */
-    pattern->type = SIMIX_COMM_SEND;
+    pattern->type = simgrid::mc::PatternCommunicationType::send;
     pattern->comm_addr = simcall_comm_isend__get__result(request);
 
-    s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
-      (std::uint64_t) pattern->comm_addr);
+    simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
+    mc_model_checker->process().read(temp_synchro, remote(
+      static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
+    simgrid::kernel::activity::Comm* synchro =
+      static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
 
     char* remote_name = mc_model_checker->process().read<char*>(
-      (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+      (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name));
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
-    pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
-    pattern->src_host = MC_smx_process_get_host_name(issuer);
+    pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid;
+    pattern->src_host = MC_smx_actor_get_host_name(issuer);
 
     struct s_smpi_mpi_request mpi_request =
       mc_model_checker->process().read<s_smpi_mpi_request>(
         (std::uint64_t) simcall_comm_isend__get__data(request));
     pattern->tag = mpi_request.tag;
 
-    if(synchro.comm.src_buff != nullptr){
-      pattern->data.resize(synchro.comm.src_buff_size);
+    if (synchro->src_buff != nullptr){
+      pattern->data.resize(synchro->src_buff_size);
       mc_model_checker->process().read_bytes(
         pattern->data.data(), pattern->data.size(),
-        remote(synchro.comm.src_buff));
+        remote(synchro->src_buff));
     }
     if(mpi_request.detached){
-      if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
+      if (!this->initial_communications_pattern_done) {
         /* Store comm pattern */
         simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
           initial_communications_pattern, pattern->src_proc,
@@ -212,7 +224,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
         list->list.push_back(std::move(pattern));
       } else {
         /* Evaluate comm determinism */
-        deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
+        this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
         xbt_dynar_get_as(
           initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
         )->index_comm++;
@@ -220,7 +232,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
       return;
     }
   } else if (call_type == MC_CALL_TYPE_RECV) {
-    pattern->type = SIMIX_COMM_RECEIVE;
+    pattern->type = simgrid::mc::PatternCommunicationType::receive;
     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 
     struct s_smpi_mpi_request mpi_request;
@@ -228,15 +240,17 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
       &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
     pattern->tag = mpi_request.tag;
 
-    s_smx_synchro_t synchro;
-    mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
+    simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+    mc_model_checker->process().read(temp_comm, remote(
+      static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
+    simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
 
     char* remote_name;
     mc_model_checker->process().read(&remote_name,
-      remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+      remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
-    pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
-    pattern->dst_host = MC_smx_process_get_host_name(issuer);
+    pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
+    pattern->dst_host = MC_smx_actor_get_host_name(issuer);
   } else
     xbt_die("Unexpected call_type %i", (int) call_type);
 
@@ -248,7 +262,11 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
   xbt_dynar_push(dynar, &pattern2);
 }
 
-void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
+
+void CommunicationDeterminismChecker::complete_comm_pattern(
+  xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
+  unsigned int issuer, int backtracking)
+{
   simgrid::mc::PatternCommunication* current_comm_pattern;
   unsigned int cursor = 0;
   std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
@@ -256,7 +274,7 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
 
   /* Complete comm pattern */
   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
-    if (current_comm_pattern->comm_addr == comm_addr) {
+    if (remote(current_comm_pattern->comm_addr) == comm_addr) {
       update_comm_pattern(current_comm_pattern, comm_addr);
       completed = 1;
       simgrid::mc::PatternCommunication* temp;
@@ -274,22 +292,16 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
   simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
     initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
 
-  if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
+  if (!this->initial_communications_pattern_done)
     /* Store comm pattern */
     pattern->list.push_back(std::move(comm_pattern));
   else {
     /* Evaluate comm determinism */
-    deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
+    this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
     pattern->index_comm++;
   }
 }
 
-
-/************************ Main algorithm ************************/
-
-namespace simgrid {
-namespace mc {
-
 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
   : Checker(session)
 {
@@ -301,29 +313,53 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 
 }
 
-// TODO, deduplicate with SafetyChecker
 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 {
   RecordTrace res;
   for (auto const& state : stack_)
-    res.push_back(state->getRecordElement());
+    res.push_back(state->getTransition());
   return res;
 }
 
-// TODO, deduplicate with SafetyChecker
 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
-    int value;
-    smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
+    smx_simcall_t req = &state->executed_req;
     if (req)
       trace.push_back(simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::executed));
+        req, state->transition.argument, simgrid::mc::RequestType::executed));
   }
   return trace;
 }
 
+void CommunicationDeterminismChecker::logState() // override
+{
+  Checker::logState();
+  if (_sg_mc_comms_determinism &&
+      !this->recv_deterministic &&
+      this->send_deterministic) {
+    XBT_INFO("******************************************************");
+    XBT_INFO("**** Only-send-deterministic communication pattern ****");
+    XBT_INFO("******************************************************");
+    XBT_INFO("%s", this->recv_diff);
+  } else if(_sg_mc_comms_determinism &&
+      !this->send_deterministic &&
+      this->recv_deterministic) {
+    XBT_INFO("******************************************************");
+    XBT_INFO("**** Only-recv-deterministic communication pattern ****");
+    XBT_INFO("******************************************************");
+    XBT_INFO("%s", this->send_diff);
+  }
+  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+  XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+  XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
+  if (_sg_mc_comms_determinism)
+    XBT_INFO("Recv-deterministic : %s",
+      !this->recv_deterministic ? "No" : "Yes");
+}
+
 void CommunicationDeterminismChecker::prepare()
 {
 
@@ -345,17 +381,14 @@ void CommunicationDeterminismChecker::prepare()
   }
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new());
+      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
-  /* Wait for requests (schedules processes) */
-  mc_model_checker->wait_for_requests();
-
-  /* Get an enabled process and insert it in the interleave set of the initial state */
-  for (auto& p : mc_model_checker->process().simix_processes())
-    if (simgrid::mc::process_is_enabled(&p.copy))
-      initial_state->interleave(&p.copy);
+  /* Get an enabled actor and insert it in the interleave set of the initial state */
+  for (auto& actor : mc_model_checker->process().actors())
+    if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
+      initial_state->interleave(actor.copy.getBuffer());
 
   stack_.push_back(std::move(initial_state));
 }
@@ -363,9 +396,8 @@ void CommunicationDeterminismChecker::prepare()
 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);
+  for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
+    xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, 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;
@@ -374,9 +406,59 @@ bool all_communications_are_finished()
   return true;
 }
 
+void CommunicationDeterminismChecker::restoreState()
+{
+  /* Intermediate backtracking */
+  {
+    simgrid::mc::State* state = stack_.back().get();
+    if (state->system_state) {
+      simgrid::mc::restore_snapshot(state->system_state);
+      MC_restore_communications_pattern(state);
+      return;
+    }
+  }
+
+  /* Restore the initial state */
+  simgrid::mc::session->restoreInitialState();
+
+  // int n = xbt_dynar_length(incomplete_communications_pattern);
+  unsigned n = MC_smx_get_maxpid();
+  assert(n == xbt_dynar_length(incomplete_communications_pattern));
+  assert(n == xbt_dynar_length(initial_communications_pattern));
+  for (unsigned j=0; j < n ; j++) {
+    xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+    xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
+  }
+
+  /* Traverse the stack from the state at position start and re-execute the transitions */
+  for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
+    if (state == stack_.back())
+      break;
+
+    int req_num = state->transition.argument;
+    smx_simcall_t saved_req = &state->executed_req;
+    xbt_assert(saved_req);
+
+    /* 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_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+    smx_simcall_t req = &issuer->simcall;
+
+    /* TODO : handle test and testany simcalls */
+    e_mc_call_type_t call = MC_get_call_type(req);
+    mc_model_checker->handle_simcall(state->transition);
+    MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
+    mc_model_checker->wait_for_requests();
+
+    /* Update statistics */
+    mc_model_checker->visited_states++;
+    mc_model_checker->executed_transitions++;
+  }
+}
+
 int CommunicationDeterminismChecker::main(void)
 {
-  int value;
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
   smx_simcall_t req = nullptr;
 
@@ -391,21 +473,23 @@ int CommunicationDeterminismChecker::main(void)
               state->interleaveSize());
 
     /* Update statistics */
-    mc_stats->visited_states++;
+    mc_model_checker->visited_states++;
 
     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
-        && (req = MC_state_get_request(state, &value))
+        && (req = MC_state_get_request(state)) != nullptr
         && (visited_state == nullptr)) {
 
+      int req_num = state->transition.argument;
+
       XBT_DEBUG("Execute: %s",
         simgrid::mc::request_to_string(
-          req, value, simgrid::mc::RequestType::simix).c_str());
+          req, req_num, simgrid::mc::RequestType::simix).c_str());
 
       std::string req_str;
       if (dot_output != nullptr)
-        req_str = simgrid::mc::request_get_dot_output(req, value);
+        req_str = simgrid::mc::request_get_dot_output(req, req_num);
 
-      mc_stats->executed_transitions++;
+      mc_model_checker->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */
       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
@@ -413,34 +497,36 @@ int CommunicationDeterminismChecker::main(void)
         call = MC_get_call_type(req);
 
       /* Answer the request */
-      simgrid::mc::handle_simcall(req, value);    /* After this call req is no longer useful */
+      mc_model_checker->handle_simcall(state->transition);
+      /* After this call req is no longer useful */
 
-      if(!initial_global_state->initial_communications_pattern_done)
-        MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+      if (!this->initial_communications_pattern_done)
+        MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
       else
-        MC_handle_comm_pattern(call, req, value, nullptr, 0);
+        MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
 
       /* Wait for requests (schedules processes) */
       mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
       std::unique_ptr<simgrid::mc::State> next_state =
-        std::unique_ptr<simgrid::mc::State>(MC_state_new());
+          std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
       /* If comm determinism verification, we cannot stop the exploration if
-         some communications are not finished (at least, data are transfered).
+         some communications are not finished (at least, data are transferred).
          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;
+        && this->initial_communications_pattern_done;
 
       if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
+          || (visited_state = visitedStates_.addVisitedState(
+            expandedStatesCount_, next_state.get(), 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())
-          if (simgrid::mc::process_is_enabled(&p.copy))
-            next_state->interleave(&p.copy);
+        /* Get enabled actors and insert them in the interleave set of the next state */
+        for (auto& actor : mc_model_checker->process().actors())
+          if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
+            next_state->interleave(actor.copy.getBuffer());
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
@@ -462,8 +548,8 @@ int CommunicationDeterminismChecker::main(void)
         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
           stack_.size());
 
-      if (!initial_global_state->initial_communications_pattern_done)
-        initial_global_state->initial_communications_pattern_done = 1;
+      if (!this->initial_communications_pattern_done)
+        this->initial_communications_pattern_done = 1;
 
       /* Trash the current state, no longer needed */
       XBT_DEBUG("Delete state %d at depth %zi",
@@ -488,7 +574,7 @@ int CommunicationDeterminismChecker::main(void)
             state->num, stack_.size() + 1);
           stack_.push_back(std::move(state));
 
-          simgrid::mc::replay(stack_);
+          this->restoreState();
 
           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
             stack_.back()->num, stack_.size());
@@ -502,27 +588,24 @@ int CommunicationDeterminismChecker::main(void)
     }
   }
 
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
 int CommunicationDeterminismChecker::run()
 {
   XBT_INFO("Check communication determinism");
-  mc_model_checker->wait_for_requests();
+  simgrid::mc::session->initialize();
 
   this->prepare();
 
-  initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
-  initial_global_state->initial_communications_pattern_done = 0;
-  initial_global_state->recv_deterministic = 1;
-  initial_global_state->send_deterministic = 1;
-  initial_global_state->recv_diff = nullptr;
-  initial_global_state->send_diff = nullptr;
+  this->initial_communications_pattern_done = 0;
+  this->recv_deterministic = 1;
+  this->send_deterministic = 1;
+  this->recv_diff = nullptr;
+  this->send_diff = nullptr;
 
   int res = this->main();
-  initial_global_state = nullptr;
   return res;
 }
 
@@ -532,4 +615,4 @@ Checker* createCommunicationDeterminismChecker(Session& session)
 }
 
 }
-}
\ No newline at end of file
+}