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 9f03fe9..2449b6c 100644 (file)
@@ -100,17 +100,14 @@ static void update_comm_pattern(
   // 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 =
-    static_cast<simgrid::kernel::activity::Comm*>(temp_comm.getBuffer());
+  simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
 
-  smx_actor_t src_proc = mc_model_checker->process().resolveProcess(
-    simgrid::mc::remote(comm->src_proc));
-  smx_actor_t dst_proc = mc_model_checker->process().resolveProcess(
-    simgrid::mc::remote(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);
+  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(
@@ -204,9 +201,8 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
     char* remote_name = mc_model_checker->process().read<char*>(
       (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_model_checker->process().resolveProcess(
-      simgrid::mc::remote(synchro->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>(
@@ -253,9 +249,8 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim
     mc_model_checker->process().read(&remote_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_model_checker->process().resolveProcess(
-      simgrid::mc::remote(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);
 
@@ -386,14 +381,14 @@ void CommunicationDeterminismChecker::prepare()
   }
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
-  /* 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.getBuffer()))
-      initial_state->interleave(p.copy.getBuffer());
+  /* 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));
 }
@@ -401,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;
@@ -516,7 +510,7 @@ int CommunicationDeterminismChecker::main(void)
 
       /* Create the new expanded state */
       std::unique_ptr<simgrid::mc::State> next_state =
-        std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+          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 transferred).
@@ -529,10 +523,10 @@ int CommunicationDeterminismChecker::main(void)
           || (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.getBuffer()))
-            next_state->interleave(p.copy.getBuffer());
+        /* 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",