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/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] (1:server@HostA) OK
> [ 0.000000] (4:client@HostD) Sent!
> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (4:client@HostD) Sent!
-> [ 0.000000] (3:client@HostC) Sent!
-> [ 0.000000] (1:server@HostA) OK
-> [ 0.000000] (2:client@HostB) Sent!
> [ 0.000000] (3:client@HostC) Sent!
> [ 0.000000] (1:server@HostA) OK
> [ 0.000000] (4:client@HostD) Sent!
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) 4: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) 1: WaitComm(from 4 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@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 2: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 4: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 4 to 1, mbox=0, no timeout)
-> [ 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@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2;1;1;2;4;1;1;3;1'
-> [ 0.000000] (0:maestro@) DFS exploration ended. 59 unique states visited; 14 backtracks (192 transition replays, 119 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;4;1;1;2;1;1;2;3;1'
+> [ 0.000000] (0:maestro@) DFS exploration ended. 32 unique states visited; 2 backtracks (36 transition replays, 2 states visited overall)
\ No newline at end of file
> [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] 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. 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/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] **************************
+> [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] 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. 2091 unique states visited; 529 backtracks (8359 transition replays, 5739 states visited overall)
+> [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
> [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!
-> [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!
> [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!
-> [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!
> [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!
> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
+> [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!
> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
> [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!
-> [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!
> [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!
+> [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!
> [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. 169 unique states visited; 29 backtracks (261 transition replays, 64 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 (261 transition replays, 64 states visited overall)
\ No newline at end of file
> [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:'1;3;1;1;2;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 119 unique states visited; 36 backtracks (330 transition replays, 175 states visited overall)
+> [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/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/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 ***
+> [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] 1: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] 2: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [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;2;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 8 unique states visited; 0 backtracks (8 transition replays, 0 states visited overall)
> [ 0.000000] (2:client1@Bourassa) Sent!
> [ 0.000000] (1:server@Boivin) OK
> [ 0.000000] (3:client2@Fafard) Sent!
-> [ 0.000000] (1:server@Boivin) OK
-> [ 0.000000] (3:client2@Fafard) Sent!
-> [ 0.000000] (2:client1@Bourassa) Sent!
-> [ 0.000000] (1:server@Boivin) OK
-> [ 0.000000] (3:client2@Fafard) Sent!
-> [ 0.000000] (2:client1@Bourassa) Sent!
-> [ 0.000000] (1:server@Boivin) OK
-> [ 0.000000] (3:client2@Fafard) Sent!
-> [ 0.000000] (1:server@Boivin) OK
-> [ 0.000000] (3:client2@Fafard) Sent!
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 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. 29 unique states visited; 5 backtracks (49 transition replays, 15 states visited overall)
\ No newline at end of file
+> [ 0.000000] (0:maestro@) DFS exploration ended. 13 unique states visited; 1 backtracks (15 transition replays, 1 states visited overall)
\ No newline at end of file
> [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] 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; 1 backtracks (3 transition replays, 0 states visited overall)
+> [Checker] DFS exploration ended. 3 unique states visited; 0 backtracks (3 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 2 --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] Dependent Transitions:
> [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] 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] 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; 2 backtracks (10 transition replays, 0 states visited overall)
+> [Checker] DFS exploration ended. 9 unique states visited; 1 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] Dependent Transitions:
> [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] 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] 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; 2 backtracks (14 transition replays, 1 states visited overall)
\ No newline at end of file
+> [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] 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: 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] 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:
-> [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] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 9, 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_ASYNC_LOCK(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] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 10, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=10)
+> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 11, 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] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=10)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=11)
+> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, 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] 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] 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] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 14, 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] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14)
> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves)
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (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] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=15)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (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)
+> [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. 128 unique states visited; 26 backtracks (296 transition replays, 143 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 -- ${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/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. 4645 unique states visited; 1082 backtracks (18004 transition replays, 12278 states visited overall)
+> [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
$ ${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. 33 unique states visited; 9 backtracks (125 transition replays, 84 states visited overall)
+> [Checker] DFS exploration ended. 33 unique states visited; 8 backtracks (125 transition replays, 84 states visited overall)
> [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. 242 unique states visited; 68 backtracks (612 transition replays, 303 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 313 unique states visited; 89 backtracks (810 transition replays, 408 states visited overall)
> Sent 0 to rank 1
> rank 1 recv the data
> rank 0 recv the data
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 30 unique states visited; 8 backtracks (56 transition replays, 19 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 30 unique states visited; 7 backtracks (56 transition replays, 19 states visited overall)
p Testing the paranoid model
! timeout 60
> [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_dfs/INFO] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
+> [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.
> The thread 0 is terminating.
> The thread 1 is terminating.
> User's main is terminating.
-> The thread 0 is terminating.
> The thread 1 is terminating.
+> The thread 0 is terminating.
> User's main is terminating.
-> The thread 1 is terminating.
> 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; 3 backtracks (27 transition replays, 2 states visited overall)
+> [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
> The thread 0 is terminating.
> The thread 1 is terminating.
> User's main is terminating.
-> The thread 0 is terminating.
-> The thread 1 is terminating.
-> User's main is terminating.
-> The thread 0 is terminating.
-> The thread 1 is terminating.
-> User's main is terminating.
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
> [0.000000] [mc_global/INFO] **************************
> [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_dfs/INFO] DFS exploration ended. 38 unique states visited; 4 backtracks (52 transition replays, 11 states visited overall)
\ No newline at end of file
+> [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
> [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. 719 unique states visited; 83 backtracks (1854 transition replays, 1053 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/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/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 (2950 transition replays, 1713 states visited overall)
\ No newline at end of file
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 */
}
void mark_done() { this->state_ = InterleavingType::done; }
- inline Transition* get_transition(unsigned times_considered)
+ inline Transition* get_transition(unsigned times_considered) const
{
xbt_assert(times_considered < this->pending_transitions_.size(),
"Actor %ld does not have a state available transition with `times_considered = %u`,\n"
* 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/strategy/BasicStrategy.hpp"
+#include "src/mc/api/strategy/WaitStrategy.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
long State::expended_states_ = 0;
-State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_unique<BasicGuide>())
+State::State(RemoteApp& remote_app) : num_(++expended_states_)
{
- remote_app.get_actors_status(guide->actors_to_run_);
+ XBT_VERB("Creating a guide for the state");
+ 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(strategy_->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
*remote_app.get_remote_process_memory());
}
-State::State(RemoteApp& remote_app, const State* parent_state)
- : num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique<BasicGuide>())
+State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
+ : num_(++expended_states_), parent_state_(parent_state)
{
- remote_app.get_actors_status(guide->actors_to_run_);
+
+ 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(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] : strategy_->actors_to_run_)
+ if (actor.is_todo())
+ count += actor.get_times_not_considered();
+
+ return count;
}
Transition* State::get_transition() const
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
+ 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"
*/
Transition* transition_ = default_transition_.get();
+ /** @brief A list of transition to be replayed in order to get in this state. */
+ std::list<Transition*> recipe_;
+
/** Sequential state ID (used for debugging) */
long num_ = 0;
/** Unique parent of this state. Required both for sleep set computation
and for guided model-checking */
- const State* parent_state_;
+ std::shared_ptr<State> parent_state_ = nullptr;
- std::unique_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
public:
explicit State(RemoteApp& remote_app);
- explicit State(RemoteApp& remote_app, const State* parent_state);
+ explicit State(RemoteApp& remote_app, std::shared_ptr<State> parent_state);
/* Returns a positive number if there is another transition to pick, or -1 if not */
aid_t next_transition() const; // this function should disapear as it is redundant with the next one
long get_num() const { return num_; }
std::size_t count_todo() const;
+ std::size_t count_todo_multiples() const;
- void consider_one(aid_t aid) { guide->consider_one(aid); }
- void consider_best() { guide->consider_best(); }
- void consider_all() { guide->consider_all(); }
+ /* Marking as TODO some actor in this state:
+ * + 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) { 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::map<aid_t, ActorState> const& get_actors_list() const { return guide->actors_to_run_; }
+ 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 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) */
-// Not Yet fully implemented
-class BasicGuide : public GuidedState {
+class BasicStrategy : public Strategy {
public:
+ void operator=(const BasicStrategy&) { return; }
+
std::pair<aid_t, double> next_transition() const override
{
for (auto const& [aid, actor] : actors_to_run_) {
#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;
actors_to_run_.at(aid).mark_todo();
}
// Matk as todo all actors enabled that are not done yet
- void consider_all()
+ unsigned long consider_all()
{
+ unsigned long count = 0;
for (auto& [_, actor] : actors_to_run_)
- if (actor.is_enabled() and not actor.is_done())
+ if (actor.is_enabled() and not actor.is_done()) {
actor.mark_todo();
+ count++;
+ }
+ return count;
}
friend class State;
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* 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_WAITSTRATEGY_HPP
+#define SIMGRID_MC_WAITSTRATEGY_HPP
+
+#include "src/mc/transition/Transition.hpp"
+
+namespace simgrid::mc {
+
+/** 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 WaitStrategy : public Strategy {
+ double taken_wait_ = 0;
+ bool taking_wait_ = false;
+
+public:
+ void operator=(const WaitStrategy& guide) { taken_wait_ = guide.taken_wait_; }
+
+ bool is_transition_wait(Transition::Type type) const
+ {
+ return type == Transition::Type::WAITANY or type == Transition::Type::BARRIER_WAIT or
+ type == Transition::Type::MUTEX_WAIT or type == Transition::Type::SEM_WAIT;
+ }
+
+ std::pair<aid_t, double> next_transition() const override
+ {
+ std::pair<aid_t, double> if_no_wait = std::make_pair(-1, 0.0);
+ for (auto const& [aid, actor] : actors_to_run_) {
+ if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
+ continue;
+ if (is_transition_wait(actor.get_transition(actor.get_times_considered())->type_))
+ return std::make_pair(aid, -(taken_wait_ + 1));
+ if_no_wait = std::make_pair(aid, -taken_wait_);
+ }
+ return if_no_wait;
+ }
+
+ /** If we are taking a wait transition, and last transition wasn't a wait, we need to increment the number
+ * of wait taken. On the opposite, if we took a wait before, and now we are taking another transition, we need
+ * to decrease the count. */
+ void execute_next(aid_t aid, RemoteApp& app) override
+ {
+ auto& actor = actors_to_run_.at(aid);
+ if ((not taking_wait_) and is_transition_wait(actor.get_transition(actor.get_times_considered())->type_)) {
+ taken_wait_++;
+ taking_wait_ = true;
+ return;
+ }
+ if (taking_wait_ and (not is_transition_wait(actor.get_transition(actor.get_times_considered())->type_))) {
+ taken_wait_--;
+ taking_wait_ = false;
+ return;
+ }
+ }
+
+ void consider_best() override
+ {
+ const auto& [aid, _] = this->next_transition();
+ auto actor = actors_to_run_.find(aid);
+ if (actor != actors_to_run_.end()) {
+ actor->second.mark_todo();
+ return;
+ }
+ for (auto& [_, actor] : actors_to_run_) {
+ if (actor.is_todo())
+ return;
+ if (actor.is_enabled() and not actor.is_done()) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ }
+};
+
+} // namespace simgrid::mc
+
+#endif
RecordTrace DFSExplorer::get_record_trace() // override
{
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;
}
+void DFSExplorer::restore_stack(std::shared_ptr<State> state)
+{
+
+ stack_ = std::list<std::shared_ptr<State>>();
+ std::shared_ptr<State> current_state(state);
+ stack_.push_front(std::shared_ptr<State>(current_state));
+ // condition corresponds to reaching initial state
+ while (current_state->get_parent_state() != nullptr) {
+ current_state = current_state->get_parent_state();
+ stack_.push_front(std::shared_ptr<State>(current_state));
+ }
+ XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
+}
+
void DFSExplorer::log_state() // override
{
on_log_state_signal(get_remote_app());
while (not stack_.empty()) {
/* Get current state */
- State* state = stack_.back().get();
+ std::shared_ptr<State> state(stack_.back());
XBT_DEBUG("**************************************************");
XBT_DEBUG("Exploration depth=%zu (state:#%ld; %zu interleaves todo)", stack_.size(), state->get_num(),
}
// Search for the next transition
- // next_transition returns a pair<aid_t, double> in case we want to consider multiple state
+ // next_transition returns a pair<aid_t, double> in case we want to consider multiple state (eg. during backtrack)
auto [next, _] = state->next_transition_guided();
if (next < 0) { // If there is no more transition in the current state, backtrack.
- XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
- stack_.size() + 1);
+ 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) {
get_remote_app().finalize_app();
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<State> next_state;
-
- next_state = std::make_unique<State>(get_remote_app(), state);
+ std::shared_ptr<State> next_state = std::make_shared<State>(get_remote_app(), state);
on_state_creation_signal(next_state.get(), get_remote_app());
/* Sleep set procedure:
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();
+ aid_t issuer_id = state->get_transition()->aid_;
+ 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_) {
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);
+ tmp_stack.pop_back();
continue;
} else if (prev_state->get_transition()->depends(state->get_transition())) {
XBT_VERB("Dependent Transitions:");
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))
+ if (not prev_state->is_actor_done(issuer_id)) {
prev_state->consider_one(issuer_id);
- else
+ opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+ } 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();
+ // 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;
} else {
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());
}
+ tmp_stack.pop_back();
}
}
+ // Before leaving that state, if the transition we just took can be taken multiple times, we
+ // need to give it to the opened states
+ if (stack_.back()->count_todo_multiples() > 0)
+ opened_states_.push(std::shared_ptr<State>(stack_.back()));
+
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
if (_sg_mc_max_visited_states > 0)
visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app());
+ stack_.push_back(std::move(next_state));
+
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
if (reduction_mode_ == ReductionMode::dpor)
- next_state->consider_best(); // Take only one transition if DPOR: others may be considered later if required
- else
- next_state->consider_all();
+ stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required
+ else {
+ stack_.back()->consider_all();
+ }
- dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
+ dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
state->get_transition()->dot_string().c_str());
} else
dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_,
state->get_transition()->dot_string().c_str());
-
- stack_.push_back(std::move(next_state));
}
-
log_state();
}
void DFSExplorer::backtrack()
{
- backtrack_count_++;
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
+ XBT_DEBUG("%lu alternatives are yet to be explored:", opened_states_.size());
+
on_backtracking_signal(get_remote_app());
get_remote_app().check_deadlock();
- /* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set.
- * In the first case, we need to remove the last transition corresponding to the Finalize */
- if (stack_.back()->get_transition()->aid_ == 0)
- 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. */
- bool found_backtracking_point = false;
- while (not stack_.empty() && not found_backtracking_point) {
- std::unique_ptr<State> state = std::move(stack_.back());
-
- stack_.pop_back();
-
+ // if no backtracking point, then set the stack_ to empty so we can end the exploration
+ if (opened_states_.empty()) {
+ XBT_DEBUG("No more opened point of exploration, the search will end");
+ stack_ = std::list<std::shared_ptr<State>>();
+ return;
+ }
- 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);
+ std::shared_ptr<State> backtracking_point = opened_states_.top(); // Take the point with smallest distance
+ opened_states_.pop();
- } else {
- XBT_DEBUG("Back-tracking to state %ld at depth %zu: %lu transitions left to be explored", state->get_num(),
- stack_.size() + 1, state->count_todo());
- stack_.push_back(
- std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
- found_backtracking_point = true;
- }
+ // 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. Let's backtrack again");
+ this->backtrack();
+ return;
}
- if (found_backtracking_point) {
- /* If asked to rollback on a state that has a snapshot, restore it */
- State* last_state = stack_.back().get();
- if (const auto* system_state = last_state->get_system_state()) {
- system_state->restore(*get_remote_app().get_remote_process_memory());
- on_restore_system_state_signal(last_state, get_remote_app());
- return;
- }
+ // We found a real backtracking point, let's go to it
+ backtrack_count_++;
+ XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num());
+ /* If asked to rollback on a state that has a snapshot, restore it */
+ if (const auto* system_state = backtracking_point->get_system_state()) {
+ system_state->restore(*get_remote_app().get_remote_process_memory());
+ on_restore_system_state_signal(backtracking_point.get(), get_remote_app());
+ this->restore_stack(backtracking_point);
+ return;
+ }
- /* if no snapshot, we need to restore the initial state and replay the transitions */
- get_remote_app().restore_initial_state();
- on_restore_initial_state_signal(get_remote_app());
-
- /* Traverse the stack from the state at position start and re-execute the transitions */
- for (std::unique_ptr<State> const& state : stack_) {
- if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
- break;
- state->get_transition()->replay(get_remote_app());
- on_transition_replay_signal(state->get_transition(), get_remote_app());
- visited_states_count_++;
- }
- } // If no backtracing point, then the stack is empty and the exploration is over
+ /* if no snapshot, we need to restore the initial state and replay the transitions */
+ get_remote_app().restore_initial_state();
+ on_restore_initial_state_signal(get_remote_app());
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (auto& state : backtracking_point->get_recipe()) {
+ state->replay(get_remote_app());
+ on_transition_replay_signal(state, get_remote_app());
+ visited_states_count_++;
+ }
+ this->restore_stack(backtracking_point);
}
DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info)
} else
XBT_INFO("Start a DFS exploration. Reduction is: %s.", to_c_str(reduction_mode_));
- auto initial_state = std::make_unique<State>(get_remote_app());
+ auto initial_state = std::make_shared<State>(get_remote_app());
XBT_DEBUG("**************************************************");
+ stack_.push_back(std::move(initial_state));
+
/* 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());
+ XBT_DEBUG("Initial state. %lu actors to consider", stack_.back()->get_actor_count());
if (reduction_mode_ == ReductionMode::dpor)
- initial_state->consider_best();
- else
- initial_state->consider_all();
-
- stack_.push_back(std::move(initial_state));
+ stack_.back()->consider_best();
+ else {
+ stack_.back()->consider_all();
+ }
+ if (stack_.back()->count_todo_multiples() > 1)
+ opened_states_.push(std::shared_ptr<State>(stack_.back()));
}
Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)
namespace simgrid::mc {
+typedef std::list<std::shared_ptr<State>> stack_t;
+
+/* Used to compare two stacks and decide which one is better to backtrack,
+ * regarding the chosen guide in the last state. */
+class OpenedStatesCompare {
+public:
+ bool operator()(std::shared_ptr<State> const& lhs, std::shared_ptr<State> const& rhs)
+ {
+ return lhs->next_transition_guided().second < rhs->next_transition_guided().second;
+ }
+};
+
class XBT_PRIVATE DFSExplorer : public Exploration {
+
XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor);
ReductionMode reduction_mode_;
void backtrack();
/** Stack representing the position in the exploration graph */
- std::list<std::unique_ptr<State>> stack_;
+ stack_t stack_;
VisitedStates visited_states_;
std::unique_ptr<VisitedState> visited_state_;
+
+ /** Opened states are states that still contains todo actors.
+ * When backtracking, we pick a state from it*/
+
+ std::priority_queue<std::shared_ptr<State>, std::vector<std::shared_ptr<State>>, OpenedStatesCompare> opened_states_;
+
+ /** Change current stack_ value to correspond to the one we would have
+ * had if we executed transition to get to state. This is required when
+ * backtracking, and achieved thanks to the fact states save their parent.*/
+ void restore_stack(std::shared_ptr<State> state);
+
+ RecordTrace get_record_trace_of_stack(stack_t stack);
};
} // namespace simgrid::mc
"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_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_strategy;
#endif
struct s_mc_message_actors_status_answer_t answer = {};
answer.type = MessageType::ACTORS_STATUS_REPLY_COUNT;
- answer.count = static_cast<int>(status.size());
+ answer.count = static_cast<int>(status.size());
xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
if (answer.count > 0) {
void Transition::replay(RemoteApp& app) const
{
replayed_transitions_++;
-
#if SIMGRID_HAVE_MC
app.handle_simcall(aid_, times_considered_, false);
app.wait_for_requests();
comm_->increment_sent_messages_count(comm_->group()->rank(src_), comm_->group()->rank(dst_), tag_);
void* buf = buf_;
- if ((flags_ & MPI_REQ_SSEND) == 0 &&
- ((flags_ & MPI_REQ_RMA) != 0 || (flags_ & MPI_REQ_BSEND) != 0 ||
- static_cast<int>(size_) < smpi_cfg_detached_send_thresh())) {
+ if ((flags_ & MPI_REQ_SSEND) == 0 && ((flags_ & MPI_REQ_RMA) != 0 || (flags_ & MPI_REQ_BSEND) != 0 ||
+ static_cast<int>(size_) < smpi_cfg_detached_send_thresh())) {
detached_ = true;
XBT_DEBUG("Send request %p is detached", this);
this->ref();
> [ 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. 20 unique states visited; 15 backtracks (47 transition replays, 12 states visited overall)
! expect return 6
# because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
> [ 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. 20 unique states visited; 15 backtracks (47 transition replays, 12 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
> [ 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; 36 backtracks (108 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
> [ 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. 20 unique states visited; 15 backtracks (47 transition replays, 12 states visited overall)
> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
> 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. 616 unique states visited; 167 backtracks (3773 transition replays, 2991 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/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/strategy/BasicStrategy.hpp
+ src/mc/api/strategy/Strategy.hpp
+ src/mc/api/strategy/WaitStrategy.hpp
+
src/xbt/mmalloc/mm_interface.c
)
