From 2e20b9d63d8a9ca26f8b508b5cab294acc3b608a Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 24 Feb 2022 13:46:20 +0100 Subject: [PATCH] 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 --- MANIFEST.in | 1 + examples/cpp/CMakeLists.txt | 10 +- .../synchro-mutex/s4u-mc-synchro-mutex.tesh | 223 +++++++++++++++++- .../cpp/synchro-mutex/s4u-synchro-mutex.cpp | 27 +-- src/kernel/activity/MutexImpl.cpp | 2 + src/kernel/activity/MutexImpl.hpp | 5 +- src/kernel/actor/MutexObserver.cpp | 2 +- src/mc/explo/SafetyChecker.cpp | 6 +- src/mc/transition/TransitionSynchro.cpp | 2 +- 9 files changed, 245 insertions(+), 33 deletions(-) diff --git a/MANIFEST.in b/MANIFEST.in index c66a0b18c1..babfd7718b 100644 --- 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 90e2b0f783..5ff7e042f0 100644 --- 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 685e522646..783e8373d5 100644 --- 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 c73a6bcfdb..9c7d4f6754 100644 --- 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 /* std::mutex and std::lock_guard */ @@ -13,7 +14,7 @@ static simgrid::config::Flag 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 lock(*mutex); + std::lock_guard 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 8051a4910e..f1e089fbc5 100644 --- 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 bbdef1cd9f..5ab4b5d21d 100644 --- 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 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 33be57db42..4c54def39e 100644 --- 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 5d173e1aa8..144638b4f0 100644 --- 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 98710f84e4..88c27ce083 100644 --- 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) -- 2.20.1