From a121f8b79e4e8a7104243fdc74e80f298dca4881 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 29 Jun 2023 22:31:05 +0200 Subject: [PATCH] Show the user-level call in MC backtraces --- examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh | 20 ++++----- examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh | 44 +++++++++---------- .../s4u-mc-failing-assert-nodpor.tesh | 40 ++++++++--------- .../s4u-mc-failing-assert.tesh | 40 ++++++++--------- .../pthread-mc-mutex-simpledeadlock.tesh | 12 ++--- examples/sthread/stdobject/stdobject.tesh | 4 +- src/instr/instr_smpi.hpp | 2 +- src/mc/explo/Exploration.cpp | 10 ++++- src/mc/transition/Transition.hpp | 7 +-- src/mc/transition/TransitionComm.cpp | 8 ++-- src/smpi/internals/smpi_replay.cpp | 2 +- teshsuite/mc/random-bug/random-bug.tesh | 12 ++--- 12 files changed, 104 insertions(+), 97 deletions(-) diff --git a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh index 424e312b7a..022c225f4b 100644 --- a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh +++ b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh @@ -15,15 +15,15 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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@) 2: iSend(mbox=0) -> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout) -> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0) -> [ 0.000000] (0:maestro@) 2: WaitComm(from 2 to 1, mbox=0, no timeout) -> [ 0.000000] (0:maestro@) 4: iSend(mbox=0) -> [ 0.000000] (0:maestro@) 1: WaitComm(from 4 to 1, mbox=0, no timeout) -> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0) -> [ 0.000000] (0:maestro@) 3: iSend(mbox=0) -> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 2 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 4 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 4 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: 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. 19 unique states visited; 2 backtracks (12 transition replays, 33 states visited overall) diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh index 10cc2f3723..83991dad80 100644 --- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh +++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh @@ -8,13 +8,13 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID *** > [0.000000] [mc_explo/INFO] ************************** > [0.000000] [mc_explo/INFO] Counter-example execution trace: -> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: 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. 98 unique states visited; 21 backtracks (153 transition replays, 272 states visited overall) @@ -26,14 +26,14 @@ $ $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] 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] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: 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;2;1' > [0.000000] [mc_dfs/INFO] DFS exploration ended. 83 unique states visited; 12 backtracks (65 transition replays, 160 states visited overall) @@ -45,12 +45,12 @@ $ $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] 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] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: 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. 44 unique states visited; 3 backtracks (11 transition replays, 58 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 3b770742f2..0a7b1709d2 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,12 +9,12 @@ $ $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] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: 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. 24 unique states visited; 8 backtracks (26 transition replays, 58 states visited overall) @@ -28,13 +28,13 @@ $ $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] 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] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: 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;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) @@ -49,12 +49,12 @@ $ $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] 2: 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] 1: WaitComm(from 2 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: 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;3;1;1' > [0.000000] [mc_dfs/INFO] DFS exploration ended. 29 unique states visited; 10 backtracks (26 transition replays, 65 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 fe7f6c9b09..1d5166eb2c 100644 --- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh @@ -12,12 +12,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 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@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: 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. 15 unique states visited; 2 backtracks (4 transition replays, 21 states visited overall) @@ -33,13 +33,13 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 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@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: 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) @@ -55,12 +55,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 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@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout) +> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0) +> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0) +> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: 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/sthread/pthread-mc-mutex-simpledeadlock.tesh b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh index e95629cea0..2de4e42603 100644 --- a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh +++ b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh @@ -21,11 +21,11 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3) > [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) > [0.000000] [mc_global/INFO] Counter-example execution trace: -> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) -> [0.000000] [mc_global/INFO] 2: MUTEX_WAIT(mutex: 0, owner: 2) -> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) -> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) -> [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner: 3) -> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall 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. 21 unique states visited; 3 backtracks (11 transition replays, 35 states visited overall) \ No newline at end of file diff --git a/examples/sthread/stdobject/stdobject.tesh b/examples/sthread/stdobject/stdobject.tesh index fefbd72569..457238ced8 100644 --- a/examples/sthread/stdobject/stdobject.tesh +++ b/examples/sthread/stdobject/stdobject.tesh @@ -21,7 +21,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c > [ 0.000000] (maestro@) *** PROPERTY NOT VALID *** > [ 0.000000] (maestro@) ************************** > [ 0.000000] (maestro@) Counter-example execution trace: -> [ 0.000000] (maestro@) 2: BeginObjectAccess(&v) -> [ 0.000000] (maestro@) 3: BeginObjectAccess(&v) +> [ 0.000000] (maestro@) Actor 2 in simcall BeginObjectAccess(&v) +> [ 0.000000] (maestro@) Actor 3 in simcall 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 (1 transition replays, 9 states visited overall) diff --git a/src/instr/instr_smpi.hpp b/src/instr/instr_smpi.hpp index 309dd16228..d0633285e8 100644 --- a/src/instr/instr_smpi.hpp +++ b/src/instr/instr_smpi.hpp @@ -37,7 +37,7 @@ public: std::to_string(linenumber); } - std::string get_call_location() const { return filename + "::" + func_call + "::" + std::to_string(linenumber); } + std::string get_call_location() const { return filename + ":" + std::to_string(linenumber) + ":" + func_call + "()"; } }; #endif diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 8bf01108a3..f6b4c85299 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -86,8 +86,14 @@ static const char* signal_name(int status) std::vector Exploration::get_textual_trace() { std::vector trace; - for (auto const& transition : get_record_trace()) - trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str())); + for (auto const& transition : get_record_trace()) { + auto call_location = transition->get_call_location(); + if (not call_location.empty()) + trace.push_back(xbt::string_printf("Actor %ld in %s ==> simcall: %s", transition->aid_, call_location.c_str(), + transition->to_string().c_str())); + else + trace.push_back(xbt::string_printf("Actor %ld in simcall %s", transition->aid_, transition->to_string().c_str())); + } return trace; } diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp index 7779f6ec3d..6beb8af391 100644 --- a/src/mc/transition/Transition.hpp +++ b/src/mc/transition/Transition.hpp @@ -42,9 +42,8 @@ public: aid_t aid_ = 0; - /** The user function call that caused this transition to exist. - * Format is filename::function::line */ - std::string user_fun_call_ = ""; + /** The user function call that caused this transition to exist. Format: >>filename:line:function()<< */ + std::string call_location_ = ""; /* Which transition was executed for this simcall * @@ -68,6 +67,8 @@ public: /** Returns something like >>label = "desc", color = c<< to describe the transition in dot format */ virtual std::string dot_string() const; + std::string get_call_location() { return call_location_; } + /* Moves the application toward a path that was already explored, but don't change the current transition */ void replay(RemoteApp& app) const; diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp index 56c785bfd8..133f989a18 100644 --- a/src/mc/transition/TransitionComm.cpp +++ b/src/mc/transition/TransitionComm.cpp @@ -36,7 +36,7 @@ CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, std:: : Transition(Type::COMM_WAIT, issuer, times_considered) { xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> - user_fun_call_); + call_location_); XBT_DEBUG("CommWaitTransition %s comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR " size:%zu", (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_); @@ -84,7 +84,7 @@ CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsig CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::COMM_TEST, issuer, times_considered) { - xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> user_fun_call_); + xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> call_location_); XBT_DEBUG("CommTestTransition comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR " size:%zu", comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_); @@ -134,7 +134,7 @@ CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsig CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered) { - xbt_assert(stream >> comm_ >> mbox_ >> rbuff_ >> tag_ >> user_fun_call_); + xbt_assert(stream >> comm_ >> mbox_ >> rbuff_ >> tag_ >> call_location_); } std::string CommRecvTransition::to_string(bool verbose) const { @@ -208,7 +208,7 @@ CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsig CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered) { - xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_ >> user_fun_call_); + xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_ >> call_location_); XBT_DEBUG("SendTransition comm:%u mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_); } std::string CommSendTransition::to_string(bool verbose = false) const diff --git a/src/smpi/internals/smpi_replay.cpp b/src/smpi/internals/smpi_replay.cpp index a51870665f..701323fb28 100644 --- a/src/smpi/internals/smpi_replay.cpp +++ b/src/smpi/internals/smpi_replay.cpp @@ -564,7 +564,7 @@ void SleepAction::kernel(simgrid::xbt::ReplayAction&) void LocationAction::kernel(simgrid::xbt::ReplayAction&) { const LocationParser& args = get_args(); - smpi_trace_set_call_location(args.filename.c_str(), args.line, ""); + smpi_trace_set_call_location(args.filename.c_str(), args.line, "replay_action"); } void TestAction::kernel(simgrid::xbt::ReplayAction&) diff --git a/teshsuite/mc/random-bug/random-bug.tesh b/teshsuite/mc/random-bug/random-bug.tesh index 46ab37aa9d..109c9ff693 100644 --- a/teshsuite/mc/random-bug/random-bug.tesh +++ b/teshsuite/mc/random-bug/random-bug.tesh @@ -7,8 +7,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) Counter-example execution trace: -> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3) -> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4) +> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3) +> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4) > [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4' > [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall) @@ -22,8 +22,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) From signal: Aborted > [ 0.000000] (0:maestro@) Counter-example execution trace: -> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3) -> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4) +> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3) +> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4) > [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4' > [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall) > [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc @@ -45,8 +45,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/ > [ 0.000000] (0:maestro@) ************************** > [ 0.000000] (0:maestro@) From signal: Segmentation fault > [ 0.000000] (0:maestro@) Counter-example execution trace: -> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3) -> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4) +> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3) +> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4) > [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4' > [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall) > [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc -- 2.20.1