I was observing that the model_checking_mode global did not had the
same value when compiling with or without optimizations.
Maybe I had a sort of race condition on model_checking_mode during
initialization, or maybe the config element of the replay path was
either called before or after the initialization of the library, thus
replacing the model_checking_mode to REPLAY even if it was supposed to
be APP_SIDE in my case.
It's fixed now, but I'm not completely sure of which of these change
was the right one (probably the replay path). Both seem legit, so commit both.
#include "src/kernel/resource/profile/Profile.hpp"
#include "src/kernel/xml/platf.hpp"
#include "src/mc/mc.h"
#include "src/kernel/resource/profile/Profile.hpp"
#include "src/kernel/xml/platf.hpp"
#include "src/mc/mc.h"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_record.hpp"
#include "src/mc/mc_replay.hpp"
#include "src/simgrid/math_utils.h"
#include "src/mc/mc_record.hpp"
#include "src/mc/mc_replay.hpp"
#include "src/simgrid/math_utils.h"
+ XBT_DEBUG("Running the main loop until t=%.3f in mode %s", max_date,
+ to_c_str(simgrid::mc::get_model_checking_mode()));
+
if (MC_is_active()) {
#if SIMGRID_HAVE_MC
mc::AppSide::get()->main_loop();
if (MC_is_active()) {
#if SIMGRID_HAVE_MC
mc::AppSide::get()->main_loop();
xbt_assert(argc >= 2, "Missing arguments");
// Currently, we need this before sg_config_init:
xbt_assert(argc >= 2, "Missing arguments");
// Currently, we need this before sg_config_init:
- simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::CHECKER_SIDE;
+ simgrid::mc::set_model_checking_mode(simgrid::mc::ModelCheckingMode::CHECKER_SIDE);
// 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:
// 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/mc/mc.h"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_replay.hpp"
#include "src/mc/mc.h"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_replay.hpp"
-/*#include "src/mc/api/RemoteApp.hpp"
-#include "src/mc/remote/AppSide.hpp"*/
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/sosp/RemoteProcessMemory.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/sosp/RemoteProcessMemory.hpp"
*/
bool actor_is_enabled(kernel::actor::ActorImpl* actor)
{
*/
bool actor_is_enabled(kernel::actor::ActorImpl* actor)
{
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
// Now, we are in the client app, no need for remote memory reading.
"This should be called from the client side");
// Now, we are in the client app, no need for remote memory reading.
*/
bool request_is_visible(const kernel::actor::Simcall* req)
{
*/
bool request_is_visible(const kernel::actor::Simcall* req)
{
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
if (req->observer_ == nullptr)
"This should be called from the client side");
if (req->observer_ == nullptr)
int MC_random(int min, int max)
{
int MC_random(int min, int max)
{
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case
"This should be called from the client side");
if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case
void MC_assert(int prop)
{
// Cannot used xbt_assert here, or it would be an infinite recursion.
void MC_assert(int prop)
{
// Cannot used xbt_assert here, or it would be an infinite recursion.
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
#if SIMGRID_HAVE_MC
if (not prop) {
"This should be called from the client side");
#if SIMGRID_HAVE_MC
if (not prop) {
- return simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::APP_SIDE ||
- simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::CHECKER_SIDE;
+ return simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::APP_SIDE ||
+ simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::CHECKER_SIDE;
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
#if SIMGRID_HAVE_MC
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
#if SIMGRID_HAVE_MC
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
simgrid::mc::AppSide::get()->declare_symbol(name, value);
#endif
"This should be called from the client side");
simgrid::mc::AppSide::get()->declare_symbol(name, value);
#endif
void MC_ignore(void* addr, size_t size)
{
#if SIMGRID_HAVE_MC
void MC_ignore(void* addr, size_t size)
{
#if SIMGRID_HAVE_MC
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
simgrid::mc::AppSide::get()->ignore_memory(addr, size);
#endif
"This should be called from the client side");
simgrid::mc::AppSide::get()->ignore_memory(addr, size);
#endif
void MC_ignore_heap(void *address, size_t size)
{
#if SIMGRID_HAVE_MC
void MC_ignore_heap(void *address, size_t size)
{
#if SIMGRID_HAVE_MC
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
simgrid::mc::AppSide::get()->ignore_heap(address, size);
#endif
"This should be called from the client side");
simgrid::mc::AppSide::get()->ignore_heap(address, size);
#endif
void MC_unignore_heap(void* address, size_t size)
{
#if SIMGRID_HAVE_MC
void MC_unignore_heap(void* address, size_t size)
{
#if SIMGRID_HAVE_MC
- xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
"This should be called from the client side");
simgrid::mc::AppSide::get()->unignore_heap(address, size);
#endif
"This should be called from the client side");
simgrid::mc::AppSide::get()->unignore_heap(address, size);
#endif
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg);
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg);
-simgrid::mc::ModelCheckingMode simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::NONE;
+static simgrid::mc::ModelCheckingMode model_checking_mode = simgrid::mc::ModelCheckingMode::NONE;
+simgrid::mc::ModelCheckingMode simgrid::mc::get_model_checking_mode()
+{
+ return model_checking_mode;
+}
+void simgrid::mc::set_model_checking_mode(simgrid::mc::ModelCheckingMode mode)
+{
+ model_checking_mode = mode;
+}
static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
{
static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
{
simgrid::config::Flag<std::string> _sg_mc_record_path{
"model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "",
[](std::string_view value) {
simgrid::config::Flag<std::string> _sg_mc_record_path{
"model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "",
[](std::string_view value) {
- xbt_assert(value.empty() || simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::NONE ||
- simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::REPLAY,
+ if (value.empty()) // Ignore default value
+ return;
+ xbt_assert(simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::NONE ||
+ simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::REPLAY,
"Specifying a MC replay path is not allowed when running the model-checker in mode %s. "
"Either remove the model-check/replay parameter, or execute your code out of simgrid-mc.",
"Specifying a MC replay path is not allowed when running the model-checker in mode %s. "
"Either remove the model-check/replay parameter, or execute your code out of simgrid-mc.",
- to_c_str(simgrid::mc::model_checking_mode));
- simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::REPLAY;
+ to_c_str(simgrid::mc::get_model_checking_mode()));
+ simgrid::mc::set_model_checking_mode(simgrid::mc::ModelCheckingMode::REPLAY);
MC_record_path() = value;
}};
MC_record_path() = value;
}};
namespace simgrid::mc {
bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY);
namespace simgrid::mc {
bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY);
-extern XBT_PUBLIC ModelCheckingMode model_checking_mode;
+XBT_PUBLIC ModelCheckingMode get_model_checking_mode();
+XBT_PUBLIC void set_model_checking_mode(ModelCheckingMode mode);
};
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
};
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
AppSide* AppSide::get()
{
// Only initialize the MC world once
AppSide* AppSide::get()
{
// Only initialize the MC world once
+ if (instance_ != nullptr)
- if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
+ if (std::getenv(MC_ENV_SOCKET_FD) == nullptr) // We are not in MC mode: don't initialize the MC world
- simgrid::mc::model_checking_mode = ModelCheckingMode::APP_SIDE;
+ XBT_DEBUG("Initialize the MC world. MC_NEED_PTRACE=%s", std::getenv("MC_NEED_PTRACE"));
+
+ simgrid::mc::set_model_checking_mode(ModelCheckingMode::APP_SIDE);
setvbuf(stdout, nullptr, _IOLBF, 0);
setvbuf(stdout, nullptr, _IOLBF, 0);
answer.type = MessageType::FORK_REPLY;
answer.value = getpid();
xbt_assert(channel_.send(answer) == 0, "Could not send response to WAIT_CHILD_REPLY: %s", strerror(errno));
answer.type = MessageType::FORK_REPLY;
answer.value = getpid();
xbt_assert(channel_.send(answer) == 0, "Could not send response to WAIT_CHILD_REPLY: %s", strerror(errno));
+ } else {
+ XBT_DEBUG("App %d forks subprocess %d.", getpid(), pid);
}
}
void AppSide::handle_wait_child(const s_mc_message_int_t* msg)
}
}
void AppSide::handle_wait_child(const s_mc_message_int_t* msg)
/* When this constructor is called, no other checkerside exists */
CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_info) : running_(true)
{
/* When this constructor is called, no other checkerside exists */
CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_info) : running_(true)
{
+ XBT_DEBUG("Create a CheckerSide. Needs_meminfo: %s", need_memory_info ? "YES" : "no");
+
// Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor)
// and the application process (child)
int sockets[2];
// Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor)
// and the application process (child)
int sockets[2];
void CheckerSide::handle_waitpid()
{
void CheckerSide::handle_waitpid()
{
- XBT_DEBUG("Check for wait event");
+ XBT_DEBUG("%d checks for wait event. %s", getpid(),
+ child_checker_ == nullptr ? "Wait directly." : "Ask our proxy to wait for its child.");
if (child_checker_ == nullptr) { // Wait directly
int status;
if (child_checker_ == nullptr) { // Wait directly
int status;