From dd493bf4a168bd2b379810313916e1a4e0898388 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 2 Aug 2022 00:15:48 +0200 Subject: [PATCH] Ensure that the verified application still works if get_max_consider() is not called at a given depth This can happen after a backtrack: the Checker already knows how many times this can be considered, but the App was reset in between so it forgot. So, make get_max_consider() const, and do the initialization in the observer constructor, where it belongs. Too bad for the tiny little tiny loss of performance compared to the lazy initialization. --- src/kernel/actor/CommObserver.cpp | 21 ++++++++++----------- src/kernel/actor/CommObserver.hpp | 4 ++-- src/kernel/actor/SimcallObserver.cpp | 2 +- src/kernel/actor/SimcallObserver.hpp | 4 ++-- src/mc/mc_base.cpp | 4 +--- 5 files changed, 16 insertions(+), 19 deletions(-) diff --git a/src/kernel/actor/CommObserver.cpp b/src/kernel/actor/CommObserver.cpp index f44571e5bc..e15d6aa877 100644 --- a/src/kernel/actor/CommObserver.cpp +++ b/src/kernel/actor/CommObserver.cpp @@ -18,16 +18,16 @@ namespace simgrid::kernel::actor { ActivityTestanySimcall::ActivityTestanySimcall(ActorImpl* actor, const std::vector& activities) : ResultingSimcall(actor, -1), activities_(activities) -{ -} - -int ActivityTestanySimcall::get_max_consider() { indexes_.clear(); // list all the activities that are ready for (unsigned i = 0; i < activities_.size(); i++) if (activities_[i]->test(get_issuer())) indexes_.push_back(i); +} + +int ActivityTestanySimcall::get_max_consider() const +{ return indexes_.size() + 1; } @@ -94,6 +94,11 @@ ActivityWaitanySimcall::ActivityWaitanySimcall(ActorImpl* actor, const std::vect double timeout) : ResultingSimcall(actor, -1), activities_(activities), timeout_(timeout) { + // list all the activities that are ready + indexes_.clear(); + for (unsigned i = 0; i < activities_.size(); i++) + if (activities_[i]->test(get_issuer())) + indexes_.push_back(i); } bool ActivityWaitSimcall::is_enabled() @@ -119,14 +124,8 @@ bool ActivityWaitanySimcall::is_enabled() return not indexes_.empty(); } -int ActivityWaitanySimcall::get_max_consider() +int ActivityWaitanySimcall::get_max_consider() const { - // list all the activities that are ready - indexes_.clear(); - for (unsigned i = 0; i < activities_.size(); i++) - if (activities_[i]->test(get_issuer())) - indexes_.push_back(i); - int res = indexes_.size(); // if (_sg_mc_timeout && timeout_) // res++; diff --git a/src/kernel/actor/CommObserver.hpp b/src/kernel/actor/CommObserver.hpp index 9cba17d454..41607aa580 100644 --- a/src/kernel/actor/CommObserver.hpp +++ b/src/kernel/actor/CommObserver.hpp @@ -38,7 +38,7 @@ public: bool is_visible() const override { return true; } bool is_enabled() override { return true; /* can return -1 if no activity is ready */ } void serialize(std::stringstream& stream) const override; - int get_max_consider() override; + int get_max_consider() const override; void prepare(int times_considered) override; const std::vector& get_activities() const { return activities_; } int get_value() const { return next_value_; } @@ -73,7 +73,7 @@ public: void serialize(std::stringstream& stream) const override; bool is_visible() const override { return true; } void prepare(int times_considered) override; - int get_max_consider() override; + int get_max_consider() const override; const std::vector& get_activities() const { return activities_; } double get_timeout() const { return timeout_; } int get_value() const { return next_value_; } diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index e4ffca22ff..87991ccefa 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -32,7 +32,7 @@ void RandomSimcall::prepare(int times_considered) XBT_DEBUG("MC_RANDOM(%d, %d) will return %d after %d times", min_, max_, next_value_, times_considered); } -int RandomSimcall::get_max_consider() +int RandomSimcall::get_max_consider() const { return max_ - min_ + 1; } diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp index 6eabf88b57..a4095e4a42 100644 --- a/src/kernel/actor/SimcallObserver.hpp +++ b/src/kernel/actor/SimcallObserver.hpp @@ -37,7 +37,7 @@ public: * If it's more than one (as with mc_random or waitany), we need to consider this transition several times to start * differing branches */ - virtual int get_max_consider() { return 1; } + virtual int get_max_consider() const { return 1; } /** Prepares the simcall to be used. * @@ -83,7 +83,7 @@ public: xbt_assert(min < max); } void serialize(std::stringstream& stream) const override; - int get_max_consider() override; + int get_max_consider() const override; void prepare(int times_considered) override; int get_value() const { return next_value_; } }; diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 93eef1ae19..a35833c032 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -40,9 +40,7 @@ namespace simgrid::mc { void execute_actors() { auto* engine = kernel::EngineImpl::get_instance(); -#if SIMGRID_HAVE_MC - xbt_assert(mc_model_checker == nullptr, "This must be called from the client"); -#endif + while (engine->has_actors_to_run()) { engine->run_all_actors(); for (auto const& actor : engine->get_actors_that_ran()) { -- 2.20.1