From 3f1310c945ff4a77280121cd1eca8d2d019c2091 Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Sat, 20 Mar 2021 22:54:34 +0100
Subject: [PATCH] Add ModelChecker::finalize_app(), but don't use it as it
 don't work yet

---
 src/mc/ModelChecker.cpp          |  9 +++++++++
 src/mc/ModelChecker.hpp          |  1 +
 src/mc/checker/SafetyChecker.cpp |  1 +
 src/mc/remote/AppSide.cpp        | 12 ++++++++++++
 src/mc/remote/mc_protocol.h      |  2 +-
 src/simix/smx_global.cpp         |  3 ++-
 6 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 3059561081..4ae4fc5a41 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -379,6 +379,15 @@ std::string ModelChecker::simcall_dot_label(int aid, int times_considered)
   return answer;
 }
 
+void ModelChecker::finalize_app()
+{
+  int res = checker_side_.get_channel().send(MessageType::FINALIZE);
+  xbt_assert(res == 0, "Could not ask the app to finalize MPI on need");
+  s_mc_message_int_t message;
+  ssize_t s = checker_side_.get_channel().receive(message);
+  xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+}
+
 bool ModelChecker::checkDeadlock()
 {
   int res = checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK);
diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 4807fbff40..6dead6e0da 100644
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -59,6 +59,7 @@ public:
   XBT_ATTRIB_NORETURN void exit(int status);
 
   bool checkDeadlock();
+  void finalize_app();
 
   Checker* getChecker() const { return checker_; }
   void setChecker(Checker* checker) { checker_ = checker; }
diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index aff600d2aa..77e2ff5948 100644
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -112,6 +112,7 @@ void SafetyChecker::run()
     if (req == nullptr) {
       XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
 
+//      mc_model_checker->finalize_app();
       this->backtrack();
       continue;
     }
diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 3279cf1a17..aaad66613a 100644
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -184,6 +184,18 @@ void AppSide::handle_messages() const
         handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
         break;
 
+      case MessageType::FINALIZE: {
+#if HAVE_SMPI
+        XBT_INFO("Finalize. Smpi_enabled: %d", (int)smpi_enabled());
+        simix_global->display_all_actor_status();
+        if (smpi_enabled())
+          SMPI_finalize();
+#endif
+        s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, 0};
+        xbt_assert(channel_.send(answer) == 0, "Could answer to FINALIZE");
+        break;
+      }
+
       default:
         xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
         break;
diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index f03cf3fa89..58332cd118 100644
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -29,7 +29,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_HANDLE,
                        SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING, SIMCALL_TO_STRING_ANSWER,
-                       SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY);
+                       SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
 
 } // namespace mc
 } // namespace simgrid
diff --git a/src/simix/smx_global.cpp b/src/simix/smx_global.cpp
index 930a257762..97f826d7a5 100644
--- a/src/simix/smx_global.cpp
+++ b/src/simix/smx_global.cpp
@@ -265,7 +265,8 @@ void Global::display_all_actor_status() const
                (xbt_log_no_loc ? (size_t)0xDEADBEEF : (size_t)actor->waiting_synchro_.get()),
                actor->waiting_synchro_->get_cname(), (int)actor->waiting_synchro_->state_);
     } else {
-      XBT_INFO("Actor %ld (%s@%s)", actor->get_pid(), actor->get_cname(), actor->get_host()->get_cname());
+      XBT_INFO("Actor %ld (%s@%s) simcall %s", actor->get_pid(), actor->get_cname(), actor->get_host()->get_cname(), SIMIX_simcall_name(actor->simcall_.call_));
+
     }
   }
 }
-- 
2.20.1