From 2ace2e9a66953011268a2b64824638305807612e Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 13 Aug 2019 22:54:53 +0200 Subject: [PATCH] Introduce a class mc::SimcallInspector, that allows MC to learn about the ongoing simcalls Not quite used yet. --- include/simgrid/forward.h | 1 + include/simgrid/simix.hpp | 26 ++++------------------- src/mc/checker/SimcallInspector.hpp | 32 +++++++++++++++++++++++++++++ src/mc/mc_base.cpp | 7 ++++--- src/mc/mc_request.cpp | 9 ++++---- src/simix/libsmx.cpp | 8 ++++---- src/simix/popping_private.hpp | 2 +- tools/cmake/DefinePackages.cmake | 1 + 8 files changed, 52 insertions(+), 34 deletions(-) create mode 100644 src/mc/checker/SimcallInspector.hpp diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h index 8d4d26c986..85eff8e2ae 100644 --- a/include/simgrid/forward.h +++ b/include/simgrid/forward.h @@ -167,6 +167,7 @@ namespace surf { } namespace mc { class CommunicationDeterminismChecker; +class SimcallInspector; } namespace vm { class VMModel; diff --git a/include/simgrid/simix.hpp b/include/simgrid/simix.hpp index 08bb97b713..473bb3f4b1 100644 --- a/include/simgrid/simix.hpp +++ b/include/simgrid/simix.hpp @@ -16,26 +16,8 @@ #include #include -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 const& code, simgrid::kernel::actor::Transition* t); -XBT_PUBLIC void simcall_run_blocking(std::function const& code, simgrid::kernel::actor::Transition* t); +XBT_PUBLIC void simcall_run_kernel(std::function const& code, simgrid::mc::SimcallInspector* t); +XBT_PUBLIC void simcall_run_blocking(std::function const& code, simgrid::mc::SimcallInspector* t); 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. */ -template typename std::result_of::type simcall(F&& code, Transition* t = nullptr) +template typename std::result_of::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: @@ -90,7 +72,7 @@ template typename std::result_of::type simcall(F&& code, Transiti * * If your code never calls actor->simcall_answer() itself, the actor will never return from its simcall. */ -template typename std::result_of::type simcall_blocking(F&& code, Transition* t = nullptr) +template typename std::result_of::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: diff --git a/src/mc/checker/SimcallInspector.hpp b/src/mc/checker/SimcallInspector.hpp new file mode 100644 index 0000000000..d1327f3c20 --- /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 + +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 7b6bcc93fa..c75d927c05 100644 --- 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 "src/mc/checker/SimcallInspector.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; - if (req->transition_ != nullptr) - return req->transition_->fireable(); + if (req->inspector_ != nullptr) + return req->inspector_->is_enabled(); 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 - 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; diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index 539143d711..ff543ee802 100644 --- 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/mc/checker/SimcallInspector.hpp" #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"); - 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) { @@ -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); - if (req->transition_ != nullptr) + if (req->inspector_ != nullptr) 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; diff --git a/src/simix/libsmx.cpp b/src/simix/libsmx.cpp index 134f4171d6..5c2f919ddc 100644 --- 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(io.get())); } -void simcall_run_kernel(std::function const& code, simgrid::kernel::actor::Transition* t) +void simcall_run_kernel(std::function const& code, simgrid::mc::SimcallInspector* t) { - SIMIX_process_self()->simcall.transition_ = t; + SIMIX_process_self()->simcall.inspector_ = t; simcall_BODY_run_kernel(&code); } -void simcall_run_blocking(std::function const& code, simgrid::kernel::actor::Transition* t = nullptr) +void simcall_run_blocking(std::function const& code, simgrid::mc::SimcallInspector* t = nullptr) { - SIMIX_process_self()->simcall.transition_ = t; + SIMIX_process_self()->simcall.inspector_ = t; simcall_BODY_run_blocking(&code); } diff --git a/src/simix/popping_private.hpp b/src/simix/popping_private.hpp index 00d77e2dc2..338a29b617 100644 --- 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 - 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_; diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index ad1948d9fc..e8b8b96fb2 100644 --- 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/SimcallInspector.hpp src/mc/checker/LivenessChecker.cpp src/mc/checker/LivenessChecker.hpp -- 2.20.1