From 039f83ac2878e7ff0839a216474c8e493c98c068 Mon Sep 17 00:00:00 2001 From: mlaurent Date: Mon, 27 Mar 2023 20:19:28 +0200 Subject: [PATCH] Now handle random transition and multiple times transitions --- examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh | 2 +- .../s4u-mc-electric-fence.tesh | 11 +++- .../synchro-mutex/s4u-mc-synchro-mutex.tesh | 4 +- .../s4u-mc-synchro-semaphore.tesh | 2 +- examples/smpi/mc/only_send_deterministic.tesh | 2 +- .../sthread/pthread-mc-producer-consumer.tesh | 2 +- src/mc/api/ActorState.hpp | 1 + src/mc/api/State.cpp | 10 ++++ src/mc/api/State.hpp | 1 + src/mc/explo/DFSExplorer.cpp | 58 +++++++++++++------ src/mc/explo/DFSExplorer.hpp | 3 +- teshsuite/mc/random-bug/random-bug.tesh | 6 +- 12 files changed, 74 insertions(+), 28 deletions(-) diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh index a2919228ed..9523bfafda 100644 --- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh +++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh @@ -16,4 +16,4 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true ${bindir > [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;1;3;3;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 307 unique states visited; 41 backtracks (623 transition replays, 275 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 263 unique states visited; 37 backtracks (559 transition replays, 259 states visited overall) diff --git a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh index 329064b013..cdc99f12dd 100644 --- a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh +++ b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh @@ -41,6 +41,9 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${plat > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! +> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! +> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK +> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! @@ -68,16 +71,22 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${plat > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! +> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! +> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK +> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! +> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! +> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK +> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 154 unique states visited; 26 backtracks (234 transition replays, 55 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 169 unique states visited; 29 backtracks (261 transition replays, 64 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 5ae1bf5e33..3c7cd0439c 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -81,10 +81,10 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bin > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true' > [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. 127 unique states visited; 25 backtracks (286 transition replays, 135 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 128 unique states visited; 26 backtracks (296 transition replays, 143 states visited overall) $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${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 'actors' to '3' > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 4489 unique states visited; 989 backtracks (16546 transition replays, 11069 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 4645 unique states visited; 1082 backtracks (18004 transition replays, 12278 states visited overall) \ No newline at end of file diff --git a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh index c4449b18f1..54e641e529 100644 --- a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh +++ b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh @@ -3,4 +3,4 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --log=mc_dfs.thres:info --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-semaphore --log=sem_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n" > [Checker] Configuration change: Set 'model-check/sleep-set' to 'true' > [Checker] Start a DFS exploration. Reduction is: dpor. -> [Checker] DFS exploration ended. 30 unique states visited; 6 backtracks (67 transition replays, 32 states visited overall) +> [Checker] DFS exploration ended. 33 unique states visited; 9 backtracks (125 transition replays, 84 states visited overall) diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index 5bb5de2daf..447496d1ce 100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@ -10,4 +10,4 @@ $ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-m > [0.000000] [mc_comm_determinism/INFO] The recv communications pattern of the actor 0 is different! Different source for communication #1 > [0.000000] [mc_comm_determinism/INFO] Send-deterministic : Yes > [0.000000] [mc_comm_determinism/INFO] Recv-deterministic : No -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 110 unique states visited; 21 backtracks (189 transition replays, 59 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 242 unique states visited; 68 backtracks (612 transition replays, 303 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 22a7bdf579..0766ba31f7 100644 --- a/examples/sthread/pthread-mc-producer-consumer.tesh +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -5,4 +5,4 @@ $ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true' > [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. 317 unique states visited; 32 backtracks (683 transition replays, 335 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 719 unique states visited; 83 backtracks (1854 transition replays, 1053 states visited overall) diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index d407e5b893..a7fee78b51 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -98,6 +98,7 @@ public: return times_considered_++; } unsigned int get_times_considered() const { return times_considered_; } + unsigned int get_times_not_considered() const { return max_consider_ - times_considered_; } aid_t get_aid() const { return aid_; } /* returns whether the actor is marked as enabled in the application side */ diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 655ef6ec67..e2a6ac4534 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -84,6 +84,16 @@ std::size_t State::count_todo() const return boost::range::count_if(this->guide_->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); } +std::size_t State::count_todo_multiples() const +{ + size_t count = 0; + for (auto& [_, actor] : guide_->actors_to_run_) + if (actor.is_todo()) + count += actor.get_times_not_considered(); + + return count; +} + Transition* State::get_transition() const { return transition_; diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 9288788cef..5a9266368c 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -67,6 +67,7 @@ public: long get_num() const { return num_; } std::size_t count_todo() const; + std::size_t count_todo_multiples() const; /* Marking as TODO some actor in this state: * + consider_one mark aid actor (and assert it is possible) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 55395e1e5d..9e4718466a 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -69,6 +69,14 @@ RecordTrace DFSExplorer::get_record_trace() // override return res; } +RecordTrace get_record_trace_of_stack(stack_t stack) +{ + RecordTrace res; + for (auto const& state : stack) + res.push_back(state->get_transition()); + return res; +} + std::vector DFSExplorer::get_textual_trace() // override { std::vector trace; @@ -89,6 +97,14 @@ void DFSExplorer::log_state() // override Exploration::log_state(); } +void DFSExplorer::add_to_opened_states(stack_t stack) +{ + stack_t tmp_stack; + for (auto& state : stack) + tmp_stack.push_back(std::make_shared(State(*state))); + opened_states_.emplace_back(tmp_stack); +} + void DFSExplorer::run() { on_exploration_start_signal(get_remote_app()); @@ -145,13 +161,15 @@ void DFSExplorer::run() this->backtrack(); continue; } - if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) { XBT_VERB("Sleep set actually containing:"); for (auto& [aid, transition] : state->get_sleep_set()) XBT_VERB(" <%ld,%s>", aid, transition.to_string().c_str()); } + // if (stack_.back()->count_todo_multiples() <= 1) + // add_to_opened_states(stack_); + /* Actually answer the request: let's execute the selected request (MCed does one step) */ state->execute_next(next, get_remote_app()); on_transition_execute_signal(state->get_transition(), get_remote_app()); @@ -162,8 +180,8 @@ void DFSExplorer::run() state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo()); /* Create the new expanded state (copy the state of MCed into our MCer data) */ - std::unique_ptr next_state; - next_state = std::make_unique(get_remote_app(), state); + std::shared_ptr next_state; + next_state = std::make_shared(get_remote_app(), state); on_state_creation_signal(next_state.get(), get_remote_app()); /* Sleep set procedure: @@ -180,9 +198,7 @@ void DFSExplorer::run() * If the process is not enabled at this point, then add every enabled process to the interleave */ if (reduction_mode_ == ReductionMode::dpor) { aid_t issuer_id = state->get_transition()->aid_; - stack_t tmp_stack; - for (auto& state : stack_) - tmp_stack.push_back(std::make_shared(State(*state))); + stack_t tmp_stack = std::list(stack_); while (not tmp_stack.empty()) { State* prev_state = tmp_stack.back().get(); if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) { @@ -198,7 +214,7 @@ void DFSExplorer::run() if (prev_state->is_actor_enabled(issuer_id)) { if (not prev_state->is_actor_done(issuer_id)) { prev_state->consider_one(issuer_id); - opened_states.emplace_back(tmp_stack); + add_to_opened_states(tmp_stack); } else XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id); } else { @@ -206,7 +222,7 @@ void DFSExplorer::run() "transition as todo", issuer_id); prev_state->consider_all(); - opened_states.emplace_back(tmp_stack); + add_to_opened_states(tmp_stack); } break; } else { @@ -234,8 +250,9 @@ void DFSExplorer::run() stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required else { stack_.back()->consider_all(); - opened_states.emplace_back(stack_); } + if (stack_.back()->count_todo_multiples() > 1) + add_to_opened_states(stack_); dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(), state->get_transition()->dot_string().c_str()); } else @@ -251,11 +268,14 @@ void DFSExplorer::backtrack() { backtrack_count_++; XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str()); + XBT_DEBUG("%ld alternatives are yet to be explored:", opened_states_.size()); + for (auto& stack : opened_states_) + XBT_DEBUG("--> %s", get_record_trace_of_stack(stack).to_string().c_str()); on_backtracking_signal(get_remote_app()); get_remote_app().check_deadlock(); // if no backtracking point, then set the stack_ to empty so we can end the exploration - if (opened_states.size() == 0) { + if (opened_states_.size() == 0) { stack_ = std::list>(); return; } @@ -268,15 +288,18 @@ void DFSExplorer::backtrack() stack_t backtrack; double min_dist = std::numeric_limits::infinity(); aid_t min_aid = -1; - for (auto& stack : opened_states) { - auto [aid, dist] = stack.back()->next_transition_guided(); - if (aid == -1) + for (auto iter = opened_states_.begin(); iter != opened_states_.end();) { + auto [aid, dist] = (*iter).back()->next_transition_guided(); + if (aid == -1) { // happens if no actors are todo anymore in this transition + iter = opened_states_.erase(iter); continue; + } if (dist < min_dist) { min_dist = dist; min_aid = aid; - backtrack = stack; + backtrack = (*iter); } + iter++; } if (min_aid == -1) { @@ -284,8 +307,8 @@ void DFSExplorer::backtrack() return; } - if (backtrack.back()->count_todo() <= 1) - opened_states.pop_back(); + if (backtrack.back()->count_todo_multiples() <= 1) + opened_states_.remove(backtrack); /* If asked to rollback on a state that has a snapshot, restore it */ State* last_state = backtrack.back().get(); @@ -341,8 +364,9 @@ DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor, bool ne stack_.back()->consider_best(); else { stack_.back()->consider_all(); - opened_states.emplace_back(stack_); } + if (stack_.back()->count_todo_multiples() > 1) + add_to_opened_states(stack_); } Exploration* create_dfs_exploration(const std::vector& args, bool with_dpor) diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index c176bafcb4..728981c03d 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -95,7 +95,8 @@ private: /** Opened states are states that still contains todo actors. * When backtracking, we pick a state from it*/ - std::vector opened_states; + std::list opened_states_; + void add_to_opened_states(stack_t stack); }; } // namespace simgrid::mc diff --git a/teshsuite/mc/random-bug/random-bug.tesh b/teshsuite/mc/random-bug/random-bug.tesh index 952ba8ebe3..ca6e6157d9 100644 --- a/teshsuite/mc/random-bug/random-bug.tesh +++ b/teshsuite/mc/random-bug/random-bug.tesh @@ -10,7 +10,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir > [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3) > [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4) > [ 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/4' -> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 31 unique states visited; 24 backtracks (74 transition replays, 19 states visited overall) ! expect return 6 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6 @@ -25,7 +25,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir} > [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3) > [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4) > [ 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/4' -> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 31 unique states visited; 24 backtracks (74 transition replays, 19 states visited overall) > [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning @@ -48,5 +48,5 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/ > [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3) > [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4) > [ 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/4' -> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 31 unique states visited; 24 backtracks (74 transition replays, 19 states visited overall) > [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc -- 2.20.1