Merge remote-tracking branch 'github/master'

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index fa49142..adf130e 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -23,7 +23,7 @@ namespace mc {
 VisitedState::VisitedState(unsigned long state_number) : num(state_number)
 {  
   this->heap_bytes_used = mcapi::get().get_remote_heap_bytes();
-  this->actors_count = mcapi::get().mc_get_remote_simulation().actors().size();
+  this->actors_count = mcapi::get().get_actors_size();
   this->system_state = std::make_shared<simgrid::mc::Snapshot>(state_number);
 }
 

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 9ac7aa3..e4f7e93 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -19,7 +19,6 @@
 
 #include <cstdint>
 
-using simgrid::mc::remote;
 using mcapi = simgrid::mc::mc_api;
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection");
@@ -52,6 +51,25 @@ static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc
   return CommPatternDifference::NONE;
 }
 
+static void patterns_copy(std::vector<simgrid::mc::PatternCommunication*>& dest,
+                             std::vector<simgrid::mc::PatternCommunication> const& source)
+{
+  dest.clear();
+  for (simgrid::mc::PatternCommunication const& comm : source) {
+    auto* copy_comm = new simgrid::mc::PatternCommunication(comm.dup());
+    dest.push_back(copy_comm);
+  }
+}
+
+static void restore_communications_pattern(simgrid::mc::State* state)
+{
+  for (unsigned i = 0; i < initial_communications_pattern.size(); i++)
+    initial_communications_pattern[i].index_comm = state->communication_indices_[i];
+
+  for (unsigned i = 0; i < mcapi::get().get_maxpid(); i++)
+    patterns_copy(incomplete_communications_pattern[i], state->incomplete_comm_pattern_[i]);
+}
+
 static char* print_determinism_result(simgrid::mc::CommPatternDifference diff, int process,
                                       const simgrid::mc::PatternCommunication* comm, unsigned int cursor)
 {
@@ -95,7 +113,7 @@ static char* print_determinism_result(simgrid::mc::CommPatternDifference diff, i
 }
 
 static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern,
-                                simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr)
+                                const simgrid::kernel::activity::CommImpl* comm_addr)
 {
   auto src_proc = mcapi::get().get_src_actor(comm_addr);
   auto dst_proc = mcapi::get().get_dst_actor(comm_addr);
@@ -143,7 +161,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, co
         XBT_INFO("%s", this->send_diff);
         xbt_free(this->send_diff);
         this->send_diff = nullptr;
-        mcapi::get().s_log_state();
+        mcapi::get().log_state();
         mcapi::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       } else if (_sg_mc_comms_determinism && (not this->send_deterministic && not this->recv_deterministic)) {
         XBT_INFO("****************************************************");
@@ -159,7 +177,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, co
           xbt_free(this->recv_diff);
           this->recv_diff = nullptr;
         }
-        mcapi::get().s_log_state();
+        mcapi::get().log_state();
         mcapi::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       }
     }
@@ -170,7 +188,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, co
 
 void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, CallType call_type, int backtracking)
 {
-  const smx_actor_t issuer                                     = mcapi::get().mc_smx_simcall_get_issuer(request);
+  const smx_actor_t issuer                                     = mcapi::get().simcall_get_issuer(request);
   const mc::PatternCommunicationList& initial_pattern          = initial_communications_pattern[issuer->get_pid()];
   const std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer->get_pid()];
 
@@ -180,7 +198,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, Ca
   if (call_type == CallType::SEND) {
     /* Create comm pattern */
     pattern->type      = PatternCommunicationType::send;
-    pattern->comm_addr = mcapi::get().get_pattern_comm_addr(request);
+    pattern->comm_addr = mcapi::get().get_comm_isend_raw_addr(request);
     pattern->rdv      = mcapi::get().get_pattern_comm_rdv(pattern->comm_addr);
     pattern->src_proc = mcapi::get().get_pattern_comm_src_proc(pattern->comm_addr);
     pattern->src_host = mc_api::get().get_actor_host_name(issuer);
@@ -211,7 +229,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, Ca
 #endif
   } else if (call_type == CallType::RECV) {
     pattern->type = PatternCommunicationType::receive;
-    pattern->comm_addr = mcapi::get().get_pattern_comm_addr(request);
+    pattern->comm_addr = mcapi::get().get_comm_isend_raw_addr(request);
 
 #if HAVE_SMPI
     pattern->tag = mcapi::get().get_smpi_request_tag(request, simgrid::simix::Simcall::COMM_IRECV);
@@ -227,14 +245,14 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, Ca
   incomplete_communications_pattern[issuer->get_pid()].push_back(pattern.release());
 }
 
