Merge branch 'master' of https://framagit.org/simgrid/simgrid

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 47a5670..80e106c 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -124,7 +124,7 @@ if(NOT PERL_FOUND)
   message(FATAL_ERROR "Please install Perl to compile SimGrid.")
 endif()
 
-# tesh.py needs python 3 (or the module python-subprocess32 on python2.8+)
+# tesh.py needs python 3
 find_package(Python3 COMPONENTS Interpreter)
 if(NOT Python3_Interpreter_FOUND)
   message(FATAL_ERROR "Please install Python (version 3 or higher) to compile SimGrid.")

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index ee49e31..8d85325 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -8,8 +8,10 @@
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
+#include "src/mc/remote/mc_protocol.h"
 #include "src/mc/transition/Transition.hpp"
 
+#include "xbt/asserts.h"
 #include "xbt/log.h"
 #include "xbt/string.hpp"
 #include "xbt/sysdep.h"
@@ -136,29 +138,23 @@ void DFSExplorer::run()
     const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
                                                                : std::get<0>(state->next_transition_guided());
 
-    if (next < 0) {
-      // If there is no more transition in the current state ), backtrace
-      XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
-               stack_.size() + 1);
 
-      if (state->get_actor_count() == 0) {
-        get_remote_app().finalize_app();
-        XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
-                 state->get_num(), stack_.size());
+    if (next < 0 || not state->is_actor_enabled(next)) {
+      if (next >= 0) { // Actor is not enabled, then
+        XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
+                 to_c_str(reduction_mode_),
+                 state->get_actors_list().at(next).get_transition()->to_string(true).c_str());
+        if (reduction_mode_ == ReductionMode::odpor) {
+          XBT_INFO("Current trace:");
+          for (auto elm : get_textual_trace())
+            XBT_ERROR("%s", elm.c_str());
+         // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
+         state->remove_subtree_at_aid(next);
+         state->add_sleep_set(state->get_actors_list().at(next).get_transition());
+        }
       }
-
-      this->backtrack();
-      continue;
-    }
-    if (not state->is_actor_enabled(next)) {
-      // if ODPOR picked an actor that is not enabled -- ReversibleRace is an overapproximation
-      xbt_assert(reduction_mode_ == ReductionMode::odpor,
-                 "Only ODPOR should be fool enough to try to execute a disabled transition");
-      XBT_VERB("Preventing ODPOR exploration from executing a disabled transition. The reversibility of the race "
-               "must have been overapproximated");
-
-      state->remove_subtree_at_aid(next);
-      state->add_sleep_set(state->get_actors_list().at(next).get_transition());
+      // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled --
+      // ReversibleRace is an overapproximation), backtrace
       XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
                stack_.size() + 1);
 

diff --git a/teshsuite/mc/mcmini/barber_shop_deadlock.tesh b/teshsuite/mc/mcmini/barber_shop_deadlock.tesh
index e3420c9..d9d74a3 100644 (file)
--- a/teshsuite/mc/mcmini/barber_shop_deadlock.tesh
+++ b/teshsuite/mc/mcmini/barber_shop_deadlock.tesh
@@ -15,44 +15,44 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted)
 > [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted)
 > [0.000000] [mc_global/INFO] Counter-example execution trace:
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 1)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 1, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_UNLOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 3)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 3)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 3, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 2, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 2, capacity: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 1)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 0, capacity: 1, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_UNLOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, capacity: 2, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1, capacity: 3)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 3)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 0, capacity: 3, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_UNLOCK(semaphore: 1, capacity: 1)
 > [0.000000] [mc_global/INFO]   Actor 1 in simcall ActorJoin(target 3, no timeout)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 1)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 1, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_UNLOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 3)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 3)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 3, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 1, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 1, capacity: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 1)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 0, capacity: 1, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_UNLOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, capacity: 2, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1, capacity: 3)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 3)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 0, capacity: 3, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_UNLOCK(semaphore: 1, capacity: 1)
 > [0.000000] [mc_global/INFO]   Actor 1 in simcall ActorJoin(target 4, no timeout)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_WAIT(semaphore: 0, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 1)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_WAIT(semaphore: 1, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_UNLOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 3)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 3)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_WAIT(semaphore: 3, granted: yes)
-> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_WAIT(semaphore: 0, capacity: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 1)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_WAIT(semaphore: 0, capacity: 1, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_UNLOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, capacity: 2, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1, capacity: 3)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 2)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 3)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_WAIT(semaphore: 0, capacity: 3, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 5 in simcall SEM_UNLOCK(semaphore: 1, capacity: 1)
 > [0.000000] [mc_global/INFO]   Actor 1 in simcall ActorJoin(target 5, no timeout)
-> [0.000000] [mc_global/INFO]   Actor 6 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 7 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO]   Actor 6 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 7 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0)
 > [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;3;3;3;3;3;2;2;2;3;3;3;1;4;4;4;4;4;2;2;2;4;4;4;1;5;5;5;5;5;2;2;2;5;5;5;1;6;7'
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 40 unique states visited; 0 backtracks (0 transition replays, 40 states visited overall)
\ No newline at end of file

diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh
index e7a6750..9eb5b19 100644 (file)
--- a/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh
+++ b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh
@@ -14,17 +14,17 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4)
 > [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
 > [0.000000] [mc_global/INFO] Counter-example execution trace:
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 2, capacity: 0, granted: yes)
 > [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 SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 1, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 3 in simcall SEM_WAIT(semaphore: 1, capacity: 0, granted: yes)
 > [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 4 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 4 in simcall SEM_WAIT(semaphore: 0, capacity: 0, granted: yes)
 > [0.000000] [mc_global/INFO]   Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4)
 > [0.000000] [mc_global/INFO]   Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4)
 > [0.000000] [mc_global/INFO]   Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4)

diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh
index 84b5876..051f684 100644 (file)
--- a/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh
+++ b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh
@@ -4,4 +4,4 @@
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_ok 5 0
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor'
 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 4979 unique states visited; 119 backtracks (1022 transition replays, 6120 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 4979 unique states visited; 119 backtracks (1022 transition replays, 6120 states visited overall)

diff --git a/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh b/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh
index 0db5bb8..93b01c4 100644 (file)
--- a/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh
+++ b/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh
@@ -24,25 +24,25 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > [0.000000] [mc_global/INFO] Counter-example execution trace:
 > [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 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 2, capacity: 0, granted: yes)
 > [0.000000] [mc_global/INFO]   Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1, capacity: 1)
 > [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 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 1, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 1, capacity: 0, granted: yes)
 > [0.000000] [mc_global/INFO]   Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 2, capacity: 1)
 > [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 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_WAIT(semaphore: 0, capacity: 0, granted: yes)
 > [0.000000] [mc_global/INFO]   Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1)
-> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_UNLOCK(semaphore: 3, capacity: 1)
 > [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 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO]   Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0)
 > [0.000000] [mc_global/INFO]   Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
 > [0.000000] [mc_global/INFO]   Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
 > [0.000000] [mc_global/INFO]   Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
@@ -53,4 +53,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > [0.000000] [mc_global/INFO]   Actor 10 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
 > [0.000000] [mc_global/INFO]   Actor 11 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;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;3;4;5;6;7;8;9;10;11'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 31 unique states visited; 0 backtracks (0 transition replays, 31 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 31 unique states visited; 0 backtracks (0 transition replays, 31 states visited overall)
\ No newline at end of file

diff --git a/tools/tesh/tesh.py b/tools/tesh/tesh.py
index 856dab0..bf95860 100755 (executable)
--- a/tools/tesh/tesh.py
+++ b/tools/tesh/tesh.py
@@ -354,8 +354,8 @@ class Cmd:
         self.args += TeshState().args_suffix
 
         logs = list()
-        logs.append("[{file}:{number}] {args}".format(file=FileReader().filename,
-                                                      number=self.linenumber, args=self.args))
+        print("[{file}:{number}] {args}".format(file=FileReader().filename,
+                                                      number=self.linenumber, args=self.args), flush=True)
 
         args = shlex.split(self.args)