Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of framagit.org:simgrid/simgrid
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 12 Nov 2023 14:01:06 +0000 (15:01 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 12 Nov 2023 14:01:06 +0000 (15:01 +0100)
src/mc/explo/odpor/ReversibleRaceCalculator.cpp
src/mc/explo/odpor/ReversibleRaceCalculator.hpp
tools/tesh/IO-orders.tesh
tools/tesh/set-output-sort.tesh
tools/tesh/tesh.py

index 5fcb30e..575d8e0 100644 (file)
@@ -29,7 +29,7 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
                                                   Execution::EventHandle e2)
 {
   using Action     = Transition::Type;
-  using Handler    = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
+  using Handler    = std::function<bool(const Execution&, const Transition*, const Transition*)>;
   using HandlerMap = std::unordered_map<Action, Handler>;
 
   const static HandlerMap handlers = {
@@ -53,9 +53,10 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
       {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
       {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
 
-  const auto* e2_action = E.get_transition_for_handle(e2);
-  if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
-    return handler->second(E, e1, e2_action);
+  const auto* other_transition = E.get_transition_for_handle(e1);
+  const auto* t2 = E.get_transition_for_handle(e2);
+  if (const auto handler = handlers.find(t2->type_); handler != handlers.end()) {
+    return handler->second(E, other_transition, t2);
   } else {
     xbt_die("There is currently no specialized computation for the transition "
             "'%s' for computing reversible races in ODPOR, so the model checker cannot "
@@ -63,12 +64,12 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
             "that the transition be supported in SimGrid using ODPPR and consider "
             "using the other model-checking algorithms supported by SimGrid instead "
             "in the meantime",
-            e2_action->to_string().c_str());
+            t2->to_string().c_str());
   }
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle /*e1*/,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // ActorJoin races with another event iff its target `T` is the same as
   // the actor executing the other transition. Clearly, then, we could not join
@@ -76,82 +77,84 @@ bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Ex
   return false;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
-                                                                   const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&,
+                                                                   const Transition* /*other_transition*/,
+                                                                   const Transition* /*t2*/)
 {
   // BarrierAsyncLock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
-                                                              const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, const Transition* other_transition,
+                                                              const Transition* /*t2*/)
 {
   // If the other event is a barrier lock event, then we
   // are not reversible; otherwise we are reversible.
-  const auto e1_action = E.get_transition_for_handle(e1)->type_;
-  return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
+  const auto other_action = other_transition->type_;
+  return other_action != Transition::Type::BARRIER_ASYNC_LOCK;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle /*e1*/,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, const Transition* /*other_transition*/,
+                                                           const Transition* /*t2*/)
 {
   // CommRecv is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle /*e1*/,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, const Transition* /*other_transition*/,
+                                                           const Transition* /*t2*/)
 {
   // CommSend is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, const Transition* other_transition,
+                                                           const Transition* /*t2*/)
 {
   // If the other event is a communication event, then we
   // are not reversible; otherwise we are reversible.
-  const auto e1_action = E.get_transition_for_handle(e1)->type_;
-  return e1_action != Transition::Type::COMM_ASYNC_SEND && e1_action != Transition::Type::COMM_ASYNC_RECV;
+  const auto other_action = other_transition->type_;
+  return other_action != Transition::Type::COMM_ASYNC_SEND && other_action != Transition::Type::COMM_ASYNC_RECV;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle /*e1*/,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, const Transition* /*other_transition*/,
+                                                           const Transition* /*t2*/)
 {
   // CommTest is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
-                                                                 const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&,
+                                                                 const Transition* /*other_transition*/,
+                                                                 const Transition* /*t2*/)
 {
   // MutexAsyncLock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle /*e1*/,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // MutexTest is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle /*e1*/,
-                                                               const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, const Transition* /*other_transition*/,
+                                                               const Transition* /*t2*/)
 {
   // MutexTrylock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle /*e1*/,
-                                                              const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, const Transition* /*other_transition*/,
+                                                              const Transition* /*t2*/)
 {
   // MutexUnlock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // Only an Unlock can be dependent with a Wait
   // and in this case, the Unlock enbaled the wait
@@ -159,56 +162,55 @@ bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E,
   return false;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
-                                                               const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, const Transition* /*other_transition*/,
+                                                               const Transition* /*t2*/)
 {
   // SemAsyncLock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle /*e1*/,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // SemUnlock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
-                                                          const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, const Transition* other_transition,
+                                                          const Transition* /*t2*/)
 {
 
-  const auto e1_transition = E.get_transition_for_handle(e1);
-  if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
-      static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1) {
+  if (other_transition->type_ == Transition::Type::SEM_UNLOCK &&
+      static_cast<const SemaphoreTransition*>(other_transition)->get_capacity() <= 1) {
     return false;
   }
-  xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
+  xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,
-                                                               const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, const Transition* /*other_transition*/,
+                                                               const Transition* /*t2*/)
 {
   // Object access is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle /*e1*/,
-                                                         const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, const Transition* /*other_transition*/,
+                                                         const Transition* /*t2*/)
 {
   // Random is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle /*e1*/,
-                                                          const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, const Transition* /*other_transition*/,
+                                                          const Transition* /*t2*/)
 {
   // TestAny is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle /*e1*/,
-                                                          const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, const Transition* /*other_transition*/,
+                                                          const Transition* /*t2*/)
 {
   // TODO: We need to check if any of the transitions
   // waited on occurred before `e1`
index 88c6839..1c67814 100644 (file)
@@ -30,25 +30,25 @@ namespace simgrid::mc::odpor {
  * is only sensible in the context of a race
  */
 class ReversibleRaceCalculator final {
-  static bool is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_BarrierWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_Random(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1, const Transition* e2);
+  static bool is_race_reversible_ActorJoin(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_BarrierAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_BarrierWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommRecv(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommSend(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommTest(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexTest(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexTrylock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexUnlock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_SemAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_SemUnlock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_SemWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_ObjectAccess(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_Random(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_TestAny(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_WaitAny(const Execution&, const Transition* t1, const Transition* t2);
 
 public:
   static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);
index e2c0a25..c7bbc67 100644 (file)
@@ -7,6 +7,7 @@ p Order: in, out, cmd
 < $ cat
 > Test suite from stdin
 > [(stdin):3] cat
+> 
 > Test suite from stdin OK
 $ ${bindir:=.}/tesh
 
@@ -16,6 +17,7 @@ p Order: out, in, cmd
 < $ cat
 > Test suite from stdin
 > [(stdin):3] cat
+> 
 > Test suite from stdin OK
 $ ${bindir:=.}/tesh
 
@@ -25,6 +27,7 @@ p Order: out, cmd, in
 < < TOTO
 > Test suite from stdin
 > [(stdin):2] cat
+> 
 > Test suite from stdin OK
 $ ${bindir:=.}/tesh
 
@@ -34,6 +37,7 @@ p Order: in, cmd, out
 < > TOTO
 > Test suite from stdin
 > [(stdin):2] cat
+> 
 > Test suite from stdin OK
 $ ${bindir:=.}/tesh
 
@@ -43,6 +47,7 @@ p Order: cmd, out, in
 < < TOTO
 > Test suite from stdin
 > [(stdin):1] cat
+> 
 > Test suite from stdin OK
 $ ${bindir:=.}/tesh
 
@@ -52,5 +57,6 @@ p Order: cmd, in, out
 < > TOTO
 > Test suite from stdin
 > [(stdin):1] cat
+> 
 > Test suite from stdin OK
 $ ${bindir:=.}/tesh
index e560f56..92b3400 100644 (file)
@@ -75,19 +75,33 @@ $ ${bindir:=.}/tesh --ignore-jenkins
 > Test suite from stdin
 > [(stdin):1] Test sorting and filtering of output
 > [(stdin):3] true
+> 
 > [(stdin):6] true
+> 
 > [(stdin):8] printf 'profiling: foo\n'
+> 
 > [(stdin):10] printf 'profiling: foo'
+> 
 > [(stdin):13] printf 'profiling: foo\n'
+> 
 > [(stdin):16] printf 'profiling: foo'
+> 
 > [(stdin):18] printf 'a\nb\nc\nd\n'
+> 
 > [(stdin):24] printf 'a\nb\nc\nd'
+> 
 > [(stdin):31] printf 'c\nd\nb\na\n'
+> 
 > [(stdin):38] printf 'c\nd\nb\na'
+> 
 > [(stdin):44] printf 'a\nprofiling: foo\nprofiling: bar\nb\nc\nd\nprofiling: baz\n'
+> 
 > [(stdin):50] printf 'a\nprofiling: foo\nprofiling: bar\nb\nc\nd\nprofiling: baz'
+> 
 > [(stdin):57] printf 'c\nprofiling: foo\nprofiling: bar\nd\nb\na\nprofiling: baz\n'
+> 
 > [(stdin):64] printf 'c\nprofiling: foo\nprofiling: bar\nd\nb\na\nprofiling: baz'
+> 
 > Test suite from stdin OK
 
 p Check the Right Prefix Length (19) for "output sort"
index bf95860..a1375b9 100755 (executable)
@@ -354,8 +354,11 @@ class Cmd:
         self.args += TeshState().args_suffix
 
         logs = list()
-        print("[{file}:{number}] {args}".format(file=FileReader().filename,
-                                                      number=self.linenumber, args=self.args), flush=True)
+        msg = "[{file}:{number}] {args}".format(file=FileReader().filename, number=self.linenumber, args=self.args)
+        if self.background:
+            logs.append(msg)
+        else:
+            print(msg, flush=True)
 
         args = shlex.split(self.args)