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

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index afd8904..b5929f3 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -25,7 +25,6 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
 {
   XBT_VERB("Creating a guide for the state");
 
-  
   if (_sg_mc_strategy == "none")
     strategy_ = std::make_shared<BasicStrategy>();
   else if (_sg_mc_strategy == "max_match_comm")
@@ -33,10 +32,9 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
   else if (_sg_mc_strategy == "min_match_comm")
     strategy_ = std::make_shared<MinMatchComm>();
   else if (_sg_mc_strategy == "uniform") {
-    xbt::random::set_mersenne_seed(_sg_mc_random_seed);  
+    xbt::random::set_mersenne_seed(_sg_mc_random_seed);
     strategy_ = std::make_shared<UniformStrategy>();
-  }
-  else
+  } else
     THROW_IMPOSSIBLE;
 
   remote_app.get_actors_status(strategy_->actors_to_run_);
@@ -51,7 +49,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
     strategy_ = std::make_shared<MaxMatchComm>();
   else if (_sg_mc_strategy == "min_match_comm")
     strategy_ = std::make_shared<MinMatchComm>();
-  else if (_sg_mc_strategy == "uniform") 
+  else if (_sg_mc_strategy == "uniform")
     strategy_ = std::make_shared<UniformStrategy>();
   else
     THROW_IMPOSSIBLE;
@@ -201,6 +199,9 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
 {
   // TODO: It would be better not to have such a flag.
   if (has_initialized_wakeup_tree) {
+    XBT_DEBUG("Reached a node with the following initialized WuT:");
+    XBT_DEBUG("\n%s", wakeup_tree_.string_of_whole_tree().c_str());
+
     return;
   }
   // TODO: Note that the next action taken by the actor may be updated
@@ -225,6 +226,11 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
 
 void State::sprout_tree_from_parent_state()
 {
+
+    XBT_DEBUG("Initializing Wut with parent one:");
+    XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
+
+    
   xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
                                        "(or what appears to be, rather for state without a parent defined)");
   const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node();

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index ca77b51..de11f78 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -144,7 +144,9 @@ public:
    */
   void remove_subtree_using_current_out_transition();
   bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+  std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); }
 
+  
   /**
    * @brief
    */

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 978cdfd..033c525 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -81,7 +81,7 @@ void DFSExplorer::log_state() // override
   XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states "
            "visited overall)",
            State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(),
-          visited_states_count_);
+           visited_states_count_);
   Exploration::log_state();
 }
 
@@ -335,6 +335,8 @@ std::shared_ptr<State> DFSExplorer::next_odpor_state()
     for (const auto& [aid, transition] : state->get_sleep_set())
       XBT_DEBUG("\t  <%ld,%s>", aid, transition->to_string().c_str());
     if (not state->has_empty_tree()) {
+       XBT_DEBUG("\t    found the following non-empty WuT:\n"
+                 "%s", state->string_of_wut().c_str());
       return state;
     }
   }
@@ -354,15 +356,19 @@ void DFSExplorer::backtrack()
      * ("eventually looks like C", viz. the `~_E` relation)
      */
     for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
-      for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+       XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
+       for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
         XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
         State& prev_state = *stack_[e];
         if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
           switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
             case odpor::WakeupTree::InsertionResult::root: {
-              XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
-                        "the execution prior to event `%u`:",
-                        e_prime, e);
+              XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for "
+                        "the execution prior to event `%u`(%ld: %.20s):",
+                        e_prime, stack_[e_prime]->get_transition_out()->aid_,
+                        stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e,
+                        prev_state.get_transition_out()->aid_,
+                        prev_state.get_transition_out()->to_string(true).c_str());
               break;
             }
             case odpor::WakeupTree::InsertionResult::interior_node: {

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index 162425d..8b531ff 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -12,6 +12,8 @@
 #include <limits>
 #include <vector>
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
 namespace simgrid::mc::odpor {
 
 std::vector<std::string> get_textual_trace(const PartialExecution& w)
@@ -64,18 +66,22 @@ std::vector<std::string> Execution::get_textual_trace() const
 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
 {
   std::unordered_set<Execution::EventHandle> racing_events;
+  // This keep tracks of events that happens-before the target
   std::unordered_set<Execution::EventHandle> disqualified_events;
 
   // For each event of the execution
   for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
     // We need `e_i -->_E target` as a necessary condition
     if (not happens_before(e_i, target)) {
+      XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target);
       continue;
     }
 
     // Further, `proc(e_i) != proc(target)`
     if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
       disqualified_events.insert(e_i);
+      XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i,
+                target);
       continue;
     }
 