-void CommunicationDeterminismChecker::complete_comm_pattern(RemotePtr<kernel::activity::CommImpl> comm_addr,
+void CommunicationDeterminismChecker::complete_comm_pattern(const kernel::activity::CommImpl* comm_addr,
                                                             unsigned int issuer, int backtracking)
 {
   /* Complete comm pattern */
   std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer];
   auto current_comm_pattern =
       std::find_if(begin(incomplete_pattern), end(incomplete_pattern),
-                   [&comm_addr](const PatternCommunication* comm) { return remote(comm->comm_addr) == comm_addr; });
+                   [&comm_addr](const PatternCommunication* comm) { return mcapi::get().comm_addr_equal(comm->comm_addr, comm_addr); });
   if (current_comm_pattern == std::end(incomplete_pattern))
     xbt_die("Corresponding communication not found!");
 
@@ -338,13 +356,13 @@ void CommunicationDeterminismChecker::restoreState()
   /* Intermediate backtracking */
   State* last_state = stack_.back().get();
   if (last_state->system_state_) {
-    last_state->system_state_->restore(&mcapi::get().mc_get_remote_simulation());
-    MC_restore_communications_pattern(last_state);
+    mc_api::get().restore_state(last_state->system_state_);
+    restore_communications_pattern(last_state);
     return;
   }
 
   /* Restore the initial state */
-  mcapi::get().s_restore_initial_state();
+  mcapi::get().restore_initial_state();
 
   unsigned n = mcapi::get().get_maxpid();
   assert(n == incomplete_communications_pattern.size());
@@ -366,13 +384,13 @@ void CommunicationDeterminismChecker::restoreState()
     /* 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 = mcapi::get().mc_smx_simcall_get_issuer(saved_req);
+    const smx_actor_t issuer = mcapi::get().simcall_get_issuer(saved_req);
     smx_simcall_t req        = &issuer->simcall_;
 
     /* TODO : handle test and testany simcalls */
     CallType call = MC_get_call_type(req);
     mcapi::get().handle_simcall(state->transition_);
-    MC_handle_comm_pattern(call, req, req_num, 1);
+    handle_comm_pattern(call, req, req_num, 1);
     mcapi::get().mc_wait_for_requests();
 
     /* Update statistics */
@@ -381,6 +399,31 @@ void CommunicationDeterminismChecker::restoreState()
   }
 }
 
+void CommunicationDeterminismChecker::handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, int backtracking)
+{
+  using simgrid::mc::CallType;
+  switch(call_type) {
+    case CallType::NONE:
+      break;
+    case CallType::SEND:
+    case CallType::RECV:
+      get_comm_pattern(req, call_type, backtracking);
+      break;
+    case CallType::WAIT:
+    case CallType::WAITANY: {
+      simgrid::kernel::activity::CommImpl* comm_addr = nullptr;
+      if (call_type == CallType::WAIT)
+        comm_addr = mcapi::get().get_comm_wait_raw_addr(req);
+      else
+        comm_addr = mcapi::get().get_comm_waitany_raw_addr(req, value);
+      auto simcall_issuer = mcapi::get().simcall_get_issuer(req);
+      complete_comm_pattern(comm_addr, simcall_issuer->get_pid(), backtracking);
+    } break;
+  default:
+    xbt_die("Unexpected call type %i", (int)call_type);
+  }
+}
+
 void CommunicationDeterminismChecker::real_run()
 {
   std::unique_ptr<VisitedState> visited_state = nullptr;
@@ -422,7 +465,7 @@ void CommunicationDeterminismChecker::real_run()
       mcapi::get().handle_simcall(cur_state->transition_);
       /* After this call req is no longer useful */
 
-      MC_handle_comm_pattern(call, req, req_num, 0);
+      handle_comm_pattern(call, req, req_num, 0);
 
       /* Wait for requests (schedules processes) */
       mcapi::get().mc_wait_for_requests();
@@ -443,7 +486,7 @@ void CommunicationDeterminismChecker::real_run()
 
       if (visited_state == nullptr) {
         /* Get enabled actors and insert them in the interleave set of the next state */
-        auto actors = mcapi::get().mc_get_remote_simulation().actors();
+        auto actors = mcapi::get().get_actors();
         for (auto& actor : actors)
           if (mcapi::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
             next_state->add_interleaving_set(actor.copy.get_buffer());
@@ -499,7 +542,7 @@ void CommunicationDeterminismChecker::real_run()
     }
   }
 
-  mcapi::get().s_log_state();
+  mcapi::get().log_state();
 }
 
 void CommunicationDeterminismChecker::run()

diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp
index 3d3a910..291afb5 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.hpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.hpp
@@ -30,11 +30,12 @@ private:
   void log_state() override;
   void deterministic_comm_pattern(int process, const PatternCommunication* comm, int backtracking);
   void restoreState();
+  void handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, int backtracking);
 
 public:
   // These are used by functions which should be moved in CommunicationDeterminismChecker:
   void get_comm_pattern(smx_simcall_t request, CallType call_type, int backtracking);
-  void complete_comm_pattern(RemotePtr<kernel::activity::CommImpl> comm_addr, unsigned int issuer, int backtracking);
+  void complete_comm_pattern(const kernel::activity::CommImpl* comm_addr, unsigned int issuer, int backtracking);
 
 private:
   /** Stack representing the position in the exploration graph */

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 4d36052..07a6bb0 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -154,7 +154,7 @@ void LivenessChecker::replay()
 
       /* Debug information */
       XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
+                mcapi::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
 
       this->get_session().execute(state->transition_);
     }
@@ -232,7 +232,7 @@ void LivenessChecker::log_state() // override
 {
   XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_);
   XBT_INFO("Visited pairs = %lu", visited_pairs_count_);
-  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+  XBT_INFO("Executed transitions = %lu", mcapi::get().mc_get_executed_trans());
 }
 
 void LivenessChecker::show_acceptance_cycle(std::size_t depth)
@@ -243,8 +243,8 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth)
   XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
-  mc::dumpRecordPath();
-  mc::session->log_state();
+  mcapi::get().dump_record_path();
+  mcapi::get().log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }
 
@@ -255,7 +255,7 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
     int req_num       = pair->graph_state->transition_.argument_;
     smx_simcall_t req = &pair->graph_state->executed_req_;
     if (req->call_ != simix::Simcall::NONE)
-      trace.push_back(request_to_string(req, req_num, RequestType::executed));
+      trace.push_back(mcapi::get().request_to_string(req, req_num, RequestType::executed));
   }
   return trace;
 }
@@ -387,7 +387,7 @@ void LivenessChecker::run()
       fflush(dot_output);
     }
 
-    XBT_DEBUG("Execute: %s", request_to_string(req, req_num, RequestType::simix).c_str());
+    XBT_DEBUG("Execute: %s", mcapi::get().request_to_string(req, req_num, RequestType::simix).c_str());
 
     /* Update stats */
     mc_model_checker->executed_transitions++;

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index c8d29ec..ed02a9e 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -46,8 +46,8 @@ void SafetyChecker::check_non_termination(const State* current_state)
       auto checker = mcapi::get().mc_get_checker();
       for (auto const& s : checker->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      mcapi::get().mc_dump_record_path();
-      mcapi::get().s_log_state();
+      mcapi::get().dump_record_path();
+      mcapi::get().log_state();
 
       throw TerminationError();
     }
@@ -173,7 +173,7 @@ void SafetyChecker::run()
   }
 
   XBT_INFO("No property violation found.");
-  mcapi::get().s_log_state();
+  mcapi::get().log_state();
 }
 
 void SafetyChecker::backtrack()
@@ -199,7 +199,7 @@ void SafetyChecker::backtrack()
       if (req->call_ == simix::Simcall::MUTEX_LOCK || req->call_ == simix::Simcall::MUTEX_TRYLOCK)
         xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
 
