include src/mc/api/RemoteApp.hpp
include src/mc/api/State.cpp
include src/mc/api/State.hpp
-include src/mc/api/guide/BasicGuide.hpp
-include src/mc/api/guide/GuidedState.hpp
-include src/mc/api/guide/WaitGuide.hpp
+include src/mc/api/strategy/BasicStrategy.hpp
+include src/mc/api/strategy/Strategy.hpp
+include src/mc/api/strategy/WaitStrategy.hpp
include src/mc/compare.cpp
include src/mc/datatypes.h
include src/mc/explo/CommunicationDeterminismChecker.cpp
> [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] 3: iSend(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] 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:'3;3;3;3;1;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 742 unique states visited; 145 backtracks (2228 transition replays, 1331 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;3;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 742 unique states visited; 145 backtracks (2218 transition replays, 1331 states visited overall)
! expect return 1
! timeout 20
-$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/guided-mc:nb_wait ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.}/model_checker_platform.xml --log=root.thresh:critical --log=mc.thresh:info
+$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:nb_wait ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.}/model_checker_platform.xml --log=root.thresh:critical --log=mc.thresh:info
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [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. 644 unique states visited; 157 backtracks (2487 transition replays, 1674 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 644 unique states visited; 157 backtracks (2475 transition replays, 1674 states visited overall)
\ No newline at end of file
> [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!
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 169 unique states visited; 28 backtracks (286 transition replays, 64 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 169 unique states visited; 28 backtracks (261 transition replays, 64 states visited overall)
\ No newline at end of file
> [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] 2: 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] 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:'2;3;1;1;2;1'
+> [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;2;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 21 unique states visited; 2 backtracks (24 transition replays, 1 states visited overall)
! expect return 1
! timeout 300
-$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/guided-mc:nb_wait -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical
+$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:nb_wait -- ${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/guided-mc' to 'nb_wait'
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'nb_wait'
> [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 ***
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
-> [Checker] There remains 0 actors, but none to interleave (depth 4).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 4).
> [Checker] Execution came to an end at 1;1;0 (state: 3, depth: 3)
> [Checker] Backtracking from 1;1;0
> [Checker] DFS exploration ended. 3 unique states visited; 0 backtracks (3 transition replays, 0 states visited overall)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] There remains 0 actors, but none to interleave (depth 6).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
> [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5)
> [Checker] Backtracking from 1;2;1;2;0
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
> [Checker] BARRIER_WAIT(barrier: 0) (state=8)
-> [Checker] There remains 0 actors, but none to interleave (depth 6).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
> [Checker] Execution came to an end at 2;1;1;2;0 (state: 9, depth: 5)
> [Checker] Backtracking from 2;1;1;2;0
> [Checker] DFS exploration ended. 9 unique states visited; 1 backtracks (10 transition replays, 0 states visited overall)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] BARRIER_WAIT(barrier: 0) (state=6)
-> [Checker] There remains 0 actors, but none to interleave (depth 8).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
> [Checker] Execution came to an end at 1;2;3;1;2;3;0 (state: 7, depth: 7)
> [Checker] Backtracking from 1;2;3;1;2;3;0
> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
-> [Checker] There remains 0 actors, but none to interleave (depth 8).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
> [Checker] Execution came to an end at 1;3;2;1;2;3;0 (state: 12, depth: 7)
> [Checker] Backtracking from 1;3;2;1;2;3;0
> [Checker] DFS exploration ended. 12 unique states visited; 1 backtracks (14 transition replays, 1 states visited overall)
\ No newline at end of file
> [Checker] Dependent Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
-> [Checker] There remains 0 actors, but none to interleave (depth 8).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
> [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7)
> [Checker] Backtracking from 1;1;1;2;2;2;0
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=10)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=12)
-> [Checker] There remains 0 actors, but none to interleave (depth 8).
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 13, depth: 7)
> [Checker] Backtracking from 2;1;2;2;1;1;0
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
-> [Checker] There remains 0 actors, but none to interleave (depth 8).
-> [Checker] Execution came to an end at 2;1;2;1;2;2;0 (state: 17, depth: 7)
-> [Checker] Backtracking from 2;1;2;1;2;2;0
-> [Checker] There remains 0 actors, but none to interleave (depth 8).
-> [Checker] Execution came to an end at 2;1;2;1;2;2;0 (state: 17, depth: 7)
-> [Checker] Backtracking from 2;1;2;1;2;2;0
-> [Checker] DFS exploration ended. 17 unique states visited; 2 backtracks (22 transition replays, 2 states visited overall)
+> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
+> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 17, depth: 7)
+> [Checker] Backtracking from 1;1;2;1;2;2;0
+> [Checker] Backtracking from 1;1;2;1;2;2;0
+> [Checker] DFS exploration ended. 17 unique states visited; 2 backtracks (21 transition replays, 2 states visited overall)
$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --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 '2'
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 130 unique states visited; 27 backtracks (334 transition replays, 151 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 130 unique states visited; 27 backtracks (308 transition replays, 151 states visited overall)
-$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/guided-mc:nb_wait -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical
+$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:nb_wait -- ${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/guided-mc' to 'nb_wait'
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'nb_wait'
> [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. 3492 unique states visited; 743 backtracks (13164 transition replays, 8263 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 3492 unique states visited; 743 backtracks (12498 transition replays, 8263 states visited overall)
\ No newline at end of file
> [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. 313 unique states visited; 89 backtracks (826 transition replays, 408 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 313 unique states visited; 89 backtracks (810 transition replays, 408 states visited overall)
> The thread 0 is terminating.
> The thread 1 is terminating.
> User's main is terminating.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (28 transition replays, 2 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (27 transition replays, 2 states visited overall)
\ No newline at end of file
> [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. 1100 unique states visited; 135 backtracks (3155 transition replays, 1702 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1100 unique states visited; 135 backtracks (2937 transition replays, 1702 states visited overall)
-$ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/guided-mc:nb_wait --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
+$ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:nb_wait --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/guided-mc' to 'nb_wait'
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'nb_wait'
> [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. 1101 unique states visited; 136 backtracks (3233 transition replays, 1713 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1101 unique states visited; 136 backtracks (2950 transition replays, 1713 states visited overall)
\ No newline at end of file
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/api/State.hpp"
-#include "src/mc/api/guide/BasicGuide.hpp"
-#include "src/mc/api/guide/WaitGuide.hpp"
+#include "src/mc/api/strategy/BasicStrategy.hpp"
+#include "src/mc/api/strategy/WaitStrategy.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
State::State(RemoteApp& remote_app) : num_(++expended_states_)
{
XBT_VERB("Creating a guide for the state");
- if (_sg_mc_guided == "none")
- guide_ = std::make_shared<BasicGuide>();
- if (_sg_mc_guided == "nb_wait")
- guide_ = std::make_shared<WaitGuide>();
+ if (_sg_mc_strategy == "none")
+ strategy_ = std::make_shared<BasicStrategy>();
+ if (_sg_mc_strategy == "nb_wait")
+ strategy_ = std::make_shared<WaitStrategy>();
recipe_ = std::list<Transition*>();
- remote_app.get_actors_status(guide_->actors_to_run_);
+ remote_app.get_actors_status(strategy_->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
: num_(++expended_states_), parent_state_(parent_state)
{
- if (_sg_mc_guided == "none")
- guide_ = std::make_shared<BasicGuide>();
- if (_sg_mc_guided == "nb_wait")
- guide_ = std::make_shared<WaitGuide>();
- *guide_ = *(parent_state->guide_);
+ if (_sg_mc_strategy == "none")
+ strategy_ = std::make_shared<BasicStrategy>();
+ if (_sg_mc_strategy == "nb_wait")
+ strategy_ = std::make_shared<WaitStrategy>();
+ *strategy_ = *(parent_state->strategy_);
recipe_ = std::list(parent_state_->get_recipe());
recipe_.push_back(parent_state_->get_transition());
- remote_app.get_actors_status(guide_->actors_to_run_);
+ remote_app.get_actors_status(strategy_->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
if (not parent_state_->get_transition()->depends(&transition)) {
sleep_set_.try_emplace(aid, transition);
- if (guide_->actors_to_run_.count(aid) != 0) {
+ if (strategy_->actors_to_run_.count(aid) != 0) {
XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
- guide_->actors_to_run_.at(aid).mark_done();
+ strategy_->actors_to_run_.at(aid).mark_done();
}
} else
XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
std::size_t State::count_todo() const
{
- return boost::range::count_if(this->guide_->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
+ return boost::range::count_if(this->strategy_->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_)
+ for (auto& [_, actor] : strategy_->actors_to_run_)
if (actor.is_todo())
count += actor.get_times_not_considered();
aid_t State::next_transition() const
{
- XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide_->actors_to_run_.size());
- for (auto const& [aid, actor] : guide_->actors_to_run_) {
+ XBT_DEBUG("Search for an actor to run. %zu actors to consider", strategy_->actors_to_run_.size());
+ for (auto const& [aid, actor] : strategy_->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()) {
if (not actor.is_todo())
std::pair<aid_t, double> State::next_transition_guided() const
{
- return guide_->next_transition();
+ return strategy_->next_transition();
}
// This should be done in GuidedState, or at least interact with it
void State::execute_next(aid_t next, RemoteApp& app)
{
// First, warn the guide, so it knows how to build a proper child state
- guide_->execute_next(next, app);
+ strategy_->execute_next(next, app);
// This actor is ready to be executed. Execution involves three phases:
// 1. Identify the appropriate ActorState to prepare for execution
// when simcall_handle will be called on it
- auto& actor_state = guide_->actors_to_run_.at(next);
+ auto& actor_state = strategy_->actors_to_run_.at(next);
const unsigned times_considered = actor_state.do_consider();
const auto* expected_executed_transition = actor_state.get_transition(times_considered);
xbt_assert(expected_executed_transition != nullptr,
#include "src/mc/api/ActorState.hpp"
#include "src/mc/api/RemoteApp.hpp"
-#include "src/mc/api/guide/GuidedState.hpp"
+#include "src/mc/api/strategy/Strategy.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "src/mc/transition/Transition.hpp"
and for guided model-checking */
std::shared_ptr<State> parent_state_ = nullptr;
- std::shared_ptr<GuidedState> guide_;
+ std::shared_ptr<Strategy> strategy_;
/* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
* set. With this information, it is check whether it should be removed from it or not when exploring a new
* + consider_one mark aid actor (and assert it is possible)
* + consider_best ensure one actor is marked by eventually marking the best regarding its guiding methode
* + conside_all mark all enabled actor that are not done yet */
- void consider_one(aid_t aid) { guide_->consider_one(aid); }
- void consider_best() { guide_->consider_best(); }
- unsigned long consider_all() { return guide_->consider_all(); }
+ void consider_one(aid_t aid) { strategy_->consider_one(aid); }
+ void consider_best() { strategy_->consider_best(); }
+ unsigned long consider_all() { return strategy_->consider_all(); }
- bool is_actor_done(aid_t actor) const { return guide_->actors_to_run_.at(actor).is_done(); }
+ bool is_actor_done(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
std::shared_ptr<State> get_parent_state() { return parent_state_; }
std::list<Transition*> get_recipe() const { return recipe_; }
- std::map<aid_t, ActorState> const& get_actors_list() const { return guide_->actors_to_run_; }
+ std::map<aid_t, ActorState> const& get_actors_list() const { return strategy_->actors_to_run_; }
- unsigned long get_actor_count() const { return guide_->actors_to_run_.size(); }
- bool is_actor_enabled(aid_t actor) { return guide_->actors_to_run_.at(actor).is_enabled(); }
+ unsigned long get_actor_count() const { return strategy_->actors_to_run_.size(); }
+ bool is_actor_enabled(aid_t actor) { return strategy_->actors_to_run_.at(actor).is_enabled(); }
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
/* 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. */
-#ifndef SIMGRID_MC_BASICGUIDE_HPP
-#define SIMGRID_MC_BASICGUIDE_HPP
+#ifndef SIMGRID_MC_BASICSTRATEGY_HPP
+#define SIMGRID_MC_BASICSTRATEGY_HPP
namespace simgrid::mc {
/** Basic MC guiding class which corresponds to no guide at all (random choice) */
-class BasicGuide : public GuidedState {
+class BasicStrategy : public Strategy {
public:
- void operator=(const GuidedState&) { return; }
+ void operator=(const BasicStrategy&) { return; }
std::pair<aid_t, double> next_transition() const override
{
#include "xbt/asserts.h"
-#ifndef SIMGRID_MC_GUIDEDSTATE_HPP
-#define SIMGRID_MC_GUIDEDSTATE_HPP
+#ifndef SIMGRID_MC_STRATEGY_HPP
+#define SIMGRID_MC_STRATEGY_HPP
namespace simgrid::mc {
-class GuidedState {
+class Strategy {
protected:
/** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this
* state */
std::map<aid_t, ActorState> actors_to_run_;
public:
- virtual ~GuidedState() = default;
+ virtual ~Strategy() = default;
virtual std::pair<aid_t, double> next_transition() const = 0;
virtual void execute_next(aid_t aid, RemoteApp& app) = 0;
virtual void consider_best() = 0;
/* 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. */
-#ifndef SIMGRID_MC_WAITGUIDE_HPP
-#define SIMGRID_MC_WAITGUIDE_HPP
+#ifndef SIMGRID_MC_WAITSTRATEGY_HPP
+#define SIMGRID_MC_WAITSTRATEGY_HPP
#include "src/mc/transition/Transition.hpp"
/** Wait MC guiding class that aims at minimizing the number of in-fly communication.
* When possible, it will try to take the wait transition. */
-class WaitGuide : public GuidedState {
+class WaitStrategy : public Strategy {
double taken_wait_ = 0;
bool taking_wait_ = false;
public:
- void operator=(const WaitGuide& guide) { taken_wait_ = guide.taken_wait_; }
+ void operator=(const WaitStrategy& guide) { taken_wait_ = guide.taken_wait_; }
bool is_transition_wait(Transition::Type type) const
{
}
RecordTrace DFSExplorer::get_record_trace() // override
-{
- return get_record_trace_of_stack(stack_);
-}
-
-/* Usefull to show debug information */
-RecordTrace DFSExplorer::get_record_trace_of_stack(stack_t stack)
{
RecordTrace res;
- for (auto const& state : stack)
- res.push_back(state->get_transition());
+ for (auto const& transition : stack_.back()->get_recipe())
+ res.push_back(transition);
+ res.push_back(stack_.back()->get_transition());
return res;
}
std::vector<std::string> DFSExplorer::get_textual_trace() // override
{
std::vector<std::string> trace;
- for (auto const& state : stack_) {
- const auto* t = state->get_transition();
- trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
+ for (auto const& transition : stack_.back()->get_recipe()) {
+ trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
}
+ trace.push_back(xbt::string_printf("%ld: %s", stack_.back()->get_transition()->aid_,
+ stack_.back()->get_transition()->to_string().c_str()));
return trace;
}
auto [next, _] = state->next_transition_guided();
if (next < 0) { // If there is no more transition in the current state, backtrack.
- XBT_VERB("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
+ XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
if (state->get_actor_count() == 0) {
XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
"transition as todo",
issuer_id);
- if (prev_state->consider_all() >
- 0) // If we ended up marking at least a transition, explore it at some point
+ // If we ended up marking at least a transition, explore it at some point
+ if (prev_state->consider_all() > 0)
opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
}
break;
// if the smallest distance corresponded to no enable actor, remove this and let the
// exploration ask again for a backtrack
if (backtracking_point->next_transition_guided().first == -1) {
- XBT_DEBUG("Best backtracking candidates has already been explored. We may backtrack again");
+ XBT_DEBUG("Best backtracking candidates has already been explored. Let's backtrack again");
+ this->backtrack();
return;
}
"model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", false,
[](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }};
-simgrid::config::Flag<std::string> _sg_mc_guided{
- "model-check/guided-mc", "Specify the the kind of heuristic to use for guided model-checking", "none",
+simgrid::config::Flag<std::string> _sg_mc_strategy{
+ "model-check/strategy", "Specify the the kind of heuristic to use for guided model-checking", "none",
[](std::string_view value) {
if (value != "none" && value != "nb_wait")
xbt_die("configuration option 'model-check/guided-mc' can only take 'none' or 'nb_wait' as a value");
}};
-
simgrid::config::Flag<int> _sg_mc_checkpoint{
"model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
"(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "
extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;
extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_termination;
extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sleep_set;
-extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_guided;
-
-
+extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_strategy;
#endif
> [ 0.000000] (0:maestro@) Behavior: printf
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (1:app@Fafard) Error reached
-> [ 0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 35 backtracks (109 transition replays, 30 states visited overall)
+> [ 0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 35 backtracks (108 transition replays, 30 states visited overall)
! expect return 6
# because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
> If this is too much, consider sharing allocations for computation buffers.
> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
->
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
-> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
-> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
-> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
-> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
-> If this is too much, consider sharing allocations for computation buffers.
-> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
->
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
-> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
-> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
-> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
-> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
-> If this is too much, consider sharing allocations for computation buffers.
-> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
->
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
-> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
-> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
-> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
-> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
-> If this is too much, consider sharing allocations for computation buffers.
-> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
->
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
-> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
-> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
-> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
-> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
-> If this is too much, consider sharing allocations for computation buffers.
-> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
->
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
-> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
-> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
-> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
-> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
-> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
-> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
-> If this is too much, consider sharing allocations for computation buffers.
-> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
->
+>
> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
> If this is too much, consider sharing allocations for computation buffers.
> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
>
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 623 unique states visited; 173 backtracks (3980 transition replays, 3108 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 623 unique states visited; 173 backtracks (3904 transition replays, 3108 states visited overall)
src/mc/transition/TransitionSynchro.cpp
src/mc/transition/TransitionSynchro.hpp
- src/mc/api/guide/BasicGuide.hpp
- src/mc/api/guide/GuidedState.hpp
- src/mc/api/guide/WaitGuide.hpp
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/mc_private.hpp
src/mc/mc_record.cpp
- src/mc/api/guide/BasicGuide.hpp
- src/mc/api/guide/GuidedState.hpp
- src/mc/api/guide/WaitGuide.hpp
+ src/mc/api/strategy/BasicStrategy.hpp
+ src/mc/api/strategy/Strategy.hpp
+ src/mc/api/strategy/WaitStrategy.hpp
src/xbt/mmalloc/mm_interface.c
)
