kill ModelChecker::simcall_is_visible()

no need for the checker to check whether a simcall is visible:
invisible simcalls are handled in the AppSide and never show up on the
cheker side.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index ea47b49..2dccd7a 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -336,30 +336,6 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n
   } else
     return nullptr;
 }
-bool ModelChecker::simcall_is_visible(aid_t aid)
-{
-  xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");
-
-  s_mc_message_simcall_is_visible_t m;
-  memset(&m, 0, sizeof(m));
-  m.type = MessageType::SIMCALL_IS_VISIBLE;
-  m.aid  = aid;
-  checker_side_.get_channel().send(m);
-
-  s_mc_message_simcall_is_visible_answer_t answer;
-  ssize_t s = checker_side_.get_channel().receive(answer);
-  xbt_assert(s != -1, "Could not receive message");
-  xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_IS_VISIBLE_ANSWER,
-             "Received unexpected message %s (%i, size=%i) "
-             "expected MessageType::SIMCALL_IS_VISIBLE_ANSWER (%i, size=%i)",
-             to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_VISIBLE_ANSWER,
-             (int)sizeof(answer));
-
-  XBT_DEBUG("is_visible(%ld) is returning %s", aid, answer.value ? "true" : "false");
-
-  this->remote_process_->clear_cache();
-  return answer.value;
-}
 
 void ModelChecker::finalize_app(bool terminate_asap)
 {

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index ab99ea5..6725877 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -55,8 +55,6 @@ public:
   Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
 
   /* Interactions with the simcall observer */
-  bool simcall_is_visible(aid_t aid);
-
   XBT_ATTRIB_NORETURN void exit(int status);
 
   bool checkDeadlock();

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index e56a854..910ec35 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -163,20 +163,6 @@ void AppSide::handle_messages() const
         handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data());
         break;
 
-      case MessageType::SIMCALL_IS_VISIBLE: {
-        assert_msg_size("SIMCALL_IS_VISIBLE", s_mc_message_simcall_is_visible_t);
-        auto msg_simcall                = (s_mc_message_simcall_is_visible_t*)message_buffer.data();
-        const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid);
-        xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid);
-        xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname());
-        bool value = actor->simcall_.observer_->is_visible();
-
-        // Send result:
-        s_mc_message_simcall_is_visible_answer_t answer{MessageType::SIMCALL_IS_VISIBLE_ANSWER, value};
-        xbt_assert(channel_.send(answer) == 0, "Could not send response");
-        break;
-      }
-
       case MessageType::ACTOR_ENABLED:
         assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
         handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index ef82981..7a3dbac 100644 (file)
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -32,8 +32,7 @@ namespace mc {
 
 XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
                        STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
-                       SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, ASSERTION_FAILED,
-                       ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
+                       SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
 
 } // namespace mc
 } // namespace simgrid
@@ -117,15 +116,5 @@ struct s_mc_message_actor_enabled_t {
   aid_t aid; // actor ID
 };
 
-/* RPC */
-struct s_mc_message_simcall_is_visible_t { // MessageType::SIMCALL_IS_VISIBLE
-  simgrid::mc::MessageType type;
-  aid_t aid;
-};
-struct s_mc_message_simcall_is_visible_answer_t { // MessageType::SIMCALL_IS_VISIBLE_ANSWER
-  simgrid::mc::MessageType type;
-  bool value;
-};
-
 #endif // __cplusplus
 #endif