-      const kernel::actor::ActorImpl* issuer = mcapi::get().mc_smx_simcall_get_issuer(req);
+      const kernel::actor::ActorImpl* issuer = mcapi::get().simcall_get_issuer(req);
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
         if (mcapi::get().request_depend(req, &prev_state->internal_req_)) {
@@ -221,14 +221,14 @@ void SafetyChecker::backtrack()
             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", mcapi::get().simix_simcall_name(req->call_),
-                    mcapi::get().simix_simcall_name(prev_state->internal_req_.call_));
+          XBT_DEBUG("Simcall %s and %s with same issuer", mcapi::get().simcall_get_name(req->call_),
+                    mcapi::get().simcall_get_name(prev_state->internal_req_.call_));
           break;
         } else {
-          const kernel::actor::ActorImpl* previous_issuer = mcapi::get().mc_smx_simcall_get_issuer(&prev_state->internal_req_);
+          const kernel::actor::ActorImpl* previous_issuer = mcapi::get().simcall_get_issuer(&prev_state->internal_req_);
           XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
-                    mcapi::get().simix_simcall_name(req->call_), issuer->get_pid(), state->num_,
-                    mcapi::get().simix_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
+                    mcapi::get().simcall_get_name(req->call_), issuer->get_pid(), state->num_,
+                    mcapi::get().simcall_get_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
         }
       }
     }
@@ -251,12 +251,12 @@ void SafetyChecker::restore_state()
   /* Intermediate backtracking */
   const State* last_state = stack_.back().get();
   if (last_state->system_state_) {
-    last_state->system_state_->restore(&mcapi::get().mc_get_remote_simulation());
+    mc_api::get().restore_state(last_state->system_state_);
     return;
   }
 
   /* Restore the initial state */
-  mcapi::get().s_restore_initial_state();
+  mcapi::get().restore_initial_state();
 
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (std::unique_ptr<State> const& state : stack_) {

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index 29e895b..34dd01c 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -205,22 +205,33 @@ unsigned long mc_api::get_maxpid() const
   return MC_smx_get_maxpid();
 }
 
-void mc_api::copy_incomplete_comm_pattern(const simgrid::mc::State* state) const
+int mc_api::get_actors_size() const
 {
-  MC_state_copy_incomplete_communications_pattern((simgrid::mc::State*)state);
+  return mc_model_checker->get_remote_simulation().actors().size();
 }
 
-void mc_api::copy_index_comm_pattern(const simgrid::mc::State* state) const
+bool mc_api::comm_addr_equal(const kernel::activity::CommImpl* comm_addr1, const kernel::activity::CommImpl* comm_addr2) const
 {
-  MC_state_copy_index_communications_pattern((simgrid::mc::State*)state);
+  return remote(comm_addr1) == remote(comm_addr2);
 }
 
-kernel::activity::CommImpl* mc_api::get_pattern_comm_addr(smx_simcall_t request) const
+kernel::activity::CommImpl* mc_api::get_comm_isend_raw_addr(smx_simcall_t request) const
 {
   auto comm_addr = simcall_comm_isend__getraw__result(request);
   return static_cast<kernel::activity::CommImpl*>(comm_addr);
 }
 
+kernel::activity::CommImpl* mc_api::get_comm_wait_raw_addr(smx_simcall_t request) const
+{
+  return simcall_comm_wait__getraw__comm(request);
+}
+
+kernel::activity::CommImpl* mc_api::get_comm_waitany_raw_addr(smx_simcall_t request, int value) const
+{
+  auto addr = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(request) + value));
+  return static_cast<simgrid::kernel::activity::CommImpl*>(addr);
+}
+
 std::string mc_api::get_pattern_comm_rdv(void* addr) const
 {
   Remote<kernel::activity::CommImpl> temp_synchro;
@@ -266,10 +277,10 @@ std::vector<char> mc_api::get_pattern_comm_data(void* addr) const
   return buffer;
 }
 
-std::vector<char> mc_api::get_pattern_comm_data(mc::RemotePtr<kernel::activity::CommImpl> const& comm_addr) const
+std::vector<char> mc_api::get_pattern_comm_data(const kernel::activity::CommImpl* comm_addr) const
 {
   simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
-  mc_model_checker->get_remote_simulation().read(temp_comm, comm_addr);
+  mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr));
   const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
   
   std::vector<char> buffer {};
@@ -295,20 +306,20 @@ bool mc_api::check_send_request_detached(smx_simcall_t const& simcall) const
   return mpi_request.detached();
 }
 
-smx_actor_t mc_api::get_src_actor(mc::RemotePtr<kernel::activity::CommImpl> const& comm_addr) const
+smx_actor_t mc_api::get_src_actor(const kernel::activity::CommImpl* comm_addr) const
 {
   simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
-  mc_model_checker->get_remote_simulation().read(temp_comm, comm_addr);
+  mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr));
   const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
 
   auto src_proc = mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(comm->src_actor_.get()));
   return src_proc;
 }
 
-smx_actor_t mc_api::get_dst_actor(mc::RemotePtr<kernel::activity::CommImpl> const& comm_addr) const
+smx_actor_t mc_api::get_dst_actor(const kernel::activity::CommImpl* comm_addr) const
 {
   simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
-  mc_model_checker->get_remote_simulation().read(temp_comm, comm_addr);
+  mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr));
   const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
 
   auto dst_proc = mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get()));
@@ -362,7 +373,7 @@ void mc_api::mc_show_deadlock() const
   MC_show_deadlock();
 }
 
-smx_actor_t mc_api::mc_smx_simcall_get_issuer(s_smx_simcall const* req) const
+smx_actor_t mc_api::simcall_get_issuer(s_smx_simcall const* req) const
 {
   return MC_smx_simcall_get_issuer(req);
 }
@@ -403,7 +414,7 @@ std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
   return mc_model_checker->get_host_name(hostname);
 }
 
-void mc_api::mc_dump_record_path() const
+void mc_api::dump_record_path() const
 {
   simgrid::mc::dumpRecordPath();
 }
@@ -437,7 +448,7 @@ std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const
   return simgrid::mc::request_get_dot_output(req, value);
 }
 
-const char* mc_api::simix_simcall_name(simgrid::simix::Simcall kind) const
+const char* mc_api::simcall_get_name(simgrid::simix::Simcall kind) const
 {
   return SIMIX_simcall_name(kind);
 }
@@ -456,6 +467,11 @@ int mc_api::get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::S
 }
 #endif
 
+void mc_api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const
+{
+  system_state->restore(&mc_model_checker->get_remote_simulation());
+}
+
 bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
 {
   return simgrid::mc::snapshot_equal(s1, s2);
@@ -472,7 +488,7 @@ void mc_api::s_close() const
   session->close();
 }
 
-void mc_api::s_restore_initial_state() const
+void mc_api::restore_initial_state() const
 {
   session->restore_initial_state();
 }
@@ -482,7 +498,7 @@ void mc_api::execute(Transition const& transition)
   session->execute(transition);
 }
 
-void mc_api::s_log_state() const
+void mc_api::log_state() const
 {
   session->log_state();
 }

diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp
index c6def81..5c8179b 100644 (file)
--- a/src/mc/mc_api.hpp
+++ b/src/mc/mc_api.hpp
@@ -42,20 +42,22 @@ public:
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;
   bool actor_is_enabled(aid_t pid) const;
   unsigned long get_maxpid() const;
+  int get_actors_size() const;
 
   // COMMUNICATION APIs
-  void copy_incomplete_comm_pattern(const simgrid::mc::State* state) const;
-  void copy_index_comm_pattern(const simgrid::mc::State* state) const;
-  kernel::activity::CommImpl* get_pattern_comm_addr(smx_simcall_t request) const;
+  bool comm_addr_equal(const kernel::activity::CommImpl* comm_addr1, const kernel::activity::CommImpl* comm_addr2) const;
+  kernel::activity::CommImpl* get_comm_isend_raw_addr(smx_simcall_t request) const;
+  kernel::activity::CommImpl* get_comm_wait_raw_addr(smx_simcall_t request) const;
+  kernel::activity::CommImpl* get_comm_waitany_raw_addr(smx_simcall_t request, int value) const;
   std::string get_pattern_comm_rdv(void* addr) const;
   unsigned long get_pattern_comm_src_proc(void* addr) const;
   unsigned long get_pattern_comm_dst_proc(void* addr) const;
   std::vector<char> get_pattern_comm_data(void* addr) const;
-  std::vector<char> get_pattern_comm_data(mc::RemotePtr<kernel::activity::CommImpl> const& comm_addr) const;
+  std::vector<char> get_pattern_comm_data(const kernel::activity::CommImpl* comm_addr) const;
   const char* get_actor_host_name(smx_actor_t actor) const;
   bool check_send_request_detached(smx_simcall_t const& simcall) const;
-  smx_actor_t get_src_actor(mc::RemotePtr<kernel::activity::CommImpl> const& comm_addr) const;
-  smx_actor_t get_dst_actor(mc::RemotePtr<kernel::activity::CommImpl> const& comm_addr) const;
+  smx_actor_t get_src_actor(const kernel::activity::CommImpl* comm_addr) const;
+  smx_actor_t get_dst_actor(const kernel::activity::CommImpl* comm_addr) const;
 
   // REMOTE APIs
   std::size_t get_remote_heap_bytes() const;
@@ -68,7 +70,6 @@ public:
   unsigned long mc_get_executed_trans() const;
   bool mc_check_deadlock() const;
   void mc_show_deadlock() const;
-  smx_actor_t mc_smx_simcall_get_issuer(s_smx_simcall const* req) const;
   bool mc_is_null() const;
   Checker* mc_get_checker() const;
   RemoteSimulation& mc_get_remote_simulation() const;
@@ -76,18 +77,24 @@ public:
   void mc_wait_for_requests() const;
   void mc_exit(int status) const;
   std::string const& mc_get_host_name(std::string const& hostname) const;
-  void mc_dump_record_path() const;
+  void dump_record_path() const;
   smx_simcall_t mc_state_choose_request(simgrid::mc::State* state) const;
 
   // SIMCALL APIs
   bool request_depend(smx_simcall_t req1, smx_simcall_t req2) const;
   std::string request_to_string(smx_simcall_t req, int value, RequestType request_type) const;
   std::string request_get_dot_output(smx_simcall_t req, int value) const;
-  const char *simix_simcall_name(simgrid::simix::Simcall kind) const;
+  const char *simcall_get_name(simgrid::simix::Simcall kind) const;
+  smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const;
   #if HAVE_SMPI
   int get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const;
   #endif
 
+  // STATE APIs
+  void restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const;
+  void log_state() const;
+  void restore_initial_state() const;
+
   // SNAPSHOT APIs
   bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;
   simgrid::mc::Snapshot* take_snapshot(int num_state) const;
@@ -95,9 +102,7 @@ public:
   // SESSION APIs
   void s_initialize() const;
   void s_close() const;
-  void s_restore_initial_state() const;
   void execute(Transition const& transition);
-  void s_log_state() const;
 };
 
 } // namespace mc

diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp
deleted file mode 100644 (file)
index 3f066a7..0000000
--- a/src/mc/mc_comm_pattern.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-/* Copyright (c) 2007-2020. 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 <cstring>
-
-#include "src/mc/checker/CommunicationDeterminismChecker.hpp"
-#include "src/mc/mc_smx.hpp"
-
-using simgrid::mc::remote;
-
-static void MC_patterns_copy(std::vector<simgrid::mc::PatternCommunication*>& dest,
-                             std::vector<simgrid::mc::PatternCommunication> const& source)
-{
-  dest.clear();
-  for (simgrid::mc::PatternCommunication const& comm : source) {
-    auto* copy_comm = new simgrid::mc::PatternCommunication(comm.dup());
-    dest.push_back(copy_comm);
-  }
-}
-
-void MC_restore_communications_pattern(simgrid::mc::State* state)
-{
-  for (unsigned i = 0; i < initial_communications_pattern.size(); i++)
-    initial_communications_pattern[i].index_comm = state->communication_indices_[i];
-
-  for (unsigned i = 0; i < MC_smx_get_maxpid(); i++)
-    MC_patterns_copy(incomplete_communications_pattern[i], state->incomplete_comm_pattern_[i]);
-}
-
-void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state)
-{
-  state->incomplete_comm_pattern_.clear();
-  for (unsigned i=0; i < MC_smx_get_maxpid(); i++) {
-    std::vector<simgrid::mc::PatternCommunication> res;
-    for (auto const& comm : incomplete_communications_pattern[i])
-      res.push_back(comm->dup());
-    state->incomplete_comm_pattern_.push_back(std::move(res));
-  }
-}
-
-void MC_state_copy_index_communications_pattern(simgrid::mc::State* state)
-{
-  state->communication_indices_.clear();
-  for (auto const& list_process_comm : initial_communications_pattern)
-    state->communication_indices_.push_back(list_process_comm.index_comm);
-}
-
-void MC_handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, int backtracking)
-{
-  // HACK, do not rely on the Checker implementation outside of it
-  auto* checker = static_cast<simgrid::mc::CommunicationDeterminismChecker*>(mc_model_checker->getChecker());
-
-  using simgrid::mc::CallType;
-  switch(call_type) {
-    case CallType::NONE:
-      break;
-    case CallType::SEND:
-    case CallType::RECV:
-      checker->get_comm_pattern(req, call_type, backtracking);
-      break;
-    case CallType::WAIT:
-    case CallType::WAITANY: {
-      simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr{nullptr};
-      if (call_type == CallType::WAIT)
-        comm_addr = remote(simcall_comm_wait__getraw__comm(req));
-
-      else {
-        simgrid::kernel::activity::ActivityImpl* addr;
-        addr = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(req) + value));
-        comm_addr = remote(static_cast<simgrid::kernel::activity::CommImpl*>(addr));
-      }
-      checker->complete_comm_pattern(comm_addr, MC_smx_simcall_get_issuer(req)->get_pid(), backtracking);
-    } break;
-  default:
-    xbt_die("Unexpected call type %i", (int)call_type);
-  }
-}

diff --git a/src/mc/mc_comm_pattern.hpp b/src/mc/mc_comm_pattern.hpp
index 70e6a30..1c95e49 100644 (file)
--- a/src/mc/mc_comm_pattern.hpp
+++ b/src/mc/mc_comm_pattern.hpp
@@ -7,9 +7,7 @@
 #define SIMGRID_MC_COMM_PATTERN_H
 
 #include <vector>
-
-#include "smpi/smpi.h"
-#include "src/mc/mc_state.hpp"
+#include "src/mc/mc_pattern.hpp"
 
 namespace simgrid {
 namespace mc {
@@ -61,12 +59,4 @@ static inline simgrid::mc::CallType MC_get_call_type(const s_smx_simcall* req)
   }
 }
 
-XBT_PRIVATE void MC_handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t request, int value,
-                                        int backtracking);
-
-XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state);
-
-XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state);
-XBT_PRIVATE void MC_state_copy_index_communications_pattern(simgrid::mc::State* state);
-
 #endif

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index c078742..967d730 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -25,8 +25,8 @@ State::State(unsigned long state_number) : num_(state_number)
     auto snapshot_ptr = mcapi::get().take_snapshot(num_);
     system_state_ = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-      mcapi::get().copy_incomplete_comm_pattern(this);
-      mcapi::get().copy_index_comm_pattern(this);
+      copy_incomplete_comm_pattern();
+      copy_index_comm_pattern();
     }
   }
 }
@@ -41,5 +41,23 @@ Transition State::get_transition() const
   return this->transition_;
 }
 
+void State::copy_incomplete_comm_pattern()
+{
+  incomplete_comm_pattern_.clear();
+  for (auto i=0; i < mcapi::get().get_maxpid(); i++) {
+    std::vector<simgrid::mc::PatternCommunication> res;
+    for (auto const& comm : incomplete_communications_pattern[i])
+      res.push_back(comm->dup());
+    incomplete_comm_pattern_.push_back(std::move(res));
+  }
+}
+
+void State::copy_index_comm_pattern()
+{
+  communication_indices_.clear();
+  for (auto const& list_process_comm : initial_communications_pattern)
+    this->communication_indices_.push_back(list_process_comm.index_comm);
+}
+
 }
 }

diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp
index 2f347e3..ec53b61 100644 (file)
--- a/src/mc/mc_state.hpp
+++ b/src/mc/mc_state.hpp
@@ -8,7 +8,7 @@
 
 #include "src/mc/Transition.hpp"
 #include "src/mc/sosp/Snapshot.hpp"
-#include "src/mc/mc_pattern.hpp"
+#include "src/mc/mc_comm_pattern.hpp"
 
 namespace simgrid {
 namespace mc {
@@ -52,6 +52,10 @@ public:
     this->actor_states_[actor->get_pid()].consider();
   }
   Transition get_transition() const;
+
+private:
+  void copy_incomplete_comm_pattern();
+  void copy_index_comm_pattern();
 };
 }
 }

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 27bf5f8..aeb9429 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -658,7 +658,6 @@ set(MC_SRC
   src/mc/mc_forward.hpp
   src/mc/Session.cpp
   src/mc/Session.hpp
-  src/mc/mc_comm_pattern.cpp
   src/mc/mc_comm_pattern.hpp
   src/mc/mc_pattern.hpp
   src/mc/compare.cpp