Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
That was a nasty optimization :-/
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Mon, 8 Mar 2021 19:51:01 +0000 (20:51 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Mon, 8 Mar 2021 19:51:01 +0000 (20:51 +0100)
src/mc/api.cpp
src/mc/api.hpp
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp
src/mc/mc_request.hpp

index 286f3e4..4bc2330 100644 (file)
@@ -171,14 +171,12 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta
     case Simcall::COMM_WAIT:
       chosen_comm = simcall_comm_wait__getraw__comm(req);
       mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(chosen_comm));
-      simcall_comm_wait__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
       simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
       break;
 
     case Simcall::COMM_TEST:
       chosen_comm = simcall_comm_test__getraw__comm(req);
       mc_model_checker->get_remote_simulation().read(remote_comm, remote(chosen_comm));
-      simcall_comm_test__set__comm(&state->executed_req_, remote_comm.get_buffer());
       simcall_comm_test__set__comm(&state->internal_req_, remote_comm.get_buffer());
       break;
 
@@ -699,23 +697,10 @@ bool Api::simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const
   }
 }
 
-std::string Api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const
+std::string Api::request_to_string(smx_simcall_t req, int value) const
 {
   xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
 
-  bool use_remote_comm = true;
-  switch (request_type) {
-    case simgrid::mc::RequestType::simix:
-      use_remote_comm = true;
-      break;
-    case simgrid::mc::RequestType::executed:
-    case simgrid::mc::RequestType::internal:
-      use_remote_comm = false;
-      break;
-    default:
-      THROW_IMPOSSIBLE;
-  }
-
   std::string type;
   std::string args;
 
@@ -755,11 +740,8 @@ std::string Api::request_to_string(smx_simcall_t req, int value, RequestType req
 
         simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_synchro;
         const simgrid::kernel::activity::CommImpl* act;
-        if (use_remote_comm) {
-          mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
-          act = temp_synchro.get_buffer();
-        } else
-          act = remote_act;
+        mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
+        act = temp_synchro.get_buffer();
 
         smx_actor_t src_proc =
             mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
@@ -775,11 +757,8 @@ std::string Api::request_to_string(smx_simcall_t req, int value, RequestType req
       simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_test__getraw__comm(req);
       simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_synchro;
       const simgrid::kernel::activity::CommImpl* act;
-      if (use_remote_comm) {
-        mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
-        act = temp_synchro.get_buffer();
-      } else
-        act = remote_act;
+      mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
+      act = temp_synchro.get_buffer();
 
       if (act->src_actor_.get() == nullptr || act->dst_actor_.get() == nullptr) {
         type = "Test FALSE";
@@ -982,7 +961,7 @@ void Api::restore_initial_state() const
 void Api::execute(Transition& transition, smx_simcall_t simcall) const
 {
   /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
-  transition.textual = request_to_string(simcall, transition.times_considered_, RequestType::executed);
+  transition.textual = request_to_string(simcall, transition.times_considered_);
   session->execute(transition);
 }
 
index 837f982..55d66d9 100644 (file)
@@ -110,7 +110,7 @@ public:
   std::list<transition_detail_t> get_enabled_transitions(simgrid::mc::State* state) const;
 
   // SIMCALL APIs
-  std::string request_to_string(smx_simcall_t req, int value, RequestType request_type) const;
+  std::string request_to_string(smx_simcall_t req, int value) const;
   std::string request_get_dot_output(smx_simcall_t req, int value) const;
   smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const;
   long simcall_get_actor_id(s_smx_simcall const* req) const;
index 5192439..d54bfb6 100644 (file)
@@ -271,7 +271,7 @@ std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() //
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
     smx_simcall_t req = &state->executed_req_;
-    trace.push_back(api::get().request_to_string(req, state->transition_.times_considered_, RequestType::executed));
+    trace.push_back(api::get().request_to_string(req, state->transition_.times_considered_));
   }
   return trace;
 }
@@ -430,7 +430,7 @@ void CommunicationDeterminismChecker::real_run()
     if (req != nullptr && visited_state == nullptr) {
       int req_num = cur_state->transition_.times_considered_;
 
-      XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num, RequestType::simix).c_str());
+      XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num).c_str());
 
       std::string req_str;
       if (dot_output != nullptr)
index 3171b6d..a1b2ca6 100644 (file)
@@ -139,8 +139,8 @@ void LivenessChecker::replay()
       req                      = &issuer->simcall_;
 
       /* Debug information */
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                api::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, api::get().request_to_string(req, req_num).c_str(),
+                state.get());
 
       api::get().execute(state->transition_, req);
     }
@@ -241,7 +241,7 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
     int req_num       = pair->graph_state->transition_.times_considered_;
     smx_simcall_t req = &pair->graph_state->executed_req_;
     if (req->call_ != simix::Simcall::NONE)
-      trace.push_back(api::get().request_to_string(req, req_num, RequestType::executed));
+      trace.push_back(api::get().request_to_string(req, req_num));
   }
   return trace;
 }
@@ -374,7 +374,7 @@ void LivenessChecker::run()
       fflush(dot_output);
     }
 
-    XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num, RequestType::simix).c_str());
+    XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num).c_str());
 
     /* Update stats */
     api::get().mc_inc_executed_trans();
index 75be763..0feca33 100644 (file)
@@ -120,8 +120,7 @@ void SafetyChecker::run()
 
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
-    XBT_DEBUG("Execute: %s",
-              api::get().request_to_string(req, state->transition_.times_considered_, RequestType::simix).c_str());
+    XBT_DEBUG("Execute: %s", api::get().request_to_string(req, state->transition_.times_considered_).c_str());
 
     std::string req_str;
     if (dot_output != nullptr)
@@ -202,12 +201,10 @@ void SafetyChecker::backtrack()
             XBT_DEBUG("Dependent Transitions:");
             int value              = prev_state->transition_.times_considered_;
             smx_simcall_t prev_req = &prev_state->executed_req_;
-            XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value, RequestType::internal).c_str(),
-                      prev_state->num_);
+            XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value).c_str(), prev_state->num_);
             value    = state->transition_.times_considered_;
             prev_req = &state->executed_req_;
-            XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value, RequestType::executed).c_str(),
-                      state->num_);
+            XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value).c_str(), state->num_);
           }
 
           if (not prev_state->actor_states_[issuer->get_pid()].is_done())
index ca980d7..528d97a 100644 (file)
 namespace simgrid {
 namespace mc {
 
-enum class RequestType {
-  simix,
-  executed,
-  internal,
-};
-
 XBT_PRIVATE bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
 }
 }