#ifndef SIMGRID_MODELCHECKER_H
#define SIMGRID_MODELCHECKER_H
-#include <simgrid/config.h> /* SIMGRID_HAVE_MC ? */
-#include <xbt/base.h>
-
#include <stddef.h> /* size_t */
+#include <xbt/base.h>
SG_BEGIN_DECL
/** Explore every branches where that function returns a value between min and max (inclusive) */
XBT_PUBLIC int MC_random(int min, int max);
-#if SIMGRID_HAVE_MC
-
-/* Internal variable used to check if we're running under the MC. Please use MC_is_active instead. */
-extern XBT_PUBLIC int _sg_do_model_check;
-extern XBT_PUBLIC int _sg_mc_max_visited_states;
-
-#define MC_is_active() _sg_do_model_check
-#define MC_visited_reduction() _sg_mc_max_visited_states
-
-/** Assertion for the model-checker
- *
- * This function is used to define safety properties to verify.
- */
+/** Assertion for the model-checker: Defines a safety property to verify */
XBT_PUBLIC void MC_assert(int);
-XBT_PUBLIC void MC_automaton_new_propositional_symbol(const char* id, int (*fct)(void));
+/** Check whether the model-checker is currently active, ie if this process was started with simgrid-mc.
+ * It is off in simulation or when replaying MC traces (see MC_record_replay_is_active()) */
+XBT_PUBLIC int MC_is_active();
+
XBT_PUBLIC void MC_automaton_new_propositional_symbol_pointer(const char* id, int* value);
XBT_PUBLIC void MC_ignore(void* addr, size_t size);
XBT_PUBLIC void MC_ignore_heap(void* address, size_t size);
XBT_PUBLIC void MC_unignore_heap(void* address, size_t size);
-#else
-
-#define MC_is_active() 0
-#define MC_visited_reduction() 0
-
-#define MC_assert(a) xbt_assert(a)
-
-#define MC_automaton_new_propositional_symbol(a, b) ((void)0)
-#define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0)
-
-#define MC_ignore(a, b) ((void)0)
-#define MC_ignore_heap(a, s) ((void)0)
-#define MC_unignore_heap(a, s) ((void)0)
-
-#endif
-
SG_END_DECL
#endif /* SIMGRID_MODELCHECKER_H */
#include "src/mc/VisitedState.hpp"
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_private.hpp"
#include <unistd.h>
xbt_assert(argc >= 2, "Missing arguments");
// Currently, we need this before sg_config_init:
- _sg_do_model_check = 1;
+ simgrid::mc::cfg_do_model_check = 1;
// The initialization function can touch argv.
// We make a copy of argv before modifying it in order to pass the original value to the model-checked application:
#include "src/kernel/activity/CommImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/kernel/actor/SimcallObserver.hpp"
-#include "src/mc/mc_config.hpp"
#include "src/mc/mc_replay.hpp"
-#include "xbt/random.hpp"
-
#if SIMGRID_HAVE_MC
#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/remote/AppSide.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
#endif
XBT_LOG_NEW_DEFAULT_CATEGORY(mc, "All MC categories");
-int MC_random(int min, int max)
-{
-#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr);
-#endif
- if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case
- static simgrid::xbt::random::XbtRandom prng;
- return prng.uniform_int(min, max);
- }
- simgrid::kernel::actor::RandomSimcall observer{simgrid::kernel::actor::ActorImpl::self(), min, max};
- return simgrid::kernel::actor::simcall_answered([&observer] { return observer.get_value(); }, &observer);
-}
-
namespace simgrid::mc {
void execute_actors()
-/* Copyright (c) 2008-2022. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2008-2022. 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. */
+/* Implementation of the user API from the App to the Checker (see modelchecker.h) */
+
#include "src/mc/ModelChecker.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
#include "src/mc/mc_replay.hpp"
#include "src/mc/remote/AppSide.hpp"
#include "xbt/asserts.h"
+#include "xbt/random.hpp"
-/** @file mc_client_api.cpp
- *
- * This is the implementation of the API used by the user simulated program to
- * communicate with the MC (declared in modelchecker.h).
- */
-
-// MC_random() is in mc_base.cpp
+int MC_random(int min, int max)
+{
+#if SIMGRID_HAVE_MC
+ xbt_assert(mc_model_checker == nullptr);
+#endif
+ if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case
+ static simgrid::xbt::random::XbtRandom prng;
+ return prng.uniform_int(min, max);
+ }
+ simgrid::kernel::actor::RandomSimcall observer{simgrid::kernel::actor::ActorImpl::self(), min, max};
+ return simgrid::kernel::actor::simcall_answered([&observer] { return observer.get_value(); }, &observer);
+}
void MC_assert(int prop)
{
+#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr);
if (not prop) {
if (MC_is_active())
if (MC_record_replay_is_active())
xbt_die("MC assertion failed");
}
+#else
+ xbt_assert(prop, "Safety property violation detected without the model-checker");
+#endif
}
-void MC_automaton_new_propositional_symbol(const char* /*id*/, int (*/*fct*/)())
+int MC_is_active()
{
- xbt_assert(mc_model_checker == nullptr);
- if (not MC_is_active())
- return;
- xbt_die("Support for client-side function proposition is not implemented: "
- "use MC_automaton_new_propositional_symbol_pointer instead.");
+ return simgrid::mc::cfg_do_model_check;
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
+#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
simgrid::mc::AppSide::get()->declare_symbol(name, value);
+#endif
}
void MC_ignore(void* addr, size_t size)
{
+#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
simgrid::mc::AppSide::get()->ignore_memory(addr, size);
+#endif
}
void MC_ignore_heap(void *address, size_t size)
{
+#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr);
simgrid::mc::AppSide::get()->ignore_heap(address, size);
+#endif
}
void MC_unignore_heap(void* address, size_t size)
{
+#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr);
simgrid::mc::AppSide::get()->unignore_heap(address, size);
+#endif
}
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_replay.hpp"
+#include <simgrid/modelchecker.h>
#include <simgrid/sg_config.hpp>
#if SIMGRID_HAVE_MC
#include <string_view>
-
-#else
-#define _sg_do_model_check 0
#endif
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg);
+bool simgrid::mc::cfg_do_model_check = 0;
+
static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
{
- xbt_assert(_sg_cfg_init_status == 0 || _sg_do_model_check || not more_check,
+#if SIMGRID_HAVE_MC
+ xbt_assert(_sg_cfg_init_status == 0 || MC_is_active() || not more_check,
"Specifying a %s is only allowed within the model-checker. Please use simgrid-mc.", spec);
+#else
+ xbt_die("Specifying a %s is only allowed within the model-checker. Please enable it before the compilation.", spec);
+#endif
}
/* Replay (this part is enabled even if MC it disabled) */
"model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "",
[](std::string_view value) { MC_record_path() = value; }};
+#if SIMGRID_HAVE_MC
simgrid::config::Flag<bool> _sg_mc_timeout{
"model-check/timeout", "Whether to enable timeouts for wait requests", false, [](bool) {
_mc_cfg_cb_check("value to enable/disable timeout for wait requests", not MC_record_replay_is_active());
}};
-#if SIMGRID_HAVE_MC
-int _sg_do_model_check = 0;
int _sg_mc_max_visited_states = 0;
static simgrid::config::Flag<std::string> cfg_mc_reduction{
/********************************** Configuration of MC **************************************/
namespace simgrid::mc {
bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
+extern XBT_PUBLIC bool cfg_do_model_check;
};
-extern "C" XBT_PUBLIC int _sg_do_model_check;
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_property_file;
#include "src/kernel/actor/ActorImpl.hpp"
#include "src/kernel/actor/SimcallObserver.hpp"
#include "src/mc/mc_base.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
#if HAVE_SMPI
#include "src/smpi/include/private.hpp"
if (instance_)
return instance_.get();
- _sg_do_model_check = 1;
+ simgrid::mc::cfg_do_model_check = 1;
setvbuf(stdout, nullptr, _IOLBF, 0);
set(MC_SRC_BASE
src/mc/mc_base.cpp
src/mc/mc_base.hpp
+ src/mc/mc_client_api.cpp
src/mc/mc_config.cpp
src/mc/mc_config.hpp
src/mc/mc_global.cpp
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
src/mc/compare.cpp
- src/mc/mc_client_api.cpp
src/mc/mc_exit.hpp
src/mc/mc_forward.hpp
src/mc/mc_private.hpp
