From add8b5f44959343a150508770c76912d4886861c Mon Sep 17 00:00:00 2001 From: mlaurent Date: Sat, 18 Mar 2023 15:58:43 +0100 Subject: [PATCH] Move DPOR and sleep set algorithm from backtrack to run procedure --- .../s4u-mc-synchro-barrier.tesh | 106 +++++++++--------- .../synchro-mutex/s4u-mc-synchro-mutex.tesh | 74 ++++++------ src/mc/explo/DFSExplorer.cpp | 96 ++++++++-------- 3 files changed, 140 insertions(+), 136 deletions(-) diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh index 51eeae219a..fa4fc258fa 100644 --- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh +++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh @@ -12,52 +12,68 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [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 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) +> [Checker] Dependent Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_WAIT(barrier: 0) (state=3) > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves) -> [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] INDEPENDENT Transitions: > [Checker] BARRIER_WAIT(barrier: 0) (state=3) > [Checker] BARRIER_WAIT(barrier: 0) (state=4) > [Checker] Dependent Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) > [Checker] BARRIER_WAIT(barrier: 0) (state=4) -> [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_WAIT(barrier: 0) (state=3) -> [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [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] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 6, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6) > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 7, 0 interleaves) +> [Checker] Dependent Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_WAIT(barrier: 0) (state=7) > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 8, 0 interleaves) -> [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] INDEPENDENT Transitions: > [Checker] BARRIER_WAIT(barrier: 0) (state=7) > [Checker] BARRIER_WAIT(barrier: 0) (state=8) > [Checker] Dependent Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6) > [Checker] BARRIER_WAIT(barrier: 0) (state=8) -> [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_WAIT(barrier: 0) (state=7) -> [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=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; 2 backtracks (10 transition replays, 0 states visited overall) $ ${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" > [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 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] INDEPENDENT Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves) +> [Checker] Dependent Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] BARRIER_WAIT(barrier: 0) (state=4) > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] BARRIER_WAIT(barrier: 0) (state=4) +> [Checker] BARRIER_WAIT(barrier: 0) (state=5) +> [Checker] Dependent Transitions: +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] BARRIER_WAIT(barrier: 0) (state=5) > [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves) -> [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] INDEPENDENT Transitions: > [Checker] BARRIER_WAIT(barrier: 0) (state=5) > [Checker] BARRIER_WAIT(barrier: 0) (state=6) @@ -67,56 +83,40 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] Dependent Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] BARRIER_WAIT(barrier: 0) (state=6) -> [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) -> [Checker] BARRIER_WAIT(barrier: 0) (state=5) -> [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) -> [Checker] BARRIER_WAIT(barrier: 0) (state=5) -> [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) -> [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) -> [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [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] INDEPENDENT Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 8, 0 interleaves) -> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves) -> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves) -> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves) -> [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] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=10) -> [Checker] BARRIER_WAIT(barrier: 0) (state=11) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=9) -> [Checker] BARRIER_WAIT(barrier: 0) (state=11) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) +> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves) > [Checker] Dependent Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) -> [Checker] BARRIER_WAIT(barrier: 0) (state=11) +> [Checker] BARRIER_WAIT(barrier: 0) (state=9) +> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves) > [Checker] INDEPENDENT Transitions: > [Checker] BARRIER_WAIT(barrier: 0) (state=9) > [Checker] BARRIER_WAIT(barrier: 0) (state=10) > [Checker] Dependent Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] BARRIER_WAIT(barrier: 0) (state=10) -> [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) -> [Checker] BARRIER_WAIT(barrier: 0) (state=9) +> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) +> [Checker] BARRIER_WAIT(barrier: 0) (state=10) +> [Checker] BARRIER_WAIT(barrier: 0) (state=11) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_WAIT(barrier: 0) (state=9) +> [Checker] BARRIER_WAIT(barrier: 0) (state=11) +> [Checker] Dependent Transitions: > [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8) -> [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_WAIT(barrier: 0) (state=11) +> [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; 2 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 ea81b940a2..6dda41c6dc 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -9,16 +9,6 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 3, state: 3, 0 interleaves) > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves) -> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves) -> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves) -> [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] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6) -> [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) @@ -28,50 +18,60 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] Dependent Transitions: > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) -> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves) -> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves) -> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves) -> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves) -> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 11, depth: 7) -> [Checker] Backtracking from 1;1;2;1;2;2;0 +> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) +> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5) +> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9) -> [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6) +> [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: 1) (stack depth: 3, state: 3, 0 interleaves) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2) > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) > [Checker] Dependent Transitions: > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) +> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8) +> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves) +> [Checker] Dependent Transitions: +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8) +> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9) +> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves) +> [Checker] Dependent Transitions: +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10) +> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 11, depth: 7) +> [Checker] Backtracking from 1;1;2;1;2;2;0 > [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: 12, 0 interleaves) +> [Checker] Dependent Transitions: +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12) > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 13, 0 interleaves) +> [Checker] INDEPENDENT Transitions: +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12) +> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=13) > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 14, 0 interleaves) -> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves) -> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves) -> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 17, depth: 7) -> [Checker] Backtracking from 2;1;2;2;1;1;0 -> [Checker] Dependent Transitions: +> [Checker] INDEPENDENT Transitions: +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12) > [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16) +> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves) > [Checker] Dependent Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14) > [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=15) -> [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14) -> [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=13) +> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16) +> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 17, depth: 7) +> [Checker] Backtracking from 2;1;2;2;1;1;0 > [Checker] DFS exploration ended. 17 unique states visited; 3 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 diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 64972274f5..edf1316724 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -164,9 +164,53 @@ void DFSExplorer::run() std::unique_ptr next_state; next_state = std::make_unique(get_remote_app(), state); - on_state_creation_signal(next_state.get(), get_remote_app()); + /* Sleep set procedure: + * adding the taken transition to the sleep set of the original state. + * Since the parent sleep set is used to compute the child sleep set, this need to be + * done after next_state creation */ + XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", + state->get_transition()->to_string().c_str(), state->get_transition()->aid_); + state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState + + /* DPOR persistent set procedure: + * for each new transition considered, check if it depends on any other previous transition executed before it + * on another process. If there exists one, find the more recent, and add its process to the interleave set. + * 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_; + for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { + State* prev_state = i->get(); + if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) { + XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(), + prev_state->get_transition()->to_string().c_str(), issuer_id); + continue; + } else if (prev_state->get_transition()->depends(state->get_transition())) { + XBT_VERB("Dependent Transitions:"); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); + + if (prev_state->is_actor_enabled(issuer_id)) { + if (not prev_state->is_actor_done(issuer_id)) + prev_state->consider_one(issuer_id); + else + XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id); + } else { + XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled " + "transition as todo", + issuer_id); + prev_state->consider_all(); + } + break; + } else { + XBT_VERB("INDEPENDENT Transitions:"); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); + } + } + } + if (_sg_mc_termination) this->check_non_termination(next_state.get()); @@ -208,52 +252,13 @@ void DFSExplorer::backtrack() stack_.pop_back(); /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that - * have it empty in the way. For each deleted state, check if the request that has generated it (from its - * predecessor state) depends on any other previous request executed before it on another process. If there exists - * one, find the more recent, and add its process to the interleave set. If the process is not enabled at this point, - * then add every enabled process to the interleave */ + * have it empty in the way. */ bool found_backtracking_point = false; while (not stack_.empty() && not found_backtracking_point) { std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); - XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", - state->get_transition()->to_string().c_str(), state->get_transition()->aid_); - state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState - - if (reduction_mode_ == ReductionMode::dpor) { - aid_t issuer_id = state->get_transition()->aid_; - for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { - State* prev_state = i->get(); - if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) { - XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(), - prev_state->get_transition()->to_string().c_str(), issuer_id); - continue; - } else if (prev_state->get_transition()->depends(state->get_transition())) { - XBT_VERB("Dependent Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num()); - XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); - - if (prev_state->is_actor_enabled(issuer_id)) { - if (not prev_state->is_actor_done(issuer_id)) - prev_state->consider_one(issuer_id); - else - XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id); - } else { - XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled " - "transition as todo", - issuer_id); - prev_state->consider_all(); - } - break; - } else { - XBT_VERB("INDEPENDENT Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num()); - XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); - } - } - } if (state->count_todo() == 0) { // Empty interleaving set: exploration at this level is over XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1); @@ -314,11 +319,10 @@ DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Explo /* Get an enabled actor and insert it in the interleave set of the initial state */ XBT_DEBUG("Initial state. %lu actors to consider", initial_state->get_actor_count()); - if (reduction_mode_ == ReductionMode::dpor) - initial_state->consider_best(); - else - initial_state->consider_all(); - + if (reduction_mode_ == ReductionMode::dpor) + initial_state->consider_best(); + else + initial_state->consider_all(); stack_.push_back(std::move(initial_state)); } -- 2.20.1