From: Martin Quinson Date: Wed, 7 Jun 2023 15:20:44 +0000 (+0000) Subject: Merge branch 'master' into 'master' X-Git-Tag: v3.34~41 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/f35b1984dec11869ee6a0117366ae5e7b3b4985f?hp=bfb0ac0270ecdefb05b03cc622375daa5e282d8d Merge branch 'master' into 'master' Enhancing guiding strategies for McSimGrid See merge request simgrid/simgrid!161 --- diff --git a/MANIFEST.in b/MANIFEST.in index 5fac1c74f3..0caa0f9991 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2192,8 +2192,10 @@ include src/mc/api/RemoteApp.hpp include src/mc/api/State.cpp include src/mc/api/State.hpp include src/mc/api/strategy/BasicStrategy.hpp +include src/mc/api/strategy/MaxMatchComm.hpp +include src/mc/api/strategy/MinMatchComm.hpp include src/mc/api/strategy/Strategy.hpp -include src/mc/api/strategy/WaitStrategy.hpp +include src/mc/api/strategy/UniformStrategy.hpp include src/mc/compare.cpp include src/mc/datatypes.h include src/mc/explo/CommunicationDeterminismChecker.cpp diff --git a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh index 703c4e4df2..4b8b1a9ecd 100644 --- a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh +++ b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh @@ -17,12 +17,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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] (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! @@ -44,4 +40,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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. 48 unique states visited; 6 backtracks (88 transition replays, 34 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 35 unique states visited; 5 backtracks (35 transition replays, 75 states visited overall) \ No newline at end of file diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh index bdb46989d0..bd11305ef5 100644 --- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh +++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh @@ -16,11 +16,11 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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. 220 unique states visited; 37 backtracks (603 transition replays, 346 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 910 unique states visited; 203 backtracks (1961 transition replays, 3074 states visited overall) ! expect return 1 ! timeout 20 -$ $VALGRIND_NO_TRACE_CHILDREN ${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 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:min_match_comm ${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 *** @@ -32,7 +32,25 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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] 2: 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. 128 unique states visited; 19 backtracks (309 transition replays, 162 states visited overall) +> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;2;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 625 unique states visited; 114 backtracks (1022 transition replays, 1761 states visited overall) +! expect return 1 +! timeout 20 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:max_match_comm ${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] 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. 64 unique states visited; 5 backtracks (23 transition replays, 92 states visited overall) \ No newline at end of file diff --git a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh index c00a9774f4..6e3c2f0692 100644 --- a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh +++ b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh @@ -8,11 +8,14 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [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! -> [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! > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK @@ -23,32 +26,32 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [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! > [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 +> [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! -> [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! > [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! > [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! @@ -56,37 +59,34 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [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! > [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! +> [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! -> [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! > [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 +> [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! -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 169 unique states visited; 28 backtracks (261 transition replays, 64 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 169 unique states visited; 28 backtracks (64 transition replays, 261 states visited overall) diff --git a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh index 4e4777a7a0..7c418cf725 100644 --- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh @@ -9,20 +9,41 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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] 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 (175 transition replays, 330 states visited overall) + +! expect return 1 +! timeout 300 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:max_match_comm -- ${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 'max_match_comm' +> [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] 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] 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:'3;1;1;1;2;1' -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 162 unique states visited; 48 backtracks (438 transition replays, 228 states visited overall) +> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall) + ! expect return 1 ! timeout 300 -$ $VALGRIND_NO_TRACE_CHILDREN ${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 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:min_match_comm -- ${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] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'min_match_comm' > [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 *** @@ -31,10 +52,9 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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] 3: 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] [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;1;3;1;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (0 transition replays, 25 states visited overall) \ No newline at end of file diff --git a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh index 36b3ec1901..b89fc2f58c 100644 --- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh @@ -7,6 +7,10 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 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] (2:client1@Bourassa) Sent! > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** > [ 0.000000] (0:maestro@) ************************** @@ -18,4 +22,48 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 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. 13 unique states visited; 1 backtracks (15 transition replays, 1 states visited overall) \ No newline at end of file +> [ 0.000000] (0:maestro@) DFS exploration ended. 20 unique states visited; 4 backtracks (11 transition replays, 35 states visited overall) + +! expect return 1 +! timeout 20 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:min_match_comm ${bindir:=.}/s4u-mc-failing-assert ${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@) Start a DFS exploration. Reduction is: dpor. +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (1:server@Boivin) OK +> [ 0.000000] (3:client2@Fafard) Sent! +> [ 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@) Counter-example execution trace: +> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) 3: iSend(mbox=0) +> [ 0.000000] (0:maestro@) 2: iSend(mbox=0) +> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) 1: iRecv(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;2;1;3;1;1' +> [ 0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 3 backtracks (1 transition replays, 22 states visited overall) + +! expect return 1 +! timeout 20 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:max_match_comm ${bindir:=.}/s4u-mc-failing-assert ${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@) Start a DFS exploration. Reduction is: dpor. +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (1:server@Boivin) OK +> [ 0.000000] (3:client2@Fafard) Sent! +> [ 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@) Counter-example execution trace: +> [ 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@) 3: WaitComm(from 3 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@) 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;2;1' +> [ 0.000000] (0:maestro@) DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall) \ No newline at end of file diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh index 2002f4bda1..6e8010b2ff 100644 --- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh +++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh @@ -7,7 +7,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] 0 actors remain, but none of them need to be interleaved (depth 4). > [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) +> [Checker] DFS exploration ended. 3 unique states visited; 0 backtracks (0 transition replays, 3 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" > [Checker] Start a DFS exploration. Reduction is: dpor. @@ -49,7 +49,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [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 (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) +> [Checker] DFS exploration ended. 9 unique states visited; 1 backtracks (0 transition replays, 10 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" > [Checker] Start a DFS exploration. Reduction is: dpor. @@ -124,4 +124,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [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 (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 +> [Checker] DFS exploration ended. 12 unique states visited; 1 backtracks (1 transition replays, 14 states visited overall) \ No newline at end of file diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh index 8ca73b7c62..c67f1dca86 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh @@ -7,7 +7,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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. 66 unique states visited; 11 backtracks (97 transition replays, 20 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (22 transition replays, 99 states visited overall) p The stats without checkpoints is: 130 unique states visited; 27 backtracks (308 transition replays, 151 states visited overall) p But it runs much faster (0.6 sec vs. 1.6 sec), damn slow checkpointing code. diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh index 4de47b1d5c..dd4f3c19db 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -29,63 +29,56 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [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 (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: -> [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: 2) (state=8) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9) -> [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: 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_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 (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) > [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] Dependent Transitions: +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) > [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14) +> [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] 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 (state: 11, depth: 7) +> [Checker] Backtracking from 1;1;2;1;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: 12, 0 interleaves) +> [Checker] Dependent Transitions: > [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] 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] 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] Dependent Transitions: -> [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] 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] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14) +> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (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 (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) +> [Checker] Execution came to an end at 2;1;2;2;1;1 (state: 17, depth: 7) +> [Checker] Backtracking from 2;1;2;2;1;1 +> [Checker] DFS exploration ended. 17 unique states visited; 2 backtracks (2 transition replays, 21 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 > [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. 66 unique states visited; 11 backtracks (126 transition replays, 49 states visited overall) - -$ $VALGRIND_NO_TRACE_CHILDREN ${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. 296 unique states visited; 52 backtracks (765 transition replays, 417 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (49 transition replays, 126 states visited overall) diff --git a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh index 674978da76..3a82897b91 100644 --- a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh +++ b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh @@ -3,4 +3,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${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; 8 backtracks (125 transition replays, 84 states visited overall) +> [Checker] DFS exploration ended. 33 unique states visited; 8 backtracks (84 transition replays, 125 states visited overall) diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index 9fa89df4e6..5a20784397 100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@ -10,4 +10,4 @@ $ $VALGRIND_NO_LEAK_CHECK ../../../smpi_script/bin/smpirun -wrapper "${bindir:=. > [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. 134 unique states visited; 25 backtracks (234 transition replays, 75 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 134 unique states visited; 25 backtracks (75 transition replays, 234 states visited overall) diff --git a/examples/smpi/mc/sendsend.tesh b/examples/smpi/mc/sendsend.tesh index 00c55d0a3a..08ea4b20e2 100644 --- a/examples/smpi/mc/sendsend.tesh +++ b/examples/smpi/mc/sendsend.tesh @@ -16,7 +16,7 @@ $ $VALGRIND_NO_LEAK_CHECK ../../../smpi_script/bin/smpirun -quiet -wrapper "${bi > Sent 0 to rank 1 > rank 0 recv the data > rank 1 recv the data -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 18 unique states visited; 2 backtracks (21 transition replays, 1 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 18 unique states visited; 2 backtracks (1 transition replays, 21 states visited overall) p Testing the paranoid model ! timeout 60 @@ -34,5 +34,5 @@ $ $VALGRIND_NO_LEAK_CHECK ../../../smpi_script/bin/smpirun -quiet -wrapper "${bi > [0.000000] [mc_global/INFO] 1: iSend(mbox=2) > [0.000000] [mc_global/INFO] 2: iSend(mbox=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) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 3 unique states visited; 0 backtracks (0 transition replays, 3 states visited overall) > Execution failed with code 3. diff --git a/examples/sthread/pthread-mc-mutex-simple.tesh b/examples/sthread/pthread-mc-mutex-simple.tesh index 3946c2d216..6e5bc5f1f8 100644 --- a/examples/sthread/pthread-mc-mutex-simple.tesh +++ b/examples/sthread/pthread-mc-mutex-simple.tesh @@ -15,4 +15,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > The thread 1 is terminating. > The thread 0 is terminating. > User's main is terminating. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (27 transition replays, 2 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (2 transition replays, 27 states visited overall) \ No newline at end of file diff --git a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh index 590fdc685b..5e6cac0556 100644 --- a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh +++ b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh @@ -15,6 +15,9 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > 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] ************************** @@ -31,4 +34,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > [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_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. 28 unique states visited; 2 backtracks (37 transition replays, 7 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 38 unique states visited; 3 backtracks (11 transition replays, 52 states visited overall) \ No newline at end of file diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh index 89be82586b..84efe3040f 100644 --- a/examples/sthread/pthread-mc-producer-consumer.tesh +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -5,11 +5,5 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > [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. 106 unique states visited; 17 backtracks (295 transition replays, 172 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 103 unique states visited; 16 backtracks (163 transition replays, 282 states visited overall) -$ $VALGRIND_NO_TRACE_CHILDREN ${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. 107 unique states visited; 18 backtracks (300 transition replays, 175 states visited overall) \ No newline at end of file diff --git a/examples/sthread/stdobject/stdobject.tesh b/examples/sthread/stdobject/stdobject.tesh index 8241aedd88..da50b773e6 100644 --- a/examples/sthread/stdobject/stdobject.tesh +++ b/examples/sthread/stdobject/stdobject.tesh @@ -25,4 +25,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 0.000000] (maestro@) 2: BeginObjectAccess(&v) > [ 0.000000] (maestro@) 3: BeginObjectAccess(&v) > [ 0.000000] (maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;3' -> [ 0.000000] (maestro@) DFS exploration ended. 7 unique states visited; 1 backtracks (9 transition replays, 1 states visited overall) +> [ 0.000000] (maestro@) DFS exploration ended. 7 unique states visited; 1 backtracks (1 transition replays, 9 states visited overall) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 877835fb5c..0b6fc02344 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -5,9 +5,12 @@ #include "src/mc/api/State.hpp" #include "src/mc/api/strategy/BasicStrategy.hpp" -#include "src/mc/api/strategy/WaitStrategy.hpp" +#include "src/mc/api/strategy/MaxMatchComm.hpp" +#include "src/mc/api/strategy/MinMatchComm.hpp" +#include "src/mc/api/strategy/UniformStrategy.hpp" #include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" +#include "xbt/random.hpp" #include #include @@ -21,10 +24,18 @@ long State::expended_states_ = 0; State::State(RemoteApp& remote_app) : num_(++expended_states_) { XBT_VERB("Creating a guide for the state"); + + if (_sg_mc_strategy == "none") strategy_ = std::make_shared(); - else if (_sg_mc_strategy == "nb_wait") - strategy_ = std::make_shared(); + else if (_sg_mc_strategy == "max_match_comm") + strategy_ = std::make_shared(); + else if (_sg_mc_strategy == "min_match_comm") + strategy_ = std::make_shared(); + else if (_sg_mc_strategy == "uniform") { + xbt::random::set_mersenne_seed(_sg_mc_random_seed); + strategy_ = std::make_shared(); + } else THROW_IMPOSSIBLE; @@ -41,13 +52,18 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) State::State(RemoteApp& remote_app, std::shared_ptr parent_state) : incoming_transition_(parent_state->get_transition_out()), num_(++expended_states_), parent_state_(parent_state) { - if (_sg_mc_strategy == "none") + + if (_sg_mc_strategy == "none") strategy_ = std::make_shared(); - else if (_sg_mc_strategy == "nb_wait") - strategy_ = std::make_shared(); + else if (_sg_mc_strategy == "max_match_comm") + strategy_ = std::make_shared(); + else if (_sg_mc_strategy == "min_match_comm") + strategy_ = std::make_shared(); + else if (_sg_mc_strategy == "uniform") + strategy_ = std::make_shared(); else THROW_IMPOSSIBLE; - *strategy_ = *(parent_state->strategy_); + strategy_->copy_from(parent_state_->strategy_.get()); remote_app.get_actors_status(strategy_->actors_to_run_); diff --git a/src/mc/api/strategy/BasicStrategy.hpp b/src/mc/api/strategy/BasicStrategy.hpp index 452efd4b7b..ef7bee3650 100644 --- a/src/mc/api/strategy/BasicStrategy.hpp +++ b/src/mc/api/strategy/BasicStrategy.hpp @@ -10,42 +10,38 @@ namespace simgrid::mc { -/** Basic MC guiding class which corresponds to no guide at all (random choice) */ +/** Basic MC guiding class which corresponds to no guide. When asked for different states + * it will follow a depth first search politics to minize the number of opened states. */ class BasicStrategy : public Strategy { + int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer + public: + void copy_from(const Strategy* strategy) override + { + const BasicStrategy* cast_strategy = dynamic_cast(strategy); + xbt_assert(cast_strategy != nullptr); + depth_ = cast_strategy->depth_ - 1; + xbt_assert(depth_ > 0, "The exploration reached a depth greater than %d. We will stop here to prevent weird interaction with DFSExplorer. If you want to change that behaviour, you should augment the size of the search by using --cfg=model-check/max-depth:", _sg_mc_max_depth.get()); + } BasicStrategy() = default; ~BasicStrategy() override = default; - BasicStrategy(const BasicStrategy&) = delete; - BasicStrategy& operator=(const BasicStrategy&) - { /* nothing to copy over while cloning */ - return *this; - } - std::pair next_transition() const override - { - for (auto const& [aid, actor] : 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()) { + std::pair best_transition(bool must_be_todo) const override { + for (auto const& [aid, actor] : 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() && must_be_todo) || not actor.is_enabled() || actor.is_done()) { continue; } - return std::make_pair(aid, 1); + return std::make_pair(aid, depth_); } - return std::make_pair(-1, 0); + return std::make_pair(-1, depth_); + } - void execute_next(aid_t aid, RemoteApp& app) override { return; } + - void consider_best() override - { - for (auto& [_, actor] : actors_to_run_) { - if (actor.is_todo()) - return; - if (actor.is_enabled() and not actor.is_done()) { - actor.mark_todo(); - return; - } - } - } + void execute_next(aid_t aid, RemoteApp& app) override { return; } + }; } // namespace simgrid::mc diff --git a/src/mc/api/strategy/MaxMatchComm.hpp b/src/mc/api/strategy/MaxMatchComm.hpp new file mode 100644 index 0000000000..a2f1d601a5 --- /dev/null +++ b/src/mc/api/strategy/MaxMatchComm.hpp @@ -0,0 +1,100 @@ +/* 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/TransitionComm.hpp" + +namespace simgrid::mc { + +/** Wait MC guiding class that aims at minimizing the number of in-fly communication. + * When possible, it will try to match corresponding in-fly communications. */ +class MaxMatchComm : public Strategy { + + /** Stores for each mailbox what kind of transition is waiting on it. + * Negative number means that much recv are waiting on that mailbox, while + * a positiv number means that much send are waiting there. */ + std::map mailbox_; + int value_of_state_ = 0; // used to valuate the state. Corresponds to the number of in-fly communications + // The two next values are used to save the operation we execute so the next strategy can update its field accordingly + Transition::Type last_transition_; + unsigned last_mailbox_ = 0; + +public: + void copy_from(const Strategy* strategy) override + { + const MaxMatchComm* cast_strategy = dynamic_cast(strategy); + xbt_assert(cast_strategy != nullptr); + for (auto& [id, val] : cast_strategy->mailbox_) + mailbox_[id] = val; + if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV) + mailbox_[cast_strategy->last_mailbox_]--; + if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND) + mailbox_[cast_strategy->last_mailbox_]++; + + for (auto const& [_, val] : mailbox_) + value_of_state_ += std::abs(val); + } + MaxMatchComm() = default; + ~MaxMatchComm() override = default; + + std::pair best_transition(bool must_be_todo) const override + { + std::pair min_found = std::make_pair(-1, value_of_state_+2); + for (auto const& [aid, actor] : actors_to_run_) { + if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) + continue; + + int aid_value = value_of_state_; + const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); + + const CommRecvTransition* cast_recv = dynamic_cast(transition); + if (cast_recv != nullptr) { + if (mailbox_.count(cast_recv->get_mailbox()) > 0 and + mailbox_.at(cast_recv->get_mailbox()) > 0) { + aid_value--; // This means we have waiting recv corresponding to this recv + } else { + aid_value++; + + } + } + + const CommSendTransition* cast_send = dynamic_cast(transition); + if (cast_send != nullptr) { + if (mailbox_.count(cast_send->get_mailbox()) > 0 and + mailbox_.at(cast_send->get_mailbox()) < 0) { + aid_value--; // This means we have waiting recv corresponding to this send + }else { + aid_value++; + } + } + + if (aid_value < min_found.second) + min_found = std::make_pair(aid, aid_value); + } + return min_found; + } + + + void execute_next(aid_t aid, RemoteApp& app) override + { + const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get(); + last_transition_ = transition->type_; + + const CommRecvTransition* cast_recv = dynamic_cast(transition); + if (cast_recv != nullptr) + last_mailbox_ = cast_recv->get_mailbox(); + + const CommSendTransition* cast_send = dynamic_cast(transition); + if (cast_send != nullptr) + last_mailbox_ = cast_send->get_mailbox(); + } + +}; + +} // namespace simgrid::mc + +#endif diff --git a/src/mc/api/strategy/MinMatchComm.hpp b/src/mc/api/strategy/MinMatchComm.hpp new file mode 100644 index 0000000000..665c92f91a --- /dev/null +++ b/src/mc/api/strategy/MinMatchComm.hpp @@ -0,0 +1,101 @@ +/* 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_MINWAITTAKEN_HPP +#define SIMGRID_MC_MINWAITTAKEN_HPP + +#include "src/mc/transition/TransitionComm.hpp" + +namespace simgrid::mc { + +/** Wait MC guiding class that aims at maximizing the number of in-fly communication. + * When possible, it will try not to match communications. */ +class MinMatchComm : public Strategy { + + + /** Stores for each mailbox what kind of transition is waiting on it. + * Negative number means that much recv are waiting on that mailbox, while + * a positiv number means that much send are waiting there. */ + std::map mailbox_; + /** Used to valuate the state. Corresponds to a maximum minus the number of in-fly communications. + * Maximum should be set in order not to reach 0.*/ + int value_of_state_ = _sg_mc_max_depth; + + // The two next values are used to save the operation we execute so the next strategy can update its field accordingly + Transition::Type last_transition_; + unsigned last_mailbox_ = 0; + +public: + void copy_from(const Strategy* strategy) override + { + const MinMatchComm* cast_strategy = dynamic_cast(strategy); + xbt_assert(cast_strategy != nullptr); + for (auto& [id, val] : cast_strategy->mailbox_) + mailbox_[id] = val; + if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV) + mailbox_[cast_strategy->last_mailbox_]--; + if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND) + mailbox_[cast_strategy->last_mailbox_]++; + + for (auto const& [_, val] : mailbox_) + value_of_state_ -= std::abs(val); + xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0"); + } + MinMatchComm() = default; + ~MinMatchComm() override = default; + + std::pair best_transition(bool must_be_todo) const override + { + std::pair min_found = std::make_pair(-1, value_of_state_+2); + for (auto const& [aid, actor] : actors_to_run_) { + if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) + continue; + + int aid_value = value_of_state_; + const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); + + const CommRecvTransition* cast_recv = dynamic_cast(transition); + if (cast_recv != nullptr) { + if ((mailbox_.count(cast_recv->get_mailbox()) > 0 and + mailbox_.at(cast_recv->get_mailbox()) <= 0) or mailbox_.count(cast_recv->get_mailbox()) == 0) + aid_value--; // This means we don't have waiting recv corresponding to this recv + else + aid_value++; + } + const CommSendTransition* cast_send = dynamic_cast(transition); + if (cast_send != nullptr) { + if ((mailbox_.count(cast_send->get_mailbox()) > 0 and + mailbox_.at(cast_send->get_mailbox()) >= 0) or mailbox_.count(cast_send->get_mailbox()) == 0) + aid_value--; + else + aid_value++; + } + + if (aid_value < min_found.second) + min_found = std::make_pair(aid, aid_value); + } + return min_found; + } + + + void execute_next(aid_t aid, RemoteApp& app) override + { + const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get(); + last_transition_ = transition->type_; + + const CommRecvTransition* cast_recv = dynamic_cast(transition); + if (cast_recv != nullptr) + last_mailbox_ = cast_recv->get_mailbox(); + + const CommSendTransition* cast_send = dynamic_cast(transition); + if (cast_send != nullptr) + last_mailbox_ = cast_send->get_mailbox(); + } + +}; + +} // namespace simgrid::mc + +#endif diff --git a/src/mc/api/strategy/Strategy.hpp b/src/mc/api/strategy/Strategy.hpp index de2f941fb8..96eb753e02 100644 --- a/src/mc/api/strategy/Strategy.hpp +++ b/src/mc/api/strategy/Strategy.hpp @@ -8,6 +8,7 @@ #include "simgrid/forward.h" #include "src/mc/api/RemoteApp.hpp" +#include "src/mc/mc_config.hpp" #include "xbt/asserts.h" #include #include @@ -16,32 +17,51 @@ namespace simgrid::mc { 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 */ + /** State's exploration status by actor. All actors should be present, eventually disabled for now. */ std::map actors_to_run_; public: - Strategy() = default; - virtual ~Strategy() = default; - Strategy(const Strategy&) = delete; - Strategy& operator=(const Strategy&) - { /* nothing to copy over while cloning */ - return *this; - } + /** Strategies can have values shared from parent to children state. + * This method should copy all value the strategy needs from its parent. */ + virtual void copy_from(const Strategy*) = 0; + + Strategy() = default; + virtual ~Strategy() = default; + + /** Returns the best transition among according to the strategy for this state. + * The strategy should consider only enabled transition not already done. + * Furthermore, if must_be_todo is set to true, only transitions marked as todo + * should be considered. */ + virtual std::pair best_transition(bool must_be_todo) const = 0; + + /** Returns the best transition among those that should be interleaved. */ + std::pair next_transition() { return best_transition(true); } - virtual std::pair next_transition() const = 0; + /** Allows for the strategy to update its fields knowing that the actor aid will + * be executed and a children strategy will then be created. */ virtual void execute_next(aid_t aid, RemoteApp& app) = 0; - virtual void consider_best() = 0; - // Mark the first enabled and not yet done transition as todo - // If there's already a transition marked as todo, does nothing + /** Ensure at least one transition is marked as todo among the enabled ones not done. + * If required, it marks as todo the best transition according to the strategy. */ + void consider_best() { + for (auto& [_, actor] :actors_to_run_) + if (actor.is_todo()) + return; + aid_t best_aid = best_transition(false).first; + if (best_aid != -1) + actors_to_run_.at(best_aid).mark_todo(); + } + + // Mark aid as todo. If it makes no sense, ie. if it is already done or not enabled, + // else raise an error void consider_one(aid_t aid) { xbt_assert(actors_to_run_.at(aid).is_enabled() and not actors_to_run_.at(aid).is_done(), "Tried to mark as TODO actor %ld but it is either not enabled or already done", aid); actors_to_run_.at(aid).mark_todo(); } - // Matk as todo all actors enabled that are not done yet + // Mark as todo all actors enabled that are not done yet and return the number + // of marked actors unsigned long consider_all() { unsigned long count = 0; diff --git a/src/mc/api/strategy/UniformStrategy.hpp b/src/mc/api/strategy/UniformStrategy.hpp new file mode 100644 index 0000000000..8e9726f44a --- /dev/null +++ b/src/mc/api/strategy/UniformStrategy.hpp @@ -0,0 +1,69 @@ +/* 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_UNIFORMSTRATEGY_HPP +#define SIMGRID_MC_UNIFORMSTRATEGY_HPP + +#include "src/mc/transition/Transition.hpp" +#include "xbt/random.hpp" + +#define MAX_RAND 100000 + +namespace simgrid::mc { + +/** Guiding strategy that valuate states randomly */ +class UniformStrategy : public Strategy { + std::map valuation; + +public: + UniformStrategy() + { + for (long aid = 0; aid < 10; aid++) + valuation[aid] = xbt::random::uniform_int(0, MAX_RAND); + } + void copy_from(const Strategy* strategy) override + { + for (auto& [aid, _] : actors_to_run_) + valuation[aid] = xbt::random::uniform_int(0, MAX_RAND); + } + + std::pair best_transition(bool must_be_todo) const override + { + int possibilities = 0; + + // Consider only valid actors + for (auto const& [aid, actor] : actors_to_run_) { + if ((actor.is_todo() or not must_be_todo) and (not actor.is_done()) and actor.is_enabled()) + possibilities++; + } + + int chosen; + if (possibilities == 0) + return std::make_pair(-1, 0); + if (possibilities == 1) + chosen = 0; + else + chosen = xbt::random::uniform_int(0, possibilities-1); + + for (auto const& [aid, actor] : actors_to_run_) { + if (((not actor.is_todo()) and must_be_todo) or actor.is_done() or (not actor.is_enabled())) + continue; + if (chosen == 0) { + return std::make_pair(aid, valuation.at(aid)); + } + chosen--; + } + + return std::make_pair(-1, 0); + } + + + void execute_next(aid_t aid, RemoteApp& app) override {} + +}; + +} // namespace simgrid::mc + +#endif diff --git a/src/mc/api/strategy/WaitStrategy.hpp b/src/mc/api/strategy/WaitStrategy.hpp deleted file mode 100644 index ed5b9a0eed..0000000000 --- a/src/mc/api/strategy/WaitStrategy.hpp +++ /dev/null @@ -1,87 +0,0 @@ -/* 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 "Strategy.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 { - int taken_wait_ = 0; - bool taking_wait_ = false; - -public: - WaitStrategy() = default; - ~WaitStrategy() override = default; - WaitStrategy(const WaitStrategy&) = delete; - WaitStrategy& operator=(const WaitStrategy& guide) - { - taken_wait_ = guide.taken_wait_; - return *this; - } - - 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 next_transition() const override - { - std::pair if_no_wait = std::make_pair(-1, 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 const& 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 - { - aid_t aid = next_transition().first; - if (auto actor = actors_to_run_.find(aid); 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 diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index a5f06d5557..aa7fbb023c 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -112,8 +112,8 @@ void DFSExplorer::log_state() // override on_log_state_signal(get_remote_app()); XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states " "visited overall)", - State::get_expanded_states(), backtrack_count_, visited_states_count_, - Transition::get_replayed_transitions()); + State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(), + visited_states_count_); Exploration::log_state(); } @@ -372,7 +372,7 @@ std::shared_ptr DFSExplorer::best_opened_state() continue; if (valid != current) *valid = std::move(*current); - if (best == end(opened_states_) || prio > best_prio) { + if (best == end(opened_states_) || prio < best_prio) { best_prio = prio; best = valid; } diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 1d9375f627..571ec6ea8d 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -70,8 +70,15 @@ simgrid::config::Flag _sg_mc_strategy{ "model-check/strategy", "Specify the the kind of heuristic to use for guided model-checking", "none", - {{"none", "No specific strategy: simply pick the first available transistion."}, - {"nb_wait", "Take any enabled wait transition, to reduce the distance between an async and its wait."}}}; + {{"none", "No specific strategy: simply pick the first available transistion and act as a DFS."}, + {"max_match_comm", "Try to minimize the number of in-fly communication by appairing matching send and receive."}, + {"min_match_comm", "Try to maximize the number of in-fly communication by not appairing matching send and receive."}, + {"uniform", "No specific strategy: choices are made randomly based on a uniform sampling."} + }}; + +simgrid::config::Flag _sg_mc_random_seed{"model-check/rand-seed", + "give a specific random seed to initialize the uniform distribution", 0, + [](int) { _mc_cfg_cb_check("Random seed"); }}; #if SIMGRID_HAVE_STATEFUL_MC simgrid::config::Flag _sg_mc_checkpoint{ diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index b544580d3c..07d199f0fb 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -25,6 +25,7 @@ extern XBT_PUBLIC simgrid::config::Flag _sg_mc_send_determinism; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_unfolding_checker; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_timeout; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_max_depth; +extern XBT_PRIVATE simgrid::config::Flag _sg_mc_random_seed; extern "C" XBT_PUBLIC int _sg_mc_max_visited_states; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_dot_output_file; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_termination; diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp index f532369d28..220b7cb501 100644 --- a/src/mc/transition/TransitionAny.cpp +++ b/src/mc/transition/TransitionAny.cpp @@ -27,9 +27,11 @@ TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::st } std::string TestAnyTransition::to_string(bool verbose) const { - auto res = xbt::string_printf("TestAny{ "); - for (auto const* t : transitions_) + auto res = xbt::string_printf("TestAny(%s){ ", this->result() ? "TRUE" : "FALSE"); + for (auto const* t : transitions_) { res += t->to_string(verbose); + res += "; "; + } res += " }"; return res; } diff --git a/src/mc/transition/TransitionAny.hpp b/src/mc/transition/TransitionAny.hpp index df5954e6ba..b0648119b1 100644 --- a/src/mc/transition/TransitionAny.hpp +++ b/src/mc/transition/TransitionAny.hpp @@ -8,6 +8,7 @@ #include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/transition/Transition.hpp" +#include "src/mc/transition/TransitionComm.hpp" #include #include @@ -23,6 +24,15 @@ public: bool depends(const Transition* other) const override; Transition* get_current_transition() const { return transitions_.at(times_considered_); } + bool result() const + { + for (Transition* transition : transitions_) { + CommTestTransition* tested_transition = static_cast(transition); + if (tested_transition->get_sender() != -1 and tested_transition->get_receiver() != -1) + return true; + } + return false; + } }; class WaitAnyTransition : public Transition { diff --git a/teshsuite/mc/random-bug/random-bug.tesh b/teshsuite/mc/random-bug/random-bug.tesh index 5dbc3806ce..46ab37aa9d 100644 --- a/teshsuite/mc/random-bug/random-bug.tesh +++ b/teshsuite/mc/random-bug/random-bug.tesh @@ -10,7 +10,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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. 26 unique states visited; 21 backtracks (65 transition replays, 18 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall) ! expect return 6 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6 @@ -25,14 +25,14 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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. 26 unique states visited; 21 backtracks (65 transition replays, 18 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall) > [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc $ $VALGRIND_NO_TRACE_CHILDREN ${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; 35 backtracks (108 transition replays, 30 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 35 backtracks (30 transition replays, 108 states visited overall) ! expect return 6 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6 @@ -48,5 +48,5 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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. 26 unique states visited; 21 backtracks (65 transition replays, 18 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall) > [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc diff --git a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh index 03726da579..abdf4d4bf0 100644 --- a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh +++ b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh @@ -73,4 +73,4 @@ $ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper > 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. 230 unique states visited; 56 backtracks (1171 transition replays, 885 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 230 unique states visited; 56 backtracks (885 transition replays, 1171 states visited overall) \ No newline at end of file diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 55875a9c83..28c0892382 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -637,8 +637,10 @@ set(MC_SRC_STATEFUL src/mc/mc_record.cpp src/mc/api/strategy/BasicStrategy.hpp + src/mc/api/strategy/MaxMatchComm.hpp + src/mc/api/strategy/MinMatchComm.hpp src/mc/api/strategy/Strategy.hpp - src/mc/api/strategy/WaitStrategy.hpp + src/mc/api/strategy/UniformStrategy.hpp src/xbt/mmalloc/mm_interface.c )