Not quite used yet.
}
namespace mc {
class CommunicationDeterminismChecker;
+class SimcallInspector;
}
namespace vm {
class VMModel;
#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 {
* 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 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:
--- /dev/null
+/* 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
#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"
// 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:
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;
#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;
{
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) {
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;
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);
}
-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);
}
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_;
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