From 685b3e4ec85031e1cb821dc3169aa2ed104b4f30 Mon Sep 17 00:00:00 2001 From: mlaurent Date: Mon, 5 Jun 2023 16:08:39 +0200 Subject: [PATCH] Fix stat missorder at the end of DFSexplorer --- examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh | 26 ++++-- examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh | 26 +++++- .../s4u-mc-electric-fence.tesh | 30 +++---- .../s4u-mc-failing-assert-nodpor.tesh | 51 ++++++++++-- .../s4u-mc-failing-assert.tesh | 52 +++++++++++- .../s4u-mc-synchro-barrier.tesh | 6 +- .../synchro-mutex/s4u-mc-synchro-mutex.tesh | 81 ++++++++++--------- .../s4u-mc-synchro-semaphore.tesh | 2 +- examples/sthread/pthread-mc-mutex-simple.tesh | 2 +- .../pthread-mc-mutex-simpledeadlock.tesh | 5 +- .../sthread/pthread-mc-producer-consumer.tesh | 9 ++- examples/sthread/stdobject/stdobject.tesh | 2 +- src/mc/api/strategy/MaxMatchComm.hpp | 6 +- src/mc/api/strategy/MinMatchComm.hpp | 6 +- src/mc/explo/DFSExplorer.cpp | 4 +- teshsuite/mc/random-bug/random-bug.tesh | 8 +- .../mc-coll-allreduce-with-leaks.tesh | 46 +---------- 17 files changed, 223 insertions(+), 139 deletions(-) diff --git a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh index 27b2bc5cf4..c04f3f230e 100644 --- a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh +++ b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh @@ -9,40 +9,56 @@ $ $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] (3:client@HostC) Sent! > [ 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] (3:client@HostC) Sent! > [ 0.000000] (2:client@HostB) Sent! -> [ 0.000000] (1:server@HostA) OK > [ 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] (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] (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] (0:maestro@) ************************** @@ -60,4 +76,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. 58 unique states visited; 10 backtracks (140 transition replays, 72 states visited overall) +> [ 0.000000] (0:maestro@) DFS exploration ended. 59 unique states visited; 14 backtracks (119 transition replays, 192 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 56813fda7e..204b615952 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. 1070 unique states visited; 252 backtracks (4082 transition replays, 2760 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 2379 unique states visited; 652 backtracks (7258 transition replays, 10289 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. 995 unique states visited; 253 backtracks (4006 transition replays, 2758 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. 930 unique states visited; 207 backtracks (2195 transition replays, 3332 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. 173 unique states visited; 29 backtracks (286 transition replays, 488 states visited overall) 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..3e9aa79b03 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,6 +9,25 @@ $ $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] 3: iSend(mbox=0) > [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) > [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) @@ -16,13 +35,34 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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_dfs/INFO] DFS exploration ended. 29 unique states visited; 5 backtracks (17 transition replays, 51 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: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 '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 *** +> [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] 2: 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] 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;2;1;1;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 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:uniform --cfg=model-check/rand-seed:42 -- ${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 'uniform' +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42' > [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 *** @@ -34,7 +74,6 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [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] [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;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 7 backtracks (19 transition replays, 70 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..5404b6e493 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,56 @@ $ $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] (1:server@Boivin) OK +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 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] (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@) ************************** +> [ 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@) 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;1;2;1' +> [ 0.000000] (0:maestro@) DFS exploration ended. 26 unique states visited; 6 backtracks (21 transition replays, 53 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] (1:server@Boivin) OK +> [ 0.000000] (2:client1@Bourassa) 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@) 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;1;1' +> [ 0.000000] (0:maestro@) DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 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] (1:server@Boivin) OK +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (3:client2@Fafard) Sent! > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** > [ 0.000000] (0:maestro@) ************************** @@ -18,4 +68,4 @@ $ $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. 13 unique states visited; 1 backtracks (1 transition replays, 15 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.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh index 4de47b1d5c..3ce27b16f2 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -29,63 +29,64 @@ $ $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) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (49 transition replays, 126 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 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 -- ${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 'model-check/strategy' to 'uniform' +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42' > [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. 647 unique states visited; 122 backtracks (871 transition replays, 1640 states visited overall) \ No newline at end of file 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/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..94c7cb7413 100644 --- a/examples/sthread/pthread-mc-producer-consumer.tesh +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -5,11 +5,12 @@ $ $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 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 --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] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform' +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42' > [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 +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 91 unique states visited; 11 backtracks (116 transition replays, 218 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/strategy/MaxMatchComm.hpp b/src/mc/api/strategy/MaxMatchComm.hpp index 4cb58913ca..b5f974c222 100644 --- a/src/mc/api/strategy/MaxMatchComm.hpp +++ b/src/mc/api/strategy/MaxMatchComm.hpp @@ -48,7 +48,7 @@ public: if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) continue; - const Transition* transition = actor.get_transition(actor.get_times_considered()); + const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); const CommRecvTransition* cast_recv = static_cast(transition); if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and @@ -68,7 +68,7 @@ public: 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()); + 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 = static_cast(transition); @@ -90,7 +90,7 @@ public: if (not actor.is_enabled() || actor.is_done()) continue; - const Transition* transition = actor.get_transition(actor.get_times_considered()); + const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); const CommRecvTransition* cast_recv = static_cast(transition); if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and diff --git a/src/mc/api/strategy/MinMatchComm.hpp b/src/mc/api/strategy/MinMatchComm.hpp index f5a9a06cd5..50fe6929ef 100644 --- a/src/mc/api/strategy/MinMatchComm.hpp +++ b/src/mc/api/strategy/MinMatchComm.hpp @@ -51,7 +51,7 @@ public: if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) continue; - const Transition* transition = actor.get_transition(actor.get_times_considered()); + const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); const CommRecvTransition* cast_recv = static_cast(transition); if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and @@ -71,7 +71,7 @@ public: 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()); + 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 = static_cast(transition); @@ -93,7 +93,7 @@ public: if (not actor.is_enabled() || actor.is_done()) continue; - const Transition* transition = actor.get_transition(actor.get_times_considered()); + const Transition* transition = actor.get_transition(actor.get_times_considered()).get(); const CommRecvTransition* cast_recv = static_cast(transition); if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index f540f7190b..fef9cc777d 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(); } 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 5377503b95..a0f27853d9 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 @@ -347,50 +347,6 @@ $ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper > Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation. > If this is too much, consider sharing allocations for computation buffers. > This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary) -> -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles: -> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90 -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers: -> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28 -> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls. -> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation. -> If this is too much, consider sharing allocations for computation buffers. -> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary) -> -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles: -> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90 -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers: -> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28 -> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls. -> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation. -> If this is too much, consider sharing allocations for computation buffers. -> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary) -> -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles: -> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90 -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers: -> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28 -> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls. -> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation. -> If this is too much, consider sharing allocations for computation buffers. -> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary) -> -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles: -> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90 -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm -> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group -> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers: -> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28 -> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls. -> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation. -> If this is too much, consider sharing allocations for computation buffers. -> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary) > > [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles: > [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90 @@ -645,4 +601,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. 1005 unique states visited; 276 backtracks (6560 transition replays, 5279 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 936 unique states visited; 254 backtracks (4843 transition replays, 6033 states visited overall) \ No newline at end of file -- 2.20.1