Introduce a class mc::SimcallInspector, that allows MC to learn about the ongoing...

Not quite used yet.

diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h
index 8d4d26c..85eff8e 100644 (file)
--- a/include/simgrid/forward.h
+++ b/include/simgrid/forward.h
@@ -167,6 +167,7 @@ namespace surf {
 }
 namespace mc {
 class CommunicationDeterminismChecker;
 }
 namespace mc {
 class CommunicationDeterminismChecker;

+class SimcallInspector;

 }
 namespace vm {
 class VMModel;
 }
 namespace vm {
 class VMModel;

diff --git a/include/simgrid/simix.hpp b/include/simgrid/simix.hpp
index 08bb97b..473bb3f 100644 (file)
--- a/include/simgrid/simix.hpp
+++ b/include/simgrid/simix.hpp
@@ -16,26 +16,8 @@
 #include <string>
 #include <unordered_map>
 
 #include <string>
 #include <unordered_map>
 

-namespace simgrid {
-namespace kernel {
-namespace actor {
-
-class Transition {
-public:
-  virtual bool fireable()
-  {
-    return true;
-  } // whether this transition can currently be taken (if not, it could block the process)
-  virtual bool visible() { return true; } // whether the model-checker should pay any attention to this simcall
-  virtual std::string to_string() = 0;
-  virtual std::string dot_label() = 0;
-};
-} // namespace actor
-} // namespace kernel
-} // namespace simgrid
-
-XBT_PUBLIC void simcall_run_kernel(std::function<void()> const& code, simgrid::kernel::actor::Transition* t);
-XBT_PUBLIC void simcall_run_blocking(std::function<void()> const& code, simgrid::kernel::actor::Transition* t);
+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);

 
 namespace simgrid {
 namespace kernel {
 
 namespace simgrid {
 namespace kernel {


@@ -60,7 +42,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.
  */
  * 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<F()>::type simcall(F&& code, Transition* t = nullptr)
+template <class F> typename std::result_of<F()>::type simcall(F&& code, mc::SimcallInspector* t = nullptr)

 {
   // If we are in the maestro, we take the fast path and execute the
   // code directly without simcall mashalling/unmarshalling/dispatch:
 {
   // If we are in the maestro, we take the fast path and execute the
   // code directly without simcall mashalling/unmarshalling/dispatch:


@@ -90,7 +72,7 @@ template <class F> typename std::result_of<F()>::type simcall(F&& code, Transiti
  *
  * If your code never calls actor->simcall_answer() itself, the actor will never return from its simcall.
  */
  *
  * If your code never calls actor->simcall_answer() itself, the actor will never return from its simcall.
  */

-template <class F> typename std::result_of<F()>::type simcall_blocking(F&& code, Transition* t = nullptr)
+template <class F> typename std::result_of<F()>::type simcall_blocking(F&& code, mc::SimcallInspector* t = nullptr)

 {
   // If we are in the maestro, we take the fast path and execute the
   // code directly without simcall mashalling/unmarshalling/dispatch:
 {
   // If we are in the maestro, we take the fast path and execute the
   // code directly without simcall mashalling/unmarshalling/dispatch:

diff --git a/src/mc/checker/SimcallInspector.hpp b/src/mc/checker/SimcallInspector.hpp
new file mode 100644 (file)
index 0000000..d1327f3
--- /dev/null
+++ b/src/mc/checker/SimcallInspector.hpp
@@ -0,0 +1,32 @@
+/* Copyright (c) 2019. 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. */
+
+#ifndef SIMGRID_MC_SIMCALL_INSPECTOR_HPP
+#define SIMGRID_MC_SIMCALL_INSPECTOR_HPP
+
+#include <string>
+
+namespace simgrid {
+namespace mc {
+
+class SimcallInspector {
+public:
+  /** whether this transition can currently be taken without blocking.
+   *
+   * For example, a mutex_lock is not enabled when the mutex is not free.
+   * A comm_receive is not enabled before the corresponding send has been issued.
+   */
+  virtual bool is_enabled() { return true; }
+
+  /** Some simcalls may only be observable under some circomstances.
+   * Most simcalls are not visible from the MC because they don't have an inspector at all. */
+  virtual bool is_visible() { return true; }
+  virtual std::string to_string() = 0;
+  virtual std::string dot_label() = 0;
+};
+} // namespace mc
+} // namespace simgrid
+
+#endif

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 7b6bcc9..c75d927 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -7,6 +7,7 @@
 #include "mc/mc.h"
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
 #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/mc_replay.hpp"
 #include "src/simix/smx_private.hpp"
 
 #include "src/mc/mc_replay.hpp"
 #include "src/simix/smx_private.hpp"
 


@@ -78,8 +79,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;
 
   // Now, we are in the client app, no need for remote memory reading.
   smx_simcall_t req = &actor->simcall;
 

-  if (req->transition_ != nullptr)
-    return req->transition_->fireable();
+  if (req->inspector_ != nullptr)
+    return req->inspector_->is_enabled();

 
   switch (req->call_) {
     case SIMCALL_NONE:
 
   switch (req->call_) {
     case SIMCALL_NONE:


@@ -153,7 +154,7 @@ bool request_is_visible(smx_simcall_t req)
   xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
 #endif
 
   xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
 #endif
 

-  return (req->transition_ != nullptr && req->transition_->visible()) || req->call_ == SIMCALL_COMM_ISEND ||
+  return (req->inspector_ != nullptr && req->inspector_->is_visible()) || req->call_ == SIMCALL_COMM_ISEND ||

          req->call_ == SIMCALL_COMM_IRECV || req->call_ == SIMCALL_COMM_WAIT || req->call_ == SIMCALL_COMM_WAITANY ||
          req->call_ == SIMCALL_COMM_TEST || req->call_ == SIMCALL_COMM_TESTANY || req->call_ == SIMCALL_MC_RANDOM ||
          req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK || req->call_ == SIMCALL_MUTEX_UNLOCK;
          req->call_ == SIMCALL_COMM_IRECV || req->call_ == SIMCALL_COMM_WAIT || req->call_ == SIMCALL_COMM_WAITANY ||
          req->call_ == SIMCALL_COMM_TEST || req->call_ == SIMCALL_COMM_TESTANY || req->call_ == SIMCALL_MC_RANDOM ||
          req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK || req->call_ == SIMCALL_MUTEX_UNLOCK;

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index 539143d..ff543ee 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -8,6 +8,7 @@
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/mc/ModelChecker.hpp"
 #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/mc_smx.hpp"
 
 using simgrid::mc::remote;
 #include "src/mc/mc_smx.hpp"
 
 using simgrid::mc::remote;


@@ -175,8 +176,8 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid
 {
   xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
 
 {
   xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
 

-  if (req->transition_ != nullptr)
-    return req->transition_->to_string();
+  if (req->inspector_ != nullptr)
+    return req->inspector_->to_string();

 
   bool use_remote_comm = true;
   switch(request_type) {
 
   bool use_remote_comm = true;
   switch(request_type) {


@@ -420,9 +421,9 @@ std::string request_get_dot_output(smx_simcall_t req, int value)
   const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
   const char* color        = get_color(issuer->get_pid() - 1);
 
   const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
   const char* color        = get_color(issuer->get_pid() - 1);
 

-  if (req->transition_ != nullptr)
+  if (req->inspector_ != nullptr)

     return simgrid::xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s",
     return simgrid::xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s",

-                                       req->transition_->dot_label().c_str(), color, color);
+                                       req->inspector_->dot_label().c_str(), color, color);

 
   std::string label;
 
 
   std::string label;
 

diff --git a/src/simix/libsmx.cpp b/src/simix/libsmx.cpp
index 134f417..5c2f919 100644 (file)
--- a/src/simix/libsmx.cpp
+++ b/src/simix/libsmx.cpp
@@ -307,15 +307,15 @@ e_smx_state_t simcall_io_wait(const smx_activity_t& io)
   return (e_smx_state_t)simcall_BODY_io_wait(static_cast<simgrid::kernel::activity::IoImpl*>(io.get()));
 }
 
   return (e_smx_state_t)simcall_BODY_io_wait(static_cast<simgrid::kernel::activity::IoImpl*>(io.get()));
 }
 

-void simcall_run_kernel(std::function<void()> const& code, simgrid::kernel::actor::Transition* t)
+void simcall_run_kernel(std::function<void()> const& code, simgrid::mc::SimcallInspector* t)

 {
 {

-  SIMIX_process_self()->simcall.transition_ = t;
+  SIMIX_process_self()->simcall.inspector_ = t;

   simcall_BODY_run_kernel(&code);
 }
 
   simcall_BODY_run_kernel(&code);
 }
 

-void simcall_run_blocking(std::function<void()> const& code, simgrid::kernel::actor::Transition* t = nullptr)
+void simcall_run_blocking(std::function<void()> const& code, simgrid::mc::SimcallInspector* t = nullptr)

 {
 {

-  SIMIX_process_self()->simcall.transition_ = t;
+  SIMIX_process_self()->simcall.inspector_ = t;

   simcall_BODY_run_blocking(&code);
 }
 
   simcall_BODY_run_blocking(&code);
 }
 

diff --git a/src/simix/popping_private.hpp b/src/simix/popping_private.hpp
index 00d77e2..338a29b 100644 (file)
--- a/src/simix/popping_private.hpp
+++ b/src/simix/popping_private.hpp
@@ -46,7 +46,7 @@ struct s_smx_simcall {
   e_smx_simcall_t call_;
   smx_actor_t issuer_;
   smx_timer_t timeout_cb_; // Callback to timeouts
   e_smx_simcall_t call_;
   smx_actor_t issuer_;
   smx_timer_t timeout_cb_; // Callback to timeouts

-  simgrid::kernel::actor::Transition* transition_ = nullptr;
+  simgrid::mc::SimcallInspector* inspector_ = nullptr; // makes that simcall observable by the MC

   int mc_value_;
   u_smx_scalar args_[11];
   u_smx_scalar result_;
   int mc_value_;
   u_smx_scalar args_[11];
   u_smx_scalar result_;

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index ad1948d..e8b8b96 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -595,6 +595,7 @@ set(MC_SRC
   src/mc/checker/CommunicationDeterminismChecker.hpp
   src/mc/checker/SafetyChecker.cpp
   src/mc/checker/SafetyChecker.hpp
   src/mc/checker/CommunicationDeterminismChecker.hpp
   src/mc/checker/SafetyChecker.cpp
   src/mc/checker/SafetyChecker.hpp

+  src/mc/checker/SimcallInspector.hpp

   src/mc/checker/LivenessChecker.cpp
   src/mc/checker/LivenessChecker.hpp
   
   src/mc/checker/LivenessChecker.cpp
   src/mc/checker/LivenessChecker.hpp