@@ -87,6 +93,8 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
       // then e_i --->_E target indirectly (either through
       // e_j directly, or transitively through e_j)
       if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
+        XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)",
+                  target, e_i, e_j, e_i, e_j, target);
         disqualified_events.insert(e_i);
         break;
       }
@@ -98,6 +106,9 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
     // it (since this would transitively make it the event
     // which "happens-between" `target` and `e`)
     if (disqualified_events.count(e_i) == 0) {
+       XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event",
+                  target, e_i);
+        disqualified_events.insert(e_i);
       racing_events.insert(e_i);
       disqualified_events.insert(e_i);
     }

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index d671e93..9b8f614 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -13,8 +13,18 @@
 #include <xbt/asserts.h>
 #include <xbt/ex.h>
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
 namespace simgrid::mc::odpor {
 
+/**
+   The reversible race detector should only be used if we already have the assumption
+   e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that :
+   - e1 -->_E e2
+   - proc(e1) != proc(e2)
+   - there is no event e3 s.t. e1 --> e3 --> e2
+*/
+
 bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
                                                   Execution::EventHandle e2)
 {
@@ -143,8 +153,12 @@ bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&,
 bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
                                                             const Transition* /*e2*/)
 {
-  // TODO: Get the semantics correct here
+  // The only possibilities for e1 to satisfy the pre-condition are :
+    // - MUTEX_ASYNC_LOCK
+
+  
   const auto e1_action = E.get_transition_for_handle(e1)->type_;
+  xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK);
   return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
 }
 

diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp
index 27d914a..f7e0ea6 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.cpp
+++ b/src/mc/explo/odpor/WakeupTree.cpp
@@ -13,6 +13,9 @@
 #include <memory>
 #include <queue>
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_wut, mc, "Logging specific to ODPOR WakeupTrees");
+
+
 namespace simgrid::mc::odpor {
 
 void WakeupTreeNode::add_child(WakeupTreeNode* node)
@@ -21,6 +24,18 @@ void WakeupTreeNode::add_child(WakeupTreeNode* node)
   node->parent_ = this;
 }
 
+std::string WakeupTreeNode::string_of_whole_tree(int indentation_level) const
+{
+  std::string tabulations = "";
+  for (int i = 0; i < indentation_level; i++)
+    tabulations += "  ";
+  std::string final_string = action_ == nullptr ? "<>\n" :
+      tabulations + "Actor " + std::to_string(action_->aid_) + ": " + action_->to_string(true) + "\n";
+  for (auto node : children_)
+    final_string += node->string_of_whole_tree(indentation_level + 1);
+  return final_string;
+}
+
 PartialExecution WakeupTreeNode::get_sequence() const
 {
   // TODO: Prevent having to compute this at the node level
@@ -85,6 +100,11 @@ std::optional<WakeupTreeNode*> WakeupTree::get_min_single_process_node() const
   return this->root_->children_.front();
 }
 
+std::string WakeupTree::string_of_whole_tree() const
+{
+  return root_->string_of_whole_tree(0);
+}
+
 WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
 {
   // Perform a BFS search to perform a deep copy of the portion

diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp
index 8247a91..b4502f4 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.hpp
+++ b/src/mc/explo/odpor/WakeupTree.hpp
@@ -72,6 +72,8 @@ public:
   std::shared_ptr<Transition> get_action() const { return action_; }
   const std::list<WakeupTreeNode*>& get_ordered_children() const { return children_; }
 
+  std::string string_of_whole_tree(int indentation_level) const;
+
   /** Insert a node `node` as a new child of this node */
   void add_child(WakeupTreeNode* node);
 };
@@ -152,6 +154,8 @@ public:
 
   std::vector<std::string> get_single_process_texts() const;
 
+  std::string string_of_whole_tree() const;
+
   /**
    * @brief Remove the subtree of the smallest (with respect
    * to the tree's "<" relation) single-process node.

diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp
index 3ea33cc..48e0617 100644 (file)
--- a/src/mc/transition/TransitionAny.cpp
+++ b/src/mc/transition/TransitionAny.cpp
@@ -59,7 +59,7 @@ std::string WaitAnyTransition::to_string(bool verbose) const
   auto res = xbt::string_printf("WaitAny{ ");
   for (auto const* t : transitions_)
     res += t->to_string(verbose);
-  res += " }";
+  res += " } (times considered = " + std::to_string(times_considered_) + ")";
   return res;
 }
 bool WaitAnyTransition::depends(const Transition* other) const