From 585a65d8e2c5bed10f20cd84c5c1cb59ef6adc8a Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 16 Apr 2023 00:38:08 +0200 Subject: [PATCH] Make sure that we never have a 0 transition at the end of the stack --- .../s4u-mc-synchro-barrier.tesh | 20 +++++++++---------- .../synchro-mutex/s4u-mc-synchro-mutex.tesh | 12 +++++------ examples/smpi/mc/sendsend.tesh | 3 +-- .../pthread-mc-mutex-simpledeadlock.tesh | 3 +-- src/mc/api/RemoteApp.cpp | 4 ++-- src/mc/api/State.hpp | 14 +++---------- src/mc/explo/DFSExplorer.cpp | 4 ++-- src/mc/explo/LivenessChecker.cpp | 3 ++- src/mc/mc_record.cpp | 2 ++ 9 files changed, 29 insertions(+), 36 deletions(-) diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh index 15c10ab3b0..2002f4bda1 100644 --- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh +++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh @@ -5,8 +5,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [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] 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] Execution came to an end at 1;1 (state: 3, depth: 3) +> [Checker] Backtracking from 1;1 > [Checker] DFS exploration ended. 3 unique states visited; 0 backtracks (3 transition replays, 0 states visited overall) $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n" @@ -28,8 +28,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) > [Checker] BARRIER_WAIT(barrier: 0) (state=4) > [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] Execution came to an end at 1;2;1;2 (state: 5, depth: 5) +> [Checker] Backtracking from 1;2;1;2 > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) > [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 6, 0 interleaves) > [Checker] INDEPENDENT Transitions: @@ -47,8 +47,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6) > [Checker] BARRIER_WAIT(barrier: 0) (state=8) > [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] Execution came to an end at 2;1;1;2 (state: 9, depth: 5) +> [Checker] Backtracking from 2;1;1;2 > [Checker] DFS exploration ended. 9 unique states visited; 1 backtracks (10 transition replays, 0 states visited overall) $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n" @@ -87,8 +87,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] BARRIER_WAIT(barrier: 0) (state=6) > [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] Execution came to an end at 1;2;3;1;2;3 (state: 7, depth: 7) +> [Checker] Backtracking from 1;2;3;1;2;3 > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] INDEPENDENT Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) @@ -122,6 +122,6 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) > [Checker] BARRIER_WAIT(barrier: 0) (state=11) > [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] Execution came to an end at 1;3;2;1;2;3 (state: 12, depth: 7) +> [Checker] Backtracking from 1;3;2;1;2;3 > [Checker] DFS exploration ended. 12 unique states visited; 1 backtracks (14 transition replays, 1 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 60d4c05992..3ef36cc3a2 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -27,8 +27,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) > [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6) > [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] Execution came to an end at 1;1;1;2;2;2 (state: 7, depth: 7) +> [Checker] Backtracking from 1;1;1;2;2;2 > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves) > [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 8, 0 interleaves) > [Checker] Dependent Transitions: @@ -51,8 +51,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=10) > [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=12) > [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] Execution came to an end at 2;1;2;2;1;1 (state: 13, depth: 7) +> [Checker] Backtracking from 2;1;2;2;1;1 > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2) @@ -73,8 +73,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14) > [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16) > [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] Execution came to an end at 1;1;2;1;2;2 (state: 17, depth: 7) +> [Checker] Backtracking from 1;1;2;1;2;2 > [Checker] DFS exploration ended. 17 unique states visited; 2 backtracks (21 transition replays, 2 states visited overall) $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical diff --git a/examples/smpi/mc/sendsend.tesh b/examples/smpi/mc/sendsend.tesh index a8b282b820..2b6590a2ac 100644 --- a/examples/smpi/mc/sendsend.tesh +++ b/examples/smpi/mc/sendsend.tesh @@ -53,7 +53,6 @@ $ $VALGRIND_NO_LEAK_CHECK ../../../smpi_script/bin/smpirun -quiet -wrapper "${bi > [0.000000] [mc_global/INFO] Counter-example execution trace: > [0.000000] [mc_global/INFO] 1: iSend(mbox=2) > [0.000000] [mc_global/INFO] 2: iSend(mbox=0) -> [0.000000] [mc_global/INFO] 0: -> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2;0' +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2' > [0.000000] [mc_dfs/INFO] DFS exploration ended. 3 unique states visited; 0 backtracks (3 transition replays, 0 states visited overall) > Execution failed with code 3. diff --git a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh index 5952dae7ca..666325f916 100644 --- a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh +++ b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh @@ -27,6 +27,5 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) > [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner: 3) > [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) -> [0.000000] [mc_global/INFO] 0: -> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3;0' +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3' > [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 1 backtracks (22 transition replays, 2 states visited overall) \ No newline at end of file diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 5511a27f56..555bef2f56 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -45,12 +45,12 @@ RemoteApp::RemoteApp(const std::vector& args, bool need_memory_introspect checker_side_ = std::make_unique(app_args_, need_memory_introspection); initial_snapshot_ = std::make_shared(0, page_store_, *checker_side_->get_remote_memory()); #else - xbt_die("SimGrid was compiled without MC support."); + xbt_die("SimGrid MC was compiled without memory introspection support."); #endif } else { master_socket_ = socket(AF_UNIX, #ifdef __APPLE__ - SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster*/ + SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster */ #else SOCK_SEQPACKET, #endif diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index e7d15482fc..7709cc1e81 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -22,19 +22,11 @@ class XBT_PRIVATE State : public xbt::Extendable { static long expended_states_; /* Count total amount of states, for stats */ /** - * @brief An empty transition that leads to this state by default - */ - const std::unique_ptr default_transition_ = std::make_unique(); - - /** - * @brief The outgoing transition: what was the last transition that - * we took to leave this state? + * @brief The outgoing transition: what was the last transition that we took to leave this state? * - * The owner of the transition is the `ActorState` instance which exists in this state, - * or a reference to the internal default transition `Transition()` if no transition has been - * set + * The owner of the transition is the `ActorState` instance which exists in this state. */ - Transition* transition_ = default_transition_.get(); + Transition* transition_ = nullptr; /** @brief A list of transition to be replayed in order to get in this state. */ std::list recipe_; diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 5903739f9e..bd8dbdc9a0 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -81,8 +81,8 @@ std::vector DFSExplorer::get_textual_trace() // override 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())); + if (auto* trans = stack_.back()->get_transition(); trans != nullptr) + trace.push_back(xbt::string_printf("%ld: %s", trans->aid_, trans->to_string().c_str())); return trace; } diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 071c1e4cae..1cd43885b7 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -289,7 +289,8 @@ std::vector LivenessChecker::get_textual_trace() // override { std::vector trace; for (std::shared_ptr const& pair : exploration_stack_) - trace.push_back(pair->app_state_->get_transition()->to_string()); + if (pair->app_state_->get_transition() != nullptr) + trace.push_back(pair->app_state_->get_transition()->to_string()); return trace; } diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index a16898e144..f63910724a 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -98,6 +98,8 @@ std::string simgrid::mc::RecordTrace::to_string() const { std::ostringstream stream; for (auto i = transitions_.begin(); i != transitions_.end(); ++i) { + if (*i == nullptr) + continue; if (i != transitions_.begin()) stream << ';'; stream << (*i)->aid_; -- 2.20.1