From: mlaurent Date: Tue, 6 Jun 2023 09:57:25 +0000 (+0200) Subject: Add factorisation for strategy and Use dynamic over static cast X-Git-Tag: v3.34~41^2~11 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0e6845546f978a7391692a2dc0e9fd2527132241 Add factorisation for strategy and Use dynamic over static cast --- diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh index 204b615952..b113f49eef 100644 --- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh +++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh @@ -28,14 +28,14 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [0.000000] [mc_explo/INFO] Counter-example execution trace: > [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) > [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) > [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) > [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 2: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;2;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 930 unique states visited; 207 backtracks (2195 transition replays, 3332 states visited overall) +> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;3;3;2;1;1;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 662 unique states visited; 144 backtracks (1540 transition replays, 2346 states visited overall) ! expect return 1 ! timeout 20 @@ -53,4 +53,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) > [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 173 unique states visited; 29 backtracks (286 transition replays, 488 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 64 unique states visited; 5 backtracks (23 transition replays, 92 states visited overall) \ No newline at end of file diff --git a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh index 3e9aa79b03..7c418cf725 100644 --- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh @@ -28,14 +28,15 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID *** > [0.000000] [mc_explo/INFO] ************************** > [0.000000] [mc_explo/INFO] Counter-example execution trace: -> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) > [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) > [0.000000] [mc_explo/INFO] 2: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;1;1;1;2;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 29 unique states visited; 5 backtracks (17 transition replays, 51 states visited overall) +> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall) ! expect return 1 @@ -48,32 +49,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID *** > [0.000000] [mc_explo/INFO] ************************** > [0.000000] [mc_explo/INFO] Counter-example execution trace: -> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0) -> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;1;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall) - -! expect return 1 -! timeout 300 -$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42' -> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none. -> [0.000000] [mc_explo/INFO] ************************** -> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID *** -> [0.000000] [mc_explo/INFO] ************************** -> [0.000000] [mc_explo/INFO] Counter-example execution trace: > [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 2: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) > [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;2;1;3;1;1;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 7 backtracks (19 transition replays, 70 states visited overall) \ No newline at end of file +> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;2;1;1;3;1;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (0 transition replays, 25 states visited overall) \ No newline at end of file diff --git a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh index 5404b6e493..3eda998bbc 100644 --- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh @@ -34,8 +34,9 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c ! timeout 20 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:min_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning > [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor. -> [ 0.000000] (1:server@Boivin) OK > [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (1:server@Boivin) OK +> [ 0.000000] (3:client2@Fafard) Sent! > [ 0.000000] (3:client2@Fafard) Sent! > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** @@ -45,17 +46,19 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 0.000000] (0:maestro@) 3: iSend(mbox=0) > [ 0.000000] (0:maestro@) 2: iSend(mbox=0) > [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout) > [ 0.000000] (0:maestro@) 1: iRecv(mbox=0) > [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout) -> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;1;1' -> [ 0.000000] (0:maestro@) DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall) +> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;3;1;1' +> [ 0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 3 backtracks (1 transition replays, 22 states visited overall) ! expect return 1 ! timeout 20 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:max_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning > [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor. -> [ 0.000000] (1:server@Boivin) OK > [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (1:server@Boivin) OK +> [ 0.000000] (3:client2@Fafard) Sent! > [ 0.000000] (3:client2@Fafard) Sent! > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** @@ -64,8 +67,9 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 0.000000] (0:maestro@) 1: iRecv(mbox=0) > [ 0.000000] (0:maestro@) 3: iSend(mbox=0) > [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout) > [ 0.000000] (0:maestro@) 1: iRecv(mbox=0) > [ 0.000000] (0:maestro@) 2: iSend(mbox=0) > [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout) -> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1' -> [ 0.000000] (0:maestro@) DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall) \ No newline at end of file +> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1' +> [ 0.000000] (0:maestro@) DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall) \ No newline at end of file diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh index 3ce27b16f2..dd4f3c19db 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -82,11 +82,3 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2' > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. > [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (49 transition replays, 126 states visited overall) - -$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '3' -> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 647 unique states visited; 122 backtracks (871 transition replays, 1640 states visited overall) \ No newline at end of file diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh index 94c7cb7413..84efe3040f 100644 --- a/examples/sthread/pthread-mc-producer-consumer.tesh +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -7,10 +7,3 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. > [0.000000] [mc_dfs/INFO] DFS exploration ended. 103 unique states visited; 16 backtracks (163 transition replays, 282 states visited overall) -$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -c 2 -C 1 -p 2 -P 1 -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform' -> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42' -> [0.000000] [sthread/INFO] Starting the simulation. -> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 91 unique states visited; 11 backtracks (116 transition replays, 218 states visited overall) \ No newline at end of file diff --git a/src/mc/api/strategy/BasicStrategy.hpp b/src/mc/api/strategy/BasicStrategy.hpp index 42676d437d..175425252e 100644 --- a/src/mc/api/strategy/BasicStrategy.hpp +++ b/src/mc/api/strategy/BasicStrategy.hpp @@ -13,12 +13,12 @@ namespace simgrid::mc { /** Basic MC guiding class which corresponds to no guide. When asked for different states * it will follow a depth first search politics to minize the number of opened states. */ class BasicStrategy : public Strategy { - int depth_ = 100000; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer + int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer public: void copy_from(const Strategy* strategy) override { - const BasicStrategy* cast_strategy = static_cast(strategy); + const BasicStrategy* cast_strategy = dynamic_cast(strategy); xbt_assert(cast_strategy != nullptr); depth_ = cast_strategy->depth_ - 1; xbt_assert(depth_ > 0, "The exploration reached a depth greater than 100000. We will stop here to prevent weird interaction with DFSExplorer."); @@ -26,31 +26,22 @@ public: BasicStrategy() = default; ~BasicStrategy() override = default; - std::pair next_transition() const override - { - for (auto const& [aid, actor] : actors_to_run_) { - /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */ - if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) { + std::pair best_transition(bool must_be_todo) const override { + for (auto const& [aid, actor] : actors_to_run_) { + /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */ + if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) { continue; } return std::make_pair(aid, depth_); } return std::make_pair(-1, depth_); + } + - void consider_best() override - { - for (auto& [_, actor] : actors_to_run_) - if (actor.is_todo()) - return; - - for (auto& [_, actor] : actors_to_run_) - if (actor.is_enabled() and not actor.is_done()) - actor.mark_todo(); - + void execute_next(aid_t aid, RemoteApp& app) override { return; } - } }; } // namespace simgrid::mc diff --git a/src/mc/api/strategy/MaxMatchComm.hpp b/src/mc/api/strategy/MaxMatchComm.hpp index b5f974c222..a2f1d601a5 100644 --- a/src/mc/api/strategy/MaxMatchComm.hpp +++ b/src/mc/api/strategy/MaxMatchComm.hpp @@ -26,7 +26,7 @@ class MaxMatchComm : public Strategy { public: void copy_from(const Strategy* strategy) override { - const MaxMatchComm* cast_strategy = static_cast(strategy); + const MaxMatchComm* cast_strategy = dynamic_cast(strategy); xbt_assert(cast_strategy != nullptr); for (auto& [id, val] : cast_strategy->mailbox_) mailbox_[id] = val; @@ -41,78 +41,58 @@ public: MaxMatchComm() = default; ~MaxMatchComm() override = default; - std::pair next_transition() const override + std::pair best_transition(bool must_be_todo) const override { - std::pair if_no_match = std::make_pair(-1, 0); + std::pair min_found = std::make_pair(-1, value_of_state_+2); for (auto const& [aid, actor] : actors_to_run_) { - if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) - continue; + if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) + continue; + int aid_value = value_of_state_; const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); - - const CommRecvTransition* cast_recv = static_cast(transition); - if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and - mailbox_.at(cast_recv->get_mailbox()) > 0) - return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting send corresponding to this recv - - const CommSendTransition* cast_send = static_cast(transition); - if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and - mailbox_.at(cast_send->get_mailbox()) < 0) - return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting recv corresponding to this send - - if (if_no_match.first == -1) - if_no_match = std::make_pair(aid, value_of_state_); + + const CommRecvTransition* cast_recv = dynamic_cast(transition); + if (cast_recv != nullptr) { + if (mailbox_.count(cast_recv->get_mailbox()) > 0 and + mailbox_.at(cast_recv->get_mailbox()) > 0) { + aid_value--; // This means we have waiting recv corresponding to this recv + } else { + aid_value++; + + } + } + + const CommSendTransition* cast_send = dynamic_cast(transition); + if (cast_send != nullptr) { + if (mailbox_.count(cast_send->get_mailbox()) > 0 and + mailbox_.at(cast_send->get_mailbox()) < 0) { + aid_value--; // This means we have waiting recv corresponding to this send + }else { + aid_value++; + } + } + + if (aid_value < min_found.second) + min_found = std::make_pair(aid, aid_value); } - return if_no_match; + return min_found; } + void execute_next(aid_t aid, RemoteApp& app) override { const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get(); last_transition_ = transition->type_; - const CommRecvTransition* cast_recv = static_cast(transition); + const CommRecvTransition* cast_recv = dynamic_cast(transition); if (cast_recv != nullptr) last_mailbox_ = cast_recv->get_mailbox(); - const CommSendTransition* cast_send = static_cast(transition); + const CommSendTransition* cast_send = dynamic_cast(transition); if (cast_send != nullptr) last_mailbox_ = cast_send->get_mailbox(); } - void consider_best() override - { - for (auto& [aid, actor] : actors_to_run_) - if (actor.is_todo()) - return; - - for (auto& [aid, actor] : actors_to_run_) { - if (not actor.is_enabled() || actor.is_done()) - continue; - - const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); - - const CommRecvTransition* cast_recv = static_cast(transition); - if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and - mailbox_.at(cast_recv->get_mailbox()) > 0) { - actor.mark_todo(); - return; - } - - const CommSendTransition* cast_send = static_cast(transition); - if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and - mailbox_.at(cast_send->get_mailbox()) < 0) { - actor.mark_todo(); - return; - } - } - for (auto& [_, actor] : actors_to_run_) { - if (actor.is_enabled() and not actor.is_done()) { - actor.mark_todo(); - return; - } - } - } }; } // namespace simgrid::mc diff --git a/src/mc/api/strategy/MinMatchComm.hpp b/src/mc/api/strategy/MinMatchComm.hpp index 50fe6929ef..665c92f91a 100644 --- a/src/mc/api/strategy/MinMatchComm.hpp +++ b/src/mc/api/strategy/MinMatchComm.hpp @@ -19,7 +19,10 @@ class MinMatchComm : public Strategy { * Negative number means that much recv are waiting on that mailbox, while * a positiv number means that much send are waiting there. */ std::map mailbox_; - int value_of_state_ = 100000; // used to valuate the state. Corresponds to the number of in-fly communications + /** Used to valuate the state. Corresponds to a maximum minus the number of in-fly communications. + * Maximum should be set in order not to reach 0.*/ + int value_of_state_ = _sg_mc_max_depth; + // The two next values are used to save the operation we execute so the next strategy can update its field accordingly Transition::Type last_transition_; unsigned last_mailbox_ = 0; @@ -27,7 +30,7 @@ class MinMatchComm : public Strategy { public: void copy_from(const Strategy* strategy) override { - const MinMatchComm* cast_strategy = static_cast(strategy); + const MinMatchComm* cast_strategy = dynamic_cast(strategy); xbt_assert(cast_strategy != nullptr); for (auto& [id, val] : cast_strategy->mailbox_) mailbox_[id] = val; @@ -38,84 +41,59 @@ public: for (auto const& [_, val] : mailbox_) value_of_state_ -= std::abs(val); - if (value_of_state_ < 0) - value_of_state_ = 0; + xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0"); } MinMatchComm() = default; ~MinMatchComm() override = default; - std::pair next_transition() const override + std::pair best_transition(bool must_be_todo) const override { - std::pair if_no_match = std::make_pair(-1, 0); + std::pair min_found = std::make_pair(-1, value_of_state_+2); for (auto const& [aid, actor] : actors_to_run_) { - if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) - continue; + if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) + continue; + int aid_value = value_of_state_; const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); - const CommRecvTransition* cast_recv = static_cast(transition); - if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and - mailbox_.at(cast_recv->get_mailbox()) <= 0) - return std::make_pair(aid, value_of_state_ - 1); // This means we don't have waiting recv corresponding to this recv - - const CommSendTransition* cast_send = static_cast(transition); - if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and - mailbox_.at(cast_send->get_mailbox()) >= 0) - return std::make_pair(aid, value_of_state_ - 1); // This means we don't have waiting recv corresponding to this send - - if (if_no_match.first == -1) - if_no_match = std::make_pair(aid, value_of_state_); + const CommRecvTransition* cast_recv = dynamic_cast(transition); + if (cast_recv != nullptr) { + if ((mailbox_.count(cast_recv->get_mailbox()) > 0 and + mailbox_.at(cast_recv->get_mailbox()) <= 0) or mailbox_.count(cast_recv->get_mailbox()) == 0) + aid_value--; // This means we don't have waiting recv corresponding to this recv + else + aid_value++; + } + const CommSendTransition* cast_send = dynamic_cast(transition); + if (cast_send != nullptr) { + if ((mailbox_.count(cast_send->get_mailbox()) > 0 and + mailbox_.at(cast_send->get_mailbox()) >= 0) or mailbox_.count(cast_send->get_mailbox()) == 0) + aid_value--; + else + aid_value++; + } + + if (aid_value < min_found.second) + min_found = std::make_pair(aid, aid_value); } - return if_no_match; + return min_found; } + void execute_next(aid_t aid, RemoteApp& app) override { const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get(); last_transition_ = transition->type_; - const CommRecvTransition* cast_recv = static_cast(transition); + const CommRecvTransition* cast_recv = dynamic_cast(transition); if (cast_recv != nullptr) last_mailbox_ = cast_recv->get_mailbox(); - const CommSendTransition* cast_send = static_cast(transition); + const CommSendTransition* cast_send = dynamic_cast(transition); if (cast_send != nullptr) last_mailbox_ = cast_send->get_mailbox(); } - void consider_best() override - { - for (auto& [aid, actor] : actors_to_run_) - if (actor.is_todo()) - return; - - for (auto& [aid, actor] : actors_to_run_) { - if (not actor.is_enabled() || actor.is_done()) - continue; - - const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); - - const CommRecvTransition* cast_recv = static_cast(transition); - if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and - mailbox_.at(cast_recv->get_mailbox()) <= 0) { - actor.mark_todo(); - return; - } - - const CommSendTransition* cast_send = static_cast(transition); - if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and - mailbox_.at(cast_send->get_mailbox()) >= 0) { - actor.mark_todo(); - return; - } - } - for (auto& [_, actor] : actors_to_run_) { - if (actor.is_enabled() and not actor.is_done()) { - actor.mark_todo(); - return; - } - } - } }; } // namespace simgrid::mc diff --git a/src/mc/api/strategy/Strategy.hpp b/src/mc/api/strategy/Strategy.hpp index 8af77743ed..9bdebad0e4 100644 --- a/src/mc/api/strategy/Strategy.hpp +++ b/src/mc/api/strategy/Strategy.hpp @@ -8,6 +8,7 @@ #include "simgrid/forward.h" #include "src/mc/api/RemoteApp.hpp" +#include "src/mc/mc_config.hpp" #include "xbt/asserts.h" #include #include @@ -24,12 +25,21 @@ public: Strategy() = default; virtual ~Strategy() = default; - virtual std::pair next_transition() const = 0; + virtual std::pair best_transition(bool must_be_todo) const = 0; + + std::pair next_transition() { return best_transition(true); } virtual void execute_next(aid_t aid, RemoteApp& app) = 0; // Mark the first enabled and not yet done transition as todo // If there's already a transition marked as todo, does nothing - virtual void consider_best() = 0; + void consider_best() { + for (auto& [_, actor] :actors_to_run_) + if (actor.is_todo()) + return; + aid_t best_aid = best_transition(false).first; + if (best_aid != -1) + actors_to_run_.at(best_aid).mark_todo(); + } // Mark aid as todo. If it makes no sense, ie. if it is already done or not enabled, // raise an error diff --git a/src/mc/api/strategy/UniformStrategy.hpp b/src/mc/api/strategy/UniformStrategy.hpp index 72f1a37799..1dfcd07939 100644 --- a/src/mc/api/strategy/UniformStrategy.hpp +++ b/src/mc/api/strategy/UniformStrategy.hpp @@ -8,6 +8,8 @@ #include "src/mc/transition/Transition.hpp" +#define MAX_RAND 100000 + namespace simgrid::mc { /** Guiding strategy that valuate states randomly */ @@ -18,34 +20,34 @@ public: UniformStrategy() { for (long aid = 0; aid < 10; aid++) - valuation[aid] = rand() % 1000; + valuation[aid] = rand() % 10000; } void copy_from(const Strategy* strategy) override { for (auto& [aid, _] : actors_to_run_) - valuation[aid] = rand() % 1000; + valuation[aid] = rand() % 10000; } - std::pair next_transition() const override + std::pair best_transition(bool must_be_todo) const override { int possibilities = 0; // Consider only valid actors for (auto const& [aid, actor] : actors_to_run_) { - if (actor.is_todo() and (not actor.is_done()) and actor.is_enabled()) + if ((actor.is_todo() or not must_be_todo) and (not actor.is_done()) and actor.is_enabled()) possibilities++; } int chosen; if (possibilities == 0) - return std::make_pair(-1, 100000); + return std::make_pair(-1, 0); if (possibilities == 1) chosen = 0; else chosen = rand() % possibilities; for (auto const& [aid, actor] : actors_to_run_) { - if ((not actor.is_todo()) or actor.is_done() or (not actor.is_enabled())) + if (((not actor.is_todo()) and must_be_todo) or actor.is_done() or (not actor.is_enabled())) continue; if (chosen == 0) { return std::make_pair(aid, valuation.at(aid)); @@ -53,46 +55,12 @@ public: chosen--; } - return std::make_pair(-1, 100000); + return std::make_pair(-1, 0); } + void execute_next(aid_t aid, RemoteApp& app) override {} - - void consider_best() override - { - - int possibilities = 0; - // Consider only valid actors - // If some actor are already considered as todo, skip - for (auto const& [aid, actor] : actors_to_run_) { - if (valuation.count(aid) == 0) - for (auto& [aid, _] : actors_to_run_) - valuation[aid] = rand() % 1000; - if (actor.is_todo()) - return; - if (actor.is_enabled() and not actor.is_done()) - possibilities++; - } - - int chosen; - if (possibilities == 0) - return; - if (possibilities == 1) - chosen = 0; - else - chosen = rand() % possibilities; - - for (auto& [aid, actor] : actors_to_run_) { - if (not actor.is_enabled() or actor.is_done()) - continue; - if (chosen == 0) { - actor.mark_todo(); - return; - } - chosen--; - } - THROW_IMPOSSIBLE; // One actor should be marked as todo before - } + }; } // namespace simgrid::mc