MC: more debug messages

diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
index b17f900..9ed6eb7 100644 (file)
--- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
+++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
@@ -18,21 +18,21 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker]  #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker]  #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=3)
+> [Checker]  #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker]  #1 BARRIER_WAIT(barrier: 0) (state=3)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=3)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker]  #1 BARRIER_WAIT(barrier: 0) (state=3)
+> [Checker]  #2 BARRIER_WAIT(barrier: 0) (state=4)
 > [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker]  #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker]  #2 BARRIER_WAIT(barrier: 0) (state=4)
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
 > [Checker] Execution came to an end at 1;2;1;2 (state: 5, depth: 5)
 > [Checker] Backtracking from 1;2;1;2
@@ -50,40 +50,40 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker]  #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker]  #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker]  #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker]  #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker]  #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker]  #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker]  #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker]  #1 BARRIER_WAIT(barrier: 0) (state=4)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=5)
+> [Checker]  #1 BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker]  #2 BARRIER_WAIT(barrier: 0) (state=5)
 > [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=5)
+> [Checker]  #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker]  #2 BARRIER_WAIT(barrier: 0) (state=5)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=5)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=6)
+> [Checker]  #2 BARRIER_WAIT(barrier: 0) (state=5)
+> [Checker]  #3 BARRIER_WAIT(barrier: 0) (state=6)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=6)
+> [Checker]  #1 BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker]  #3 BARRIER_WAIT(barrier: 0) (state=6)
 > [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=6)
+> [Checker]  #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker]  #3 BARRIER_WAIT(barrier: 0) (state=6)
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
 > [Checker] Execution came to an end at 1;2;3;1;2;3 (state: 7, depth: 7)
 > [Checker] Backtracking from 1;2;3;1;2;3
@@ -91,8 +91,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker]   <2,BARRIER_ASYNC_LOCK(barrier: 0)>
 > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker]  #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker]  #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
 > [Checker] 3 actors remain, but none of them need to be interleaved (depth 4).
 > [Checker] Backtracking from 1;3
 > [Checker] DFS exploration ended. 8 unique states visited; 1 backtracks (1 transition replays, 10 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 f7f1a55..5f726fe 100644 (file)
--- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
+++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
@@ -14,24 +14,24 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
+> [Checker]  #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker]  #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
+> [Checker]  #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
+> [Checker]  #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
+> [Checker]  #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
+> [Checker]  #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
+> [Checker]  #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker]  #2 MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
+> [Checker]  #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker]  #2 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
 > [Checker] Execution came to an end at 1;1;1;2;2;2 (state: 7, depth: 7)
 > [Checker] Backtracking from 1;1;1;2;2;2
@@ -39,11 +39,11 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker]   <1,MUTEX_UNLOCK(mutex: 0, owner: -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]  #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
+> [Checker]  #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
+> [Checker]  #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
+> [Checker]  #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
 > [Checker] 2 actors remain, but none of them need to be interleaved (depth 5).
 > [Checker] Backtracking from 1;1;2
 > [Checker] Sleep set actually containing:
@@ -52,28 +52,28 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 9, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
+> [Checker]  #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
+> [Checker]  #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 10, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 2) (state=10)
+> [Checker]  #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
+> [Checker]  #2 MUTEX_WAIT(mutex: 0, owner: 2) (state=10)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 11, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
+> [Checker]  #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
+> [Checker]  #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 12, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 1) (state=12)
+> [Checker]  #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
+> [Checker]  #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=12)
 > [Checker] Sleep set actually containing:
 > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 13, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=13)
+> [Checker]  #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
+> [Checker]  #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=13)
 > [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: 14, depth: 7)
 > [Checker] Backtracking from 2;1;2;2;1;1

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 451920d..8af6212 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -253,8 +253,10 @@ void DFSExplorer::run()
           continue;
         } else if (prev_state->get_transition_out()->depends(state->get_transition_out().get())) {
           XBT_VERB("Dependent Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
-          XBT_VERB("  %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
+          XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_,
+                   prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+          XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_,
+                   state->get_transition_out()->to_string().c_str(), state->get_num());
 
           if (prev_state->is_actor_enabled(issuer_id)) {
             if (not prev_state->is_actor_done(issuer_id)) {
@@ -273,8 +275,10 @@ void DFSExplorer::run()
           break;
         } else {
           XBT_VERB("INDEPENDENT Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
-          XBT_VERB("  %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
+          XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_,
+                   prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+          XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_,
+                   state->get_transition_out()->to_string().c_str(), state->get_num());
         }
         tmp_stack.pop_back();
       }

diff --git a/src/sthread/sthread_impl.cpp b/src/sthread/sthread_impl.cpp
index de2667b..9dbf789 100644 (file)
--- a/src/sthread/sthread_impl.cpp
+++ b/src/sthread/sthread_impl.cpp
@@ -275,6 +275,7 @@ int sthread_gettimeofday(struct timeval* tv)
 
 void sthread_sleep(double seconds)
 {
+  XBT_DEBUG("sleep(%lf)", seconds);
   simgrid::s4u::this_actor::sleep_for(seconds);
 }