Test the dependencies of Mutex transitions

- give each mutex an ID so that we can get reproducible debug messages.
  This is arguably a waste of resource in non-MC setups. Patch welcome.
- give one mutex per pair of actors in the test, to make the test more
  interesting for the reduction
- rework a bit the verbose output of the safety explorer

diff --git a/MANIFEST.in b/MANIFEST.in
index c66a0b1..babfd77 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -365,6 +365,7 @@ include examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-
 include examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-variable-waituntil.tesh
 include examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable.cpp
 include examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable.tesh
+include examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
 include examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp
 include examples/cpp/synchro-mutex/s4u-synchro-mutex.tesh
 include examples/cpp/synchro-semaphore/s4u-synchro-semaphore.cpp

diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt
index 90e2b0f..5ff7e04 100644 (file)
--- a/examples/cpp/CMakeLists.txt
+++ b/examples/cpp/CMakeLists.txt
@@ -26,10 +26,6 @@ if(SIMGRID_HAVE_MC)
      set(_${example}_factories "^thread") # Timeout
      add_dependencies(tests-mc s4u-${example})
   endforeach()
-
-  # Make all MC tests buildable together
-  #foreach(example ) # no test to be build in any case
-  #endforeach()
   
   if(HAVE_C_STACK_CLEANER)
     add_executable       (s4u-mc-bugged1-liveness-cleaner-on  EXCLUDE_FROM_ALL s4u-mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp)
@@ -62,7 +58,6 @@ if(SIMGRID_HAVE_MC)
                        --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example}
                        --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
                        ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-mc-${example}.tesh)
-    set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-mc-${example}.tesh)
   endforeach()
 
 
@@ -95,6 +90,11 @@ else()
     set(_${example}_disable 1)
   endforeach()
 endif()
+# The tesh files of MC hijacked tests must always be added to the distribution
+foreach (example synchro-mutex)
+  set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-mc-${example}.tesh)
+endforeach()
+
 
 if(NOT HAVE_GRAPHVIZ)
   set(_dag-from-dot_disable 1)

diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
index 685e522..783e837 100644 (file)
--- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
+++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
@@ -1,11 +1,220 @@
 #!/usr/bin/env tesh
 
-$ ${bindir:=.}/../../../bin/simgrid-mc -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:1 --log=s4u_test.thres:critical
-> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '1'
-> [0.000000] [mc_safety/INFO] DFS exploration ended. 13 unique states visited; 3 backtracks (18 transition replays, 3 states visited overall)
+p This file tests the dependencies between MUTEX transitions
+
+$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
+> [Checker] Start a DFS exploration. Reduction is: dpor.
+> [App    ] Configuration change: Set 'actors' to '1'
+> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Execute 3: MUTEX_LOCK(mutex: 0, owner:3) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Execute 3: MUTEX_WAIT(mutex: 0, owner:3) (stack depth: 5, state: 5, 0 interleaves)
+> [Checker] Execute 3: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 6, 0 interleaves)
+> [Checker] Backtracking from 2;2;2;3;3;3;0
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=2)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:2) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker] Execute 3: MUTEX_LOCK(mutex: 0, owner:3) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:3) (stack depth: 2, state: 8, 0 interleaves)
+> [Checker] Execute 3: MUTEX_WAIT(mutex: 0, owner:3) (stack depth: 3, state: 9, 0 interleaves)
+> [Checker] Execute 3: MUTEX_UNLOCK(mutex: 0, owner:2) (stack depth: 4, state: 10, 0 interleaves)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 5, state: 11, 0 interleaves)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 12, 0 interleaves)
+> [Checker] Backtracking from 3;2;3;3;2;2;0
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:2) (state=10)
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=11)
+> [Checker] Backtracking from 3;2;3;3
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=8)
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:3) (state=9)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=8)
+> [Checker] DFS exploration ended. 13 unique states visited; 3 backtracks (18 transition replays, 3 states visited overall)
+
+$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors: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.
+> [App    ] Configuration change: Set 'actors' to '2'
+> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Execute 3: MUTEX_LOCK(mutex: 0, owner:3) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Execute 3: MUTEX_WAIT(mutex: 0, owner:3) (stack depth: 5, state: 5, 0 interleaves)
+> [Checker] Execute 3: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 6, 0 interleaves)
+> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 7, state: 7, 0 interleaves)
+> [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 8, state: 8, 0 interleaves)
+> [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 9, state: 9, 0 interleaves)
+> [Checker] Execute 5: MUTEX_LOCK(mutex: 1, owner:5) (stack depth: 10, state: 10, 0 interleaves)
+> [Checker] Execute 5: MUTEX_WAIT(mutex: 1, owner:5) (stack depth: 11, state: 11, 0 interleaves)
+> [Checker] Execute 5: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 12, 0 interleaves)
+> [Checker] Backtracking from 2;2;2;3;3;3;4;4;4;5;5;5;0
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 1, owner:-1) (state=9)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=10)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 1, owner:4) (state=8)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=10)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=10)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=6)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:3) (state=5)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=2)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:2) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=7)
+> [Checker] Execute 5: MUTEX_LOCK(mutex: 1, owner:5) (stack depth: 7, state: 7, 0 interleaves)
+> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:5) (stack depth: 8, state: 14, 0 interleaves)
+> [Checker] Execute 5: MUTEX_WAIT(mutex: 1, owner:5) (stack depth: 9, state: 15, 0 interleaves)
+> [Checker] Execute 5: MUTEX_UNLOCK(mutex: 1, owner:4) (stack depth: 10, state: 16, 0 interleaves)
+> [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 11, state: 17, 0 interleaves)
+> [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 18, 0 interleaves)
+> [Checker] Backtracking from 2;2;2;3;3;3;5;4;5;5;4;4;0
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 1, owner:4) (state=16)
+> [Checker]   MUTEX_WAIT(mutex: 1, owner:4) (state=17)
+> [Checker] Backtracking from 2;2;2;3;3;3;5;4;5;5
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=14)
+> [Checker]   MUTEX_WAIT(mutex: 1, owner:5) (state=15)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=14)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=6)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:3) (state=5)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=2)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:2) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=7)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=2)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:2) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=4)
+> [Checker] Execute 3: MUTEX_LOCK(mutex: 0, owner:3) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:3) (stack depth: 2, state: 20, 0 interleaves)
+> [Checker] Execute 3: MUTEX_WAIT(mutex: 0, owner:3) (stack depth: 3, state: 21, 0 interleaves)
+> [Checker] Execute 3: MUTEX_UNLOCK(mutex: 0, owner:2) (stack depth: 4, state: 22, 0 interleaves)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 5, state: 23, 0 interleaves)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 24, 0 interleaves)
+> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 7, state: 25, 0 interleaves)
+> [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 8, state: 26, 0 interleaves)
+> [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 9, state: 27, 0 interleaves)
+> [Checker] Execute 5: MUTEX_LOCK(mutex: 1, owner:5) (stack depth: 10, state: 28, 0 interleaves)
+> [Checker] Execute 5: MUTEX_WAIT(mutex: 1, owner:5) (stack depth: 11, state: 29, 0 interleaves)
+> [Checker] Execute 5: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 30, 0 interleaves)
+> [Checker] Backtracking from 3;2;3;3;2;2;4;4;4;5;5;5;0
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 1, owner:-1) (state=27)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=28)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 1, owner:4) (state=26)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=28)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=28)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=24)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=23)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:2) (state=22)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:3) (state=21)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=20)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:4) (state=25)
+> [Checker] Execute 5: MUTEX_LOCK(mutex: 1, owner:5) (stack depth: 7, state: 25, 0 interleaves)
+> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:5) (stack depth: 8, state: 32, 0 interleaves)
+> [Checker] Execute 5: MUTEX_WAIT(mutex: 1, owner:5) (stack depth: 9, state: 33, 0 interleaves)
+> [Checker] Execute 5: MUTEX_UNLOCK(mutex: 1, owner:4) (stack depth: 10, state: 34, 0 interleaves)
+> [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 11, state: 35, 0 interleaves)
+> [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 36, 0 interleaves)
+> [Checker] Backtracking from 3;2;3;3;2;2;5;4;5;5;4;4;0
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 1, owner:4) (state=34)
+> [Checker]   MUTEX_WAIT(mutex: 1, owner:4) (state=35)
+> [Checker] Backtracking from 3;2;3;3;2;2;5;4;5;5
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=32)
+> [Checker]   MUTEX_WAIT(mutex: 1, owner:5) (state=33)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=32)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:-1) (state=24)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=23)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:2) (state=22)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:3) (state=21)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=20)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 1, owner:5) (state=25)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner:2) (state=22)
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:2) (state=23)
+> [Checker] Backtracking from 3;2;3;3
+> [Checker] INDEPENDENT Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=20)
+> [Checker]   MUTEX_WAIT(mutex: 0, owner:3) (state=21)
+> [Checker] Dependent Transitions:
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=1)
+> [Checker]   MUTEX_LOCK(mutex: 0, owner:3) (state=20)
+> [Checker] DFS exploration ended. 37 unique states visited; 7 backtracks (76 transition replays, 33 states visited overall)
 
-$ ${bindir:=.}/../../../bin/simgrid-mc -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
+$ ${bindir:=.}/../../../bin/simgrid-mc -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical
 > [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
-> [0.000000] [mc_safety/INFO] DFS exploration ended. 241 unique states visited; 79 backtracks (744 transition replays, 425 states visited overall)
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '3'
+> [0.000000] [mc_safety/INFO] DFS exploration ended. 85 unique states visited; 15 backtracks (240 transition replays, 141 states visited overall)

diff --git a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp
index c73a6bc..9c7d4f6 100644 (file)
--- a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp
+++ b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp
@@ -5,6 +5,7 @@
 
 #include "simgrid/s4u.hpp" /* All of S4U */
 #include "xbt/config.hpp"
+namespace sg4 = simgrid::s4u;
 
 #include <mutex> /* std::mutex and std::lock_guard */
 
@@ -13,7 +14,7 @@ static simgrid::config::Flag<int> cfg_actor_count("actors", "How many pairs of a
 XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_test, "a sample log category");
 
 /* This worker uses a classical mutex */
-static void worker(simgrid::s4u::MutexPtr mutex, int& result)
+static void worker(sg4::MutexPtr mutex, int& result)
 {
   // lock the mutex before enter in the critical section
   mutex->lock();
@@ -28,11 +29,11 @@ static void worker(simgrid::s4u::MutexPtr mutex, int& result)
   mutex->unlock();
 }
 
-static void workerLockGuard(simgrid::s4u::MutexPtr mutex, int& result)
+static void workerLockGuard(sg4::MutexPtr mutex, int& result)
 {
   // Simply use the std::lock_guard like this
   // It's like a lock() that would do the unlock() automatically when getting out of scope
-  std::lock_guard<simgrid::s4u::Mutex> lock(*mutex);
+  std::lock_guard<sg4::Mutex> lock(*mutex);
 
   // then you are in a safe zone
   XBT_INFO("Hello s4u, I'm ready to compute after a lock_guard");
@@ -46,26 +47,22 @@ static void workerLockGuard(simgrid::s4u::MutexPtr mutex, int& result)
 static void master()
 {
   int result = 0;
-  simgrid::s4u::MutexPtr mutex = simgrid::s4u::Mutex::create();
-
-  for (int i = 0; i < cfg_actor_count * 2; i++) {
-    // To create a worker use the static method simgrid::s4u::Actor.
-    if((i % 2) == 0 )
-      simgrid::s4u::Actor::create("worker", simgrid::s4u::Host::by_name("Jupiter"), workerLockGuard, mutex,
-                                  std::ref(result));
-    else
-      simgrid::s4u::Actor::create("worker", simgrid::s4u::Host::by_name("Tremblay"), worker, mutex, std::ref(result));
+
+  for (int i = 0; i < cfg_actor_count; i++) {
+    sg4::MutexPtr mutex = sg4::Mutex::create();
+    sg4::Actor::create("worker", sg4::Host::by_name("Jupiter"), workerLockGuard, mutex, std::ref(result));
+    sg4::Actor::create("worker", sg4::Host::by_name("Tremblay"), worker, mutex, std::ref(result));
   }
 
-  simgrid::s4u::this_actor::sleep_for(10);
+  sg4::this_actor::sleep_for(10);
   XBT_INFO("Results is -> %d", result);
 }
 
 int main(int argc, char **argv)
 {
-  simgrid::s4u::Engine e(&argc, argv);
+  sg4::Engine e(&argc, argv);
   e.load_platform("../../platforms/two_hosts.xml");
-  simgrid::s4u::Actor::create("main", e.host_by_name("Tremblay"), master);
+  sg4::Actor::create("main", e.host_by_name("Tremblay"), master);
   e.run();
 
   return 0;

diff --git a/src/kernel/activity/MutexImpl.cpp b/src/kernel/activity/MutexImpl.cpp
index 8051a49..f1e089f 100644 (file)
--- a/src/kernel/activity/MutexImpl.cpp
+++ b/src/kernel/activity/MutexImpl.cpp
@@ -53,6 +53,8 @@ void MutexAcquisitionImpl::finish()
   simcall->issuer_->simcall_answer();
 }
 
+unsigned MutexImpl::next_id_ = 0;
+
 MutexAcquisitionImplPtr MutexImpl::lock_async(actor::ActorImpl* issuer)
 {
   auto res = MutexAcquisitionImplPtr(new kernel::activity::MutexAcquisitionImpl(issuer, this), true);

diff --git a/src/kernel/activity/MutexImpl.hpp b/src/kernel/activity/MutexImpl.hpp
index bbdef1c..5ab4b5d 100644 (file)
--- a/src/kernel/activity/MutexImpl.hpp
+++ b/src/kernel/activity/MutexImpl.hpp
@@ -68,17 +68,20 @@ class XBT_PUBLIC MutexImpl {
   actor::ActorImpl* owner_ = nullptr;
   // List of sleeping actors:
   std::deque<MutexAcquisitionImplPtr> sleeping_;
+  static unsigned next_id_;
+  unsigned id_;
 
   friend MutexAcquisitionImpl;
 
 public:
-  MutexImpl() : piface_(this) {}
+  MutexImpl() : piface_(this), id_(next_id_++) {}
   MutexImpl(MutexImpl const&) = delete;
   MutexImpl& operator=(MutexImpl const&) = delete;
 
   MutexAcquisitionImplPtr lock_async(actor::ActorImpl* issuer);
   bool try_lock(actor::ActorImpl* issuer);
   void unlock(actor::ActorImpl* issuer);
+  unsigned get_id() const { return id_; }
 
   MutexImpl* ref();
   void unref();

diff --git a/src/kernel/actor/MutexObserver.cpp b/src/kernel/actor/MutexObserver.cpp
index 33be57d..4c54def 100644 (file)
--- a/src/kernel/actor/MutexObserver.cpp
+++ b/src/kernel/actor/MutexObserver.cpp
@@ -25,7 +25,7 @@ MutexObserver::MutexObserver(ActorImpl* actor, mc::Transition::Type type, activi
 void MutexObserver::serialize(std::stringstream& stream) const
 {
   auto* owner = get_mutex()->get_owner();
-  stream << (short)type_ << ' ' << (uintptr_t)get_mutex() << ' ' << (owner != nullptr ? owner->get_pid() : -1);
+  stream << (short)type_ << ' ' << get_mutex()->get_id() << ' ' << (owner != nullptr ? owner->get_pid() : -1);
 }
 
 bool MutexObserver::is_enabled()

diff --git a/src/mc/explo/SafetyChecker.cpp b/src/mc/explo/SafetyChecker.cpp
index 5d173e1..144638b 100644 (file)
--- a/src/mc/explo/SafetyChecker.cpp
+++ b/src/mc/explo/SafetyChecker.cpp
@@ -97,8 +97,7 @@ void SafetyChecker::run()
     State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_VERB("Exploration depth=%zu (state=%p, num %ld)(%zu interleave)", stack_.size(), state, state->num_,
-             state->count_todo());
+    XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->num_, state->count_todo());
 
     api::get().mc_inc_visited_states();
 
@@ -143,7 +142,8 @@ void SafetyChecker::run()
 
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
-    XBT_DEBUG("Execute: %s", state->get_transition()->to_string().c_str());
+    XBT_VERB("Execute %ld: %.60s (stack depth: %ld, state: %zu, %zu interleaves)", state->get_transition()->aid_,
+             state->get_transition()->to_string().c_str(), stack_.size(), state->num_, state->count_todo());
 
     std::string req_str;
     if (dot_output != nullptr)

diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp
index 98710f8..88c27ce 100644 (file)
--- a/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@ -16,7 +16,7 @@ namespace simgrid {
 namespace mc {
 std::string MutexTransition::to_string(bool verbose) const
 {
-  return xbt::string_printf("%s(%" PRIxPTR ", owner:%ld)", Transition::to_c_str(type_), mutex_, owner_);
+  return xbt::string_printf("%s(mutex: %" PRIxPTR ", owner:%ld)", Transition::to_c_str(type_), mutex_, owner_);
 }
 
 MutexTransition::MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)