mc: rename Inspector to Observer

diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h
index a8f7cd3..72889a3 100644 (file)
--- a/include/simgrid/forward.h
+++ b/include/simgrid/forward.h
@@ -180,7 +180,7 @@ namespace surf {
 }
 namespace mc {
 class CommunicationDeterminismChecker;
-class SimcallInspector;
+class SimcallObserver;
 }
 namespace vm {
 class VMModel;

diff --git a/include/simgrid/simix.hpp b/include/simgrid/simix.hpp
index b6bea16..76fd191 100644 (file)
--- a/include/simgrid/simix.hpp
+++ b/include/simgrid/simix.hpp
@@ -17,8 +17,8 @@
 #include <string>
 #include <unordered_map>
 
-XBT_PUBLIC void simcall_run_kernel(std::function<void()> const& code, simgrid::mc::SimcallInspector* t);
-XBT_PUBLIC void simcall_run_blocking(std::function<void()> const& code, simgrid::mc::SimcallInspector* t);
+XBT_PUBLIC void simcall_run_kernel(std::function<void()> const& code, simgrid::mc::SimcallObserver* t);
+XBT_PUBLIC void simcall_run_blocking(std::function<void()> const& code, simgrid::mc::SimcallObserver* t);
 
 namespace simgrid {
 namespace kernel {
@@ -43,7 +43,7 @@ namespace actor {
  * you may need to wait for that mutex to be unlocked by its current owner.
  * Potentially blocking simcall must be issued using simcall_blocking(), right below in this file.
  */
-template <class F> typename std::result_of_t<F()> simcall(F&& code, mc::SimcallInspector* t = nullptr)
+template <class F> typename std::result_of_t<F()> simcall(F&& code, mc::SimcallObserver* t = nullptr)
 {
   // If we are in the maestro, we take the fast path and execute the
   // code directly without simcall marshalling/unmarshalling/dispatch:
@@ -76,7 +76,7 @@ template <class F> typename std::result_of_t<F()> simcall(F&& code, mc::SimcallI
  *
  * If your code never calls actor->simcall_answer() itself, the actor will never return from its simcall.
  */
-template <class R, class F> R simcall_blocking(F&& code, mc::SimcallInspector* t = nullptr)
+template <class R, class F> R simcall_blocking(F&& code, mc::SimcallObserver* t = nullptr)
 {
   // If we are in the maestro, we take the fast path and execute the
   // code directly without simcall marshalling/unmarshalling/dispatch:

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 78dcd01..68a5565 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -3,7 +3,7 @@
 #include "src/kernel/activity/MailboxImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_pattern.hpp"
@@ -69,7 +69,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta
     return nullptr; // Not executable in the application
 
   smx_simcall_t req = nullptr;
-  if (actor->simcall_.inspector_ != nullptr) {
+  if (actor->simcall_.observer_ != nullptr) {
     state->transition_.times_considered_ = procstate->times_considered;
     procstate->times_considered++;
     if (actor->simcall_.mc_max_consider_ <= procstate->times_considered)
@@ -722,7 +722,7 @@ std::string Api::request_to_string(smx_simcall_t req, int value, RequestType req
 
   smx_actor_t issuer = simcall_get_issuer(req);
 
-  if (issuer->simcall_.inspector_ != nullptr)
+  if (issuer->simcall_.observer_ != nullptr)
     return mc_model_checker->simcall_to_string(issuer->get_pid(), value);
 
   switch (req->call_) {
@@ -860,7 +860,7 @@ std::string Api::request_get_dot_output(smx_simcall_t req, int value) const
 
   std::string label;
 
-  if (req->inspector_ != nullptr) {
+  if (req->observer_ != nullptr) {
     label = mc_model_checker->simcall_dot_label(issuer->get_pid(), value);
   } else
     switch (req->call_) {

diff --git a/src/mc/checker/SimcallInspector.cpp b/src/mc/checker/SimcallObserver.cpp
similarity index 69%
rename from src/mc/checker/SimcallInspector.cpp
rename to src/mc/checker/SimcallObserver.cpp
index 29ed4c0..93b92ab 100644 (file)
--- a/src/mc/checker/SimcallInspector.cpp
+++ b/src/mc/checker/SimcallObserver.cpp
@@ -3,22 +3,22 @@
 /* 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 "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 #include "simgrid/s4u/Host.hpp"
 #include "src/kernel/actor/ActorImpl.hpp"
 
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_inspector, mc, "Logging specific to MC simcall inspection");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation");
 
 namespace simgrid {
 namespace mc {
 
-std::string SimcallInspector::to_string(int /*time_considered*/) const
+std::string SimcallObserver::to_string(int /*time_considered*/) const
 {
   return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
                                      issuer_->get_cname());
 }
 
-std::string SimcallInspector::dot_label() const
+std::string SimcallObserver::dot_label() const
 {
   if (issuer_->get_host())
     return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_cname());
@@ -27,12 +27,12 @@ std::string SimcallInspector::dot_label() const
 
 std::string RandomSimcall::to_string(int time_considered) const
 {
-  return SimcallInspector::to_string(time_considered) + "MC_RANDOM(" + std::to_string(time_considered) + ")";
+  return SimcallObserver::to_string(time_considered) + "MC_RANDOM(" + std::to_string(time_considered) + ")";
 }
 
 std::string RandomSimcall::dot_label() const
 {
-  return SimcallInspector::dot_label() + "MC_RANDOM(" + std::to_string(next_value_) + ")";
+  return SimcallObserver::dot_label() + "MC_RANDOM(" + std::to_string(next_value_) + ")";
 }
 
 void RandomSimcall::prepare(int times_considered)
@@ -53,12 +53,12 @@ int RandomSimcall::get_value() const
 
 std::string MutexUnlockSimcall::to_string(int time_considered) const
 {
-  return SimcallInspector::to_string(time_considered) + "Mutex UNLOCK";
+  return SimcallObserver::to_string(time_considered) + "Mutex UNLOCK";
 }
 
 std::string MutexUnlockSimcall::dot_label() const
 {
-  return SimcallInspector::dot_label() + "Mutex UNLOCK";
+  return SimcallObserver::dot_label() + "Mutex UNLOCK";
 }
 
 } // namespace mc

diff --git a/src/mc/checker/SimcallInspector.hpp b/src/mc/checker/SimcallObserver.hpp
similarity index 83%
rename from src/mc/checker/SimcallInspector.hpp
rename to src/mc/checker/SimcallObserver.hpp
index 3a06e8f..a611f16 100644 (file)
--- a/src/mc/checker/SimcallInspector.hpp
+++ b/src/mc/checker/SimcallObserver.hpp
@@ -3,8 +3,8 @@
 /* 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. */
 
-#ifndef SIMGRID_MC_SIMCALL_INSPECTOR_HPP
-#define SIMGRID_MC_SIMCALL_INSPECTOR_HPP
+#ifndef SIMGRID_MC_SIMCALL_OBSERVER_HPP
+#define SIMGRID_MC_SIMCALL_OBSERVER_HPP
 
 #include "simgrid/forward.h"
 
@@ -13,11 +13,11 @@
 namespace simgrid {
 namespace mc {
 
-class SimcallInspector {
+class SimcallObserver {
   kernel::actor::ActorImpl* issuer_;
 
 public:
-  explicit SimcallInspector(kernel::actor::ActorImpl* issuer) : issuer_(issuer) {}
+  explicit SimcallObserver(kernel::actor::ActorImpl* issuer) : issuer_(issuer) {}
   kernel::actor::ActorImpl* get_issuer() const { return issuer_; }
   /** Whether this transition can currently be taken without blocking.
    *
@@ -46,19 +46,19 @@ public:
   virtual void prepare(int times_considered) { /* Nothing to do by default */}
 
   /** Some simcalls may only be observable under some circumstances.
-   * Most simcalls are not visible from the MC because they don't have an inspector at all. */
+   * Most simcalls are not visible from the MC because they don't have an observer at all. */
   virtual bool is_visible() const { return true; }
   virtual std::string to_string(int times_considered) const = 0;
   virtual std::string dot_label() const                     = 0;
 };
 
-class RandomSimcall : public SimcallInspector {
+class RandomSimcall : public SimcallObserver {
   int min_;
   int max_;
   int next_value_ = 0;
 
 public:
-  RandomSimcall(smx_actor_t actor, int min, int max) : SimcallInspector(actor), min_(min), max_(max) {}
+  RandomSimcall(smx_actor_t actor, int min, int max) : SimcallObserver(actor), min_(min), max_(max) {}
   int get_max_consider() const override;
   void prepare(int times_considered) override;
   std::string to_string(int times_considered) const override;
@@ -66,8 +66,8 @@ public:
   int get_value() const;
 };
 
-class MutexUnlockSimcall : public SimcallInspector {
-  using SimcallInspector::SimcallInspector;
+class MutexUnlockSimcall : public SimcallObserver {
+  using SimcallObserver::SimcallObserver;
 
 public:
   std::string to_string(int times_considered) const override;

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 5a56243..344752b 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -7,7 +7,7 @@
 #include "mc/mc.h"
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_replay.hpp"
 #include "src/simix/smx_private.hpp"
@@ -57,8 +57,8 @@ void wait_for_requests()
   xbt_dynar_reset(simix_global->actors_vector);
   for (std::pair<const aid_t, smx_actor_t> const& kv : simix_global->process_list) {
     auto actor = kv.second;
-    if (actor->simcall_.inspector_ != nullptr)
-      actor->simcall_.mc_max_consider_ = actor->simcall_.inspector_->get_max_consider();
+    if (actor->simcall_.observer_ != nullptr)
+      actor->simcall_.mc_max_consider_ = actor->simcall_.observer_->get_max_consider();
     xbt_dynar_push_as(simix_global->actors_vector, smx_actor_t, actor);
   }
 #endif
@@ -90,8 +90,8 @@ bool actor_is_enabled(smx_actor_t actor)
   // Now, we are in the client app, no need for remote memory reading.
   smx_simcall_t req = &actor->simcall_;
 
-  if (req->inspector_ != nullptr)
-    return req->inspector_->is_enabled();
+  if (req->observer_ != nullptr)
+    return req->observer_->is_enabled();
 
   using simix::Simcall;
   switch (req->call_) {
@@ -163,8 +163,8 @@ bool request_is_visible(const s_smx_simcall* req)
 #if SIMGRID_HAVE_MC
   xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
 #endif
-  if (req->inspector_ != nullptr)
-    return req->inspector_->is_visible();
+  if (req->observer_ != nullptr)
+    return req->observer_->is_visible();
 
   using simix::Simcall;
   return req->call_ == Simcall::COMM_ISEND || req->call_ == Simcall::COMM_IRECV || req->call_ == Simcall::COMM_WAIT ||

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index 84219c7..a453f05 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -8,7 +8,7 @@
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 #include "src/mc/mc_smx.hpp"
 #include <array>
 

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 0c82035..a0a16e6 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -6,7 +6,7 @@
 #include "src/mc/remote/AppSide.hpp"
 #include "src/internal_config.h"
 #include "src/kernel/actor/ActorImpl.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 #include <simgrid/modelchecker.h>
 
 #include <cerrno>
@@ -141,8 +141,8 @@ void AppSide::handle_messages() const
         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 %d", msg_simcall->aid);
-        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
-        bool value = actor->simcall_.inspector_->is_visible();
+        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};
@@ -155,8 +155,8 @@ void AppSide::handle_messages() const
         auto msg_simcall                = (s_mc_message_simcall_to_string_t*)message_buffer.data();
         const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid);
         xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid);
-        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
-        std::string value = actor->simcall_.inspector_->to_string(msg_simcall->time_considered);
+        xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname());
+        std::string value = actor->simcall_.observer_->to_string(msg_simcall->time_considered);
 
         // Send result:
         s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}};
@@ -170,8 +170,8 @@ void AppSide::handle_messages() const
         auto msg_simcall                = (s_mc_message_simcall_to_string_t*)message_buffer.data();
         const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid);
         xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid);
-        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
-        std::string value = actor->simcall_.inspector_->dot_label();
+        xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname());
+        std::string value = actor->simcall_.observer_->dot_label();
 
         // Send result:
         s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}};

diff --git a/src/s4u/s4u_Mutex.cpp b/src/s4u/s4u_Mutex.cpp
index cd7ce96..d6a65f6 100644 (file)
--- a/src/s4u/s4u_Mutex.cpp
+++ b/src/s4u/s4u_Mutex.cpp
@@ -7,7 +7,7 @@
 #include "simgrid/mutex.h"
 #include "simgrid/s4u/Mutex.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 
 namespace simgrid {
 namespace s4u {

diff --git a/src/simix/libsmx.cpp b/src/simix/libsmx.cpp
index 518a8be..c061cdd 100644 (file)
--- a/src/simix/libsmx.cpp
+++ b/src/simix/libsmx.cpp
@@ -18,7 +18,7 @@
 #include "src/kernel/activity/IoImpl.hpp"
 #include "src/kernel/activity/MailboxImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 #include "src/mc/mc_replay.hpp"
 #include "src/plugins/vm/VirtualMachineImpl.hpp"
 #include "xbt/random.hpp"
@@ -351,18 +351,18 @@ bool simcall_io_test(const simgrid::kernel::activity::ActivityImplPtr& io) // XB
   return simgrid::kernel::actor::simcall([io] { return io->test(); });
 }
 
-void simcall_run_kernel(std::function<void()> const& code, simgrid::mc::SimcallInspector* t)
+void simcall_run_kernel(std::function<void()> const& code, simgrid::mc::SimcallObserver* t)
 {
-  simgrid::kernel::actor::ActorImpl::self()->simcall_.inspector_ = t;
+  simgrid::kernel::actor::ActorImpl::self()->simcall_.observer_ = t;
   simcall_BODY_run_kernel(&code);
-  simgrid::kernel::actor::ActorImpl::self()->simcall_.inspector_ = nullptr;
+  simgrid::kernel::actor::ActorImpl::self()->simcall_.observer_ = nullptr;
 }
 
-void simcall_run_blocking(std::function<void()> const& code, simgrid::mc::SimcallInspector* t = nullptr)
+void simcall_run_blocking(std::function<void()> const& code, simgrid::mc::SimcallObserver* t = nullptr)
 {
-  simgrid::kernel::actor::ActorImpl::self()->simcall_.inspector_ = t;
+  simgrid::kernel::actor::ActorImpl::self()->simcall_.observer_ = t;
   simcall_BODY_run_blocking(&code);
-  simgrid::kernel::actor::ActorImpl::self()->simcall_.inspector_ = nullptr;
+  simgrid::kernel::actor::ActorImpl::self()->simcall_.observer_ = nullptr;
 }
 
 int simcall_mc_random(int min, int max) // XBT_ATTRIB_DEPRECATD_v331

diff --git a/src/simix/popping_generated.cpp b/src/simix/popping_generated.cpp
index 0aa70b7..a4f88aa 100644 (file)
--- a/src/simix/popping_generated.cpp
+++ b/src/simix/popping_generated.cpp
@@ -21,7 +21,7 @@
 #include "src/mc/mc_forward.hpp"
 #endif
 #include "src/kernel/activity/ConditionVariableImpl.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
 
@@ -57,8 +57,8 @@ void simgrid::kernel::actor::ActorImpl::simcall_handle(int times_considered_)
 {
   XBT_DEBUG("Handling simcall %p: %s", &simcall_, SIMIX_simcall_name(simcall_.call_));
   SIMCALL_SET_MC_VALUE(simcall_, times_considered_);
-  if (simcall_.inspector_ != nullptr)
-    simcall_.inspector_->prepare(times_considered_);
+  if (simcall_.observer_ != nullptr)
+    simcall_.observer_->prepare(times_considered_);
   if (context_->wannadie())
     return;
   switch (simcall_.call_) {

diff --git a/src/simix/popping_private.hpp b/src/simix/popping_private.hpp
index 6300263..e7abda9 100644 (file)
--- a/src/simix/popping_private.hpp
+++ b/src/simix/popping_private.hpp
@@ -44,14 +44,14 @@ union u_smx_scalar {
  * @brief Represents a simcall to the kernel.
  */
 struct s_smx_simcall {
-  simgrid::simix::Simcall call_             = simgrid::simix::Simcall::NONE;
-  smx_actor_t issuer_                       = nullptr;
-  smx_timer_t timeout_cb_                   = nullptr; // Callback to timeouts
-  simgrid::mc::SimcallInspector* inspector_ = nullptr; // makes that simcall observable by the MC
+  simgrid::simix::Simcall call_           = simgrid::simix::Simcall::NONE;
+  smx_actor_t issuer_                     = nullptr;
+  smx_timer_t timeout_cb_                 = nullptr; // Callback to timeouts
+  simgrid::mc::SimcallObserver* observer_ = nullptr; // makes that simcall observable by the MC
   unsigned int mc_max_consider_ = 0; // How many times this simcall should be used. If >1, this will be a fork.
-  int mc_value_                             = 0;
-  std::array<u_smx_scalar, 11> args_        = {};
-  u_smx_scalar result_                      = {};
+  int mc_value_                           = 0;
+  std::array<u_smx_scalar, 11> args_      = {};
+  u_smx_scalar result_                    = {};
 };
 
 #define SIMCALL_SET_MC_VALUE(simcall, value) ((simcall).mc_value_ = (value))

diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py
index bd2789e..a938e4f 100755 (executable)
--- a/src/simix/simcalls.py
+++ b/src/simix/simcalls.py
@@ -314,7 +314,7 @@ if __name__ == '__main__':
     fd.write('#include "src/mc/mc_forward.hpp"\n')
     fd.write('#endif\n')
     fd.write('#include "src/kernel/activity/ConditionVariableImpl.hpp"\n')
-    fd.write('#include "src/mc/checker/SimcallInspector.hpp"\n')
+    fd.write('#include "src/mc/checker/SimcallObserver.hpp"\n')
 
     fd.write('\n')
     fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n')
@@ -338,8 +338,8 @@ if __name__ == '__main__':
     fd.write('{\n')
     fd.write('  XBT_DEBUG("Handling simcall %p: %s", &simcall_, SIMIX_simcall_name(simcall_.call_));\n')
     fd.write('  SIMCALL_SET_MC_VALUE(simcall_, times_considered_);\n')
-    fd.write('  if (simcall_.inspector_ != nullptr)\n')
-    fd.write('    simcall_.inspector_->prepare(times_considered_);\n')
+    fd.write('  if (simcall_.observer_ != nullptr)\n')
+    fd.write('    simcall_.observer_->prepare(times_considered_);\n')
 
     fd.write('  if (context_->wannadie())\n')
     fd.write('    return;\n')

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 548a950..fef48b5 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -580,8 +580,8 @@ set(MC_SRC_BASE
   src/mc/mc_config.cpp
   src/mc/mc_config.hpp
   src/mc/mc_global.cpp
-  src/mc/checker/SimcallInspector.cpp
-  src/mc/checker/SimcallInspector.hpp
+  src/mc/checker/SimcallObserver.cpp
+  src/mc/checker/SimcallObserver.hpp
   )
 
 set(MC_SRC