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

diff --git a/.mailmap b/.mailmap
index 5efced4..2e99416 100644 (file)
--- a/.mailmap
+++ b/.mailmap
@@ -77,6 +77,7 @@ Arnaud Giersch <arnaud.giersch@univ-fcomte.fr> <arnaud.giersch@iut-bm.univ-fcomt
 Julien Gossa <julien.gossa@unistra.fr> <gossa@unistra.fr>
 Adrien Gougeon <adrien.gougeon@inria.fr>
 Adrien Gougeon <adrien.gougeon@inria.fr> <adrien.gougeon@ens-rennes.fr>
+Alexander Grund <git@grundis.de>
 Loic Guegan <manzerbredes@mailbox.org> <manzerberdes@gmx.com>
 Marion Guthmuller <marion.guthmuller@inria.fr> <marion.guthmuller@loria.fr>
 Ahmed Harbaoui <amad206@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
@@ -153,5 +154,5 @@ Pedro Velho <pedro.velho@gmail.com> <velho@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
 Pedro Velho <pedro.velho@gmail.com> <velho@mohave.(none)>
 Flavien Vernier <vernier@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
 Matthieu Volat <matthieu.volat@univ-lyon1.fr> <mazhe@alkumuna.eu>
-Steven Whatelse <stevenwhatelse@hotmail.fr>
+Steven Quinito Masnada <stevenwhatelse@hotmail.fr>
 Chidambar Zinnoury <illogict@48e7efb5-ca39-0410-a469-dd3cf9ba447f>

diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh
index 3c2eee5..2ec84f7 100644 (file)
--- a/examples/sthread/pthread-mc-producer-consumer.tesh
+++ b/examples/sthread/pthread-mc-producer-consumer.tesh
@@ -3,14 +3,14 @@
 
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q  -C 1 -P 1
 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 786 unique states visited; 97 backtracks (2049 transition replays, 2932 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 203 unique states visited; 23 backtracks (396 transition replays, 622 states visited overall)
 
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:sdpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q  -C 1 -P 1
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'sdpor'
 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: sdpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1186 unique states visited; 157 backtracks (3403 transition replays, 4746 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 347 unique states visited; 45 backtracks (736 transition replays, 1128 states visited overall)
 
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q  -C 1 -P 1
 > [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. 617 unique states visited; 29 backtracks (524 transition replays, 1170 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 133 unique states visited; 4 backtracks (58 transition replays, 195 states visited overall)
\ No newline at end of file

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index ba6f7ba..42ff35e 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -278,6 +278,9 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
       E_prime_v.push_transition(get_event_with_handle(e_star).get_transition());
       v.push_back(get_event_with_handle(e_star).get_transition());
 
+      XBT_DEBUG("Added Event `%u` (%ld:%s) to the construction of v", e_star, get_actor_with_handle(e_star),
+                get_event_with_handle(e_star).get_transition()->to_string().c_str());
+
       const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
 
       // When checking whether any event in `dom_[E'](v)` happens before
@@ -315,6 +318,9 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
         // relation orders actions taken by each actor
         disqualified_actors.insert(q);
       }
+    } else {
+      XBT_DEBUG("Event `%u` (%ld:%s) dismissed from the construction of v", e_star, get_actor_with_handle(e_star),
+                get_event_with_handle(e_star).get_transition()->to_string().c_str());
     }
   }
 

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index d35c167..575d8e0 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -156,9 +156,10 @@ bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&,
 bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, const Transition* /*other_transition*/,
                                                             const Transition* /*t2*/)
 {
-  // TODO: for now we over approximate the reversibility
-
-  return true;
+  // Only an Unlock can be dependent with a Wait
+  // and in this case, the Unlock enbaled the wait
+  // Not reversibled
+  return false;
 }
 
 bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, const Transition* /*other_transition*/,

diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp
index 230308f..b1bea23 100644 (file)
--- a/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@ -88,6 +88,12 @@ bool MutexTransition::depends(const Transition* o) const
     if (type_ == Type::MUTEX_ASYNC_LOCK && other->type_ == Type::MUTEX_UNLOCK)
       return false;
 
+    // Theorem 4.4.9: LOCK indep UNLOCK.
+    //  any combination of wait and test is indenpendent.
+    if ((type_ == Type::MUTEX_WAIT || type_ == Type::MUTEX_TEST) &&
+        (other->type_ == Type::MUTEX_WAIT || other->type_ == Type::MUTEX_TEST))
+      return false;
+
     // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
     // request is queued)
     if (type_ == Type::MUTEX_TEST &&