Change opened states for a priority queue

[simgrid.git] / src / mc / explo / DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 792383e..3afde70 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -43,7 +43,7 @@ void DFSExplorer::check_non_termination(const State* current_state)
 {
   for (auto const& state : stack_) {
     if (state->get_system_state()->equals_to(*current_state->get_system_state(),
-                                             get_remote_app().get_remote_process_memory())) {
+                                             *get_remote_app().get_remote_process_memory())) {
       XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
@@ -62,9 +62,15 @@ void DFSExplorer::check_non_termination(const State* current_state)
 }
 
 RecordTrace DFSExplorer::get_record_trace() // override
+{
+  return get_record_trace_of_stack(stack_);
+}
+
+/* Usefull to show debug information */
+RecordTrace DFSExplorer::get_record_trace_of_stack(stack_t stack)
 {
   RecordTrace res;
-  for (auto const& state : stack_)
+  for (auto const& state : stack)
     res.push_back(state->get_transition());
   return res;
 }
@@ -89,6 +95,18 @@ void DFSExplorer::log_state() // override
   Exploration::log_state();
 }
 
+/* Copy a given stack by deep-copying it at the State level : this is required so we can backtrack at different
+ * points without interacting with the stacks in the opened_states_ waiting for their turn. On the other hand,
+ * the exploration of one stack in opened_states_ could only slightly modify the sleep set of another stack in
+ * opened_states_, so it is only a slight waste of performance in the exploration. */
+void DFSExplorer::add_to_opened_states(stack_t stack)
+{
+  stack_t tmp_stack;
+  for (auto& state : stack)
+    tmp_stack.push_back(std::make_shared<State>(State(*state)));
+  opened_states_.emplace(tmp_stack);
+}
+
 void DFSExplorer::run()
 {
   on_exploration_start_signal(get_remote_app());
@@ -129,7 +147,7 @@ void DFSExplorer::run()
     }
 
     // Search for the next transition
-    // next_transition returns a pair<aid_t, double> in case we want to consider multiple state
+    // next_transition returns a pair<aid_t, double> in case we want to consider multiple state (eg. during backtrack)
     auto [next, _] = state->next_transition_guided();
 
     if (next < 0) { // If there is no more transition in the current state, backtrack.
@@ -196,15 +214,16 @@ void DFSExplorer::run()
           if (prev_state->is_actor_enabled(issuer_id)) {
             if (not prev_state->is_actor_done(issuer_id)) {
               prev_state->consider_one(issuer_id);
-              opened_states.emplace_back(tmp_stack);
+              add_to_opened_states(tmp_stack);
             } else
               XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
           } else {
             XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
                       "transition as todo",
                       issuer_id);
-            prev_state->consider_all();
-            opened_states.emplace_back(tmp_stack);
+            if (prev_state->consider_all() >
+                0) // If we ended up marking at least a transition, explore it at some point
+              add_to_opened_states(tmp_stack);
           }
           break;
         } else {
@@ -216,6 +235,11 @@ void DFSExplorer::run()
       }
     }
 
+    // Before leaving that state, if the transition we just took can be taken multiple times, we
+    // need to give it to the opened states
+    if (stack_.back()->count_todo_multiples() > 0)
+      add_to_opened_states(stack_);
+
     if (_sg_mc_termination)
       this->check_non_termination(next_state.get());
 
@@ -232,8 +256,8 @@ void DFSExplorer::run()
         stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required
       else {
         stack_.back()->consider_all();
-        opened_states.emplace_back(stack_);
       }
+
       dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
                  state->get_transition()->dot_string().c_str());
     } else
@@ -241,65 +265,46 @@ void DFSExplorer::run()
                  visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_,
                  state->get_transition()->dot_string().c_str());
   }
-
   log_state();
 }
 
 void DFSExplorer::backtrack()
 {
-  backtrack_count_++;
   XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
+  XBT_DEBUG("%lu alternatives are yet to be explored:", opened_states_.size());
+
   on_backtracking_signal(get_remote_app());
   get_remote_app().check_deadlock();
 
   // if no backtracking point, then set the stack_ to empty so we can end the exploration
-  if (opened_states.size() == 0) {
+  if (opened_states_.empty()) {
     stack_ = std::list<std::shared_ptr<State>>();
     return;
   }
 
-  /* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set.
-   * In the first case, we need to remove the last transition corresponding to the Finalize */
-  if (stack_.back()->get_transition()->aid_ == 0)
-    stack_.pop_back();
-
-  stack_t backtrack;
-  double min_dist = std::numeric_limits<double>::infinity();
-  aid_t min_aid   = -1;
-  for (auto& stack : opened_states) {
-    auto [aid, dist] = stack.back()->next_transition_guided();
-    if (aid == -1)
-      continue;
-    if (dist < min_dist) {
-      min_dist  = dist;
-      min_aid   = aid;
-      backtrack = stack;
-    }
-  }
+  stack_t backtrack = opened_states_.top(); // Take the point with smallest distance
+  opened_states_.pop();
 
-  if (min_aid == -1) {
-    stack_ = std::list<std::shared_ptr<State>>();
+  // if the smallest distance corresponded to no enable actor, remove this and let the
+  // exploration ask again for a backtrack
+  if (backtrack.back()->next_transition_guided().first == -1)
     return;
-  }
 
-  if (backtrack.back()->count_todo() <= 1)
-    opened_states.pop_back();
-  XBT_VERB("%lu todo actors in last states of the next backtracking point %s (remaining %lu opened stacks)",
-           backtrack.back()->count_todo(), backtrack.back()->get_transition()->to_string().c_str(),
-           opened_states.size());
+  // We found a real backtracking point, let's go to it
+  backtrack_count_++;
 
   /* If asked to rollback on a state that has a snapshot, restore it */
   State* last_state = backtrack.back().get();
   if (const auto* system_state = last_state->get_system_state()) {
-    system_state->restore(get_remote_app().get_remote_process_memory());
+    system_state->restore(*get_remote_app().get_remote_process_memory());
     on_restore_system_state_signal(last_state, get_remote_app());
+    stack_ = backtrack;
     return;
   }
 
   /* if no snapshot, we need to restore the initial state and replay the transitions */
   get_remote_app().restore_initial_state();
   on_restore_initial_state_signal(get_remote_app());
-
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (std::shared_ptr<State> const& state : backtrack) {
     if (state == backtrack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
@@ -309,10 +314,11 @@ void DFSExplorer::backtrack()
     visited_states_count_++;
   }
   stack_ = backtrack;
-  XBT_VERB(">> Backtracked to %s", get_record_trace().to_string().c_str());
+  XBT_DEBUG(">> Backtracked to %s", get_record_trace().to_string().c_str());
 }
 
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args)
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info)
+    : Exploration(args, need_memory_info || _sg_mc_termination)
 {
   if (with_dpor)
     reduction_mode_ = ReductionMode::dpor;
@@ -341,8 +347,9 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Explo
     stack_.back()->consider_best();
   else {
     stack_.back()->consider_all();
-    opened_states.emplace_back(stack_);
   }
+  if (stack_.back()->count_todo_multiples() > 1)
+    add_to_opened_states(stack_);
 }
 
 Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)