From 42e47242b26a374aa63a9a29b1ac79c443213220 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 16 Oct 2022 23:59:01 +0200 Subject: [PATCH] Don't include simgrid/config.h from simgrid/modelchecker.h so that the later is cheap to load The functions are now generated in any case, and only do something when SIMGRID_HAVE_MC is compiled in. Also: - kill MC_automaton_new_propositional_symbol() that was never implemented - kill MC_visited_reduction() that was not used (anymore?) - Convert _sg_do_model_check to simgrid::mc::cfg_do_model_check --- include/simgrid/modelchecker.h | 39 +++++---------------------- src/mc/VisitedState.cpp | 1 + src/mc/explo/simgrid_mc.cpp | 2 +- src/mc/mc_base.cpp | 17 +----------- src/mc/mc_client_api.cpp | 46 +++++++++++++++++++++----------- src/mc/mc_config.cpp | 15 ++++++----- src/mc/mc_config.hpp | 2 +- src/mc/remote/AppSide.cpp | 3 ++- tools/cmake/DefinePackages.cmake | 2 +- 9 files changed, 53 insertions(+), 74 deletions(-) diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 69217b7e43..f9c67cb13e 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -8,54 +8,27 @@ #ifndef SIMGRID_MODELCHECKER_H #define SIMGRID_MODELCHECKER_H -#include /* SIMGRID_HAVE_MC ? */ -#include - #include /* size_t */ +#include 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 */ diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index 8264c2a6e4..0b04eddad7 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -5,6 +5,7 @@ #include "src/mc/VisitedState.hpp" #include "src/mc/explo/Exploration.hpp" +#include "src/mc/mc_config.hpp" #include "src/mc/mc_private.hpp" #include diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp index d540f2acf5..b9e33e7810 100644 --- a/src/mc/explo/simgrid_mc.cpp +++ b/src/mc/explo/simgrid_mc.cpp @@ -21,7 +21,7 @@ int main(int argc, char** argv) 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: diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 91012ba602..781a5ee262 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -9,32 +9,17 @@ #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() diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index e64019f7c1..d2dd997a3a 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -1,26 +1,35 @@ -/* 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()) @@ -28,41 +37,48 @@ void MC_assert(int prop) 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 } diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index fb1b1a6d8d..63a083e4f8 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -5,21 +5,25 @@ #include "src/mc/mc_config.hpp" #include "src/mc/mc_replay.hpp" +#include #include #if SIMGRID_HAVE_MC #include - -#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) */ @@ -27,13 +31,12 @@ simgrid::config::Flag _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) { MC_record_path() = value; }}; +#if SIMGRID_HAVE_MC simgrid::config::Flag _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 cfg_mc_reduction{ diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index 39e07cdf52..52e20db6da 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -11,9 +11,9 @@ /********************************** 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 _sg_mc_buffering; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_checkpoint; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_property_file; diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 541089809e..e3c5651659 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -10,6 +10,7 @@ #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" @@ -43,7 +44,7 @@ AppSide* AppSide::initialize() if (instance_) return instance_.get(); - _sg_do_model_check = 1; + simgrid::mc::cfg_do_model_check = 1; setvbuf(stdout, nullptr, _IOLBF, 0); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index e9b706048d..f8dae81003 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -562,6 +562,7 @@ set(TRACING_SRC 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 @@ -644,7 +645,6 @@ set(MC_SRC 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 -- 2.20.1