Merge branch 'master' of framagit.org:simgrid/simgrid

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index a1dd5f6..cee3dcc 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -170,14 +170,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;
 
@@ -701,23 +699,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;
 
@@ -757,11 +742,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()));
@@ -777,11 +759,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";
@@ -973,7 +952,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);
 }
 

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 837f982..55d66d9 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -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;

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 9d8cb16..4c131c9 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -272,7 +272,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;
 }
@@ -431,7 +431,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)

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 3171b6d..a1b2ca6 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -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();

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index c54759c..4198071 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -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)
@@ -186,43 +185,38 @@ void SafetyChecker::backtrack()
     std::unique_ptr<State> state = std::move(stack_.back());
     stack_.pop_back();
     if (reductionMode_ == ReductionMode::dpor) {
-      smx_simcall_t req = &state->internal_req_;
-      // FIXME: need something less ugly than this substring search
-      if (req->call_ == simix::Simcall::MUTEX_LOCK ||
-          (req->observer_ &&
-           api::get().request_to_string(req, 0, RequestType::internal).find("Mutex") != std::string::npos))
+      auto call = state->executed_req_.call_;
+      const kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_);
+      if (call == simix::Simcall::MUTEX_LOCK)
         xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
 
-      const kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(req);
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
-        if (api::get().simcall_check_dependency(req, &prev_state->internal_req_)) {
+        if (state->executed_req_.issuer_ == prev_state->executed_req_.issuer_) {
+          XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(call),
+                    SIMIX_simcall_name(prev_state->executed_req_.call_));
+          break;
+        } else if (api::get().simcall_check_dependency(&state->internal_req_, &prev_state->internal_req_)) {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             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())
             prev_state->mark_todo(issuer);
           else
-            XBT_DEBUG("Process %p is in done set", req->issuer_);
-          break;
-        } else if (req->issuer_ == prev_state->internal_req_.issuer_) {
-          XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_),
-                    SIMIX_simcall_name(prev_state->internal_req_.call_));
+            XBT_DEBUG("Actor %s %ld is in done set", issuer->get_cname(), issuer->get_pid());
           break;
         } else {
-          const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->internal_req_);
+          const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->executed_req_);
           XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
-                    SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_,
-                    SIMIX_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
+                    SIMIX_simcall_name(call), issuer->get_pid(), state->num_,
+                    SIMIX_simcall_name(prev_state->executed_req_.call_), previous_issuer->get_pid(), prev_state->num_);
         }
       }
     }

diff --git a/src/mc/mc_request.hpp b/src/mc/mc_request.hpp
index ca980d7..528d97a 100644 (file)
--- a/src/mc/mc_request.hpp
+++ b/src/mc/mc_request.hpp
@@ -11,12 +11,6 @@
 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);
 }
 }