X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/19c58cbb49a4c58174169566b13aafb2b873fd81..614bd225f0d440c8285d735b2dbaf4090c04c838:/src/mc/mc_liveness.cpp

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index bce2296b7e..c9e84cd35f 100644
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -13,7 +13,6 @@
 #include <xbt/dynar.h>
 #include <xbt/fifo.h>
 #include <xbt/log.h>
-#include <xbt/parmap.h>
 #include <xbt/sysdep.h>
 
 #include "src/mc/mc_request.h"
@@ -22,6 +21,7 @@
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_smx.h"
 #include "src/mc/Client.hpp"
+#include "src/mc/mc_private.h"
 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_exit.h"
@@ -32,13 +32,14 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
 /********* Global variables *********/
 
 xbt_dynar_t acceptance_pairs;
-xbt_parmap_t parmap;
 
 /********* Static functions *********/
 
 namespace simgrid {
 namespace mc {
 
+static xbt_dynar_t visited_pairs;
+
 Pair::Pair() : num(++mc_stats->expanded_pairs),
   visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
 {}
@@ -48,6 +49,33 @@ Pair::~Pair() {
     MC_state_delete(this->graph_state, 1);
 }
 
+static  void show_stack_liveness(xbt_fifo_t stack)
+{
+  int value;
+  simgrid::mc::Pair* pair;
+  xbt_fifo_item_t item;
+  smx_simcall_t req;
+  char *req_str = nullptr;
+
+  for (item = xbt_fifo_get_last_item(stack);
+       item; item = xbt_fifo_get_prev_item(item)) {
+    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+    req = MC_state_get_executed_request(pair->graph_state, &value);
+    if (req && req->call != SIMCALL_NONE) {
+      req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
+      XBT_INFO("%s", req_str);
+      xbt_free(req_str);
+    }
+  }
+}
+
+static void dump_stack_liveness(xbt_fifo_t stack)
+{
+  simgrid::mc::Pair* pair;
+  while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
+    delete pair;
+}
+
 static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
 {
   unsigned int cursor = 0;
@@ -60,6 +88,15 @@ static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
   return std::move(values);
 }
 
+static int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->graph_state->system_state;
+  simgrid::mc::Snapshot* s2 = state2->graph_state->system_state;
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
+}
+
 static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
 {
   simgrid::mc::VisitedPair* new_pair = new VisitedPair(
@@ -76,7 +113,10 @@ static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* p
     simgrid::mc::VisitedPair* pair_test;
     int cursor;
 
-    index = get_search_interval(acceptance_pairs, new_pair, &min, &max);
+    index = simgrid::mc::get_search_interval(
+      (simgrid::mc::VisitedPair**) xbt_dynar_get_ptr(acceptance_pairs, 0),
+      xbt_dynar_length(acceptance_pairs),
+      new_pair, &min, &max);
 
     if (min != -1 && max != -1) {       // Acceptance pair with same number of processes and same heap bytes used exists
 
@@ -209,6 +249,163 @@ static void MC_pre_modelcheck_liveness(void)
   }
 }
 
+static void MC_replay_liveness(xbt_fifo_t stack)
+{
+  xbt_fifo_item_t item;
+  simgrid::mc::Pair* pair = nullptr;
+  mc_state_t state = nullptr;
+  smx_simcall_t req = nullptr, saved_req = NULL;
+  int value, depth = 1;
+  char *req_str;
+
+  XBT_DEBUG("**** Begin Replay ****");
+
+  /* Intermediate backtracking */
+  if(_sg_mc_checkpoint > 0) {
+    item = xbt_fifo_get_first_item(stack);
+    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+    if(pair->graph_state->system_state){
+      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+      return;
+    }
+  }
+
+  /* Restore the initial state */
+  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+
+    /* Traverse the stack from the initial state and re-execute the transitions */
+    for (item = xbt_fifo_get_last_item(stack);
+         item != xbt_fifo_get_first_item(stack);
+         item = xbt_fifo_get_prev_item(item)) {
+
+      pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+
+      state = (mc_state_t) pair->graph_state;
+
+      if (pair->exploration_started) {
+
+        saved_req = MC_state_get_executed_request(state, &value);
+
+        if (saved_req != nullptr) {
+          /* because we got a copy of the executed request, we have to fetch the
+             real one, pointed by the request field of the issuer process */
+          const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+          req = &issuer->simcall;
+
+          /* Debug information */
+          if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
+            req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }
+
+        }
+
+        simgrid::mc::handle_simcall(req, value);
+        mc_model_checker->wait_for_requests();
+      }
+
+      /* Update statistics */
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
+
+      depth++;
+
+    }
+
+  XBT_DEBUG("**** End Replay ****");
+}
+
+/**
+ * \brief Checks whether a given pair has already been visited by the algorithm.
+ */
+static
+int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+{
+  if (_sg_mc_visited == 0)
+    return -1;
+
+  simgrid::mc::VisitedPair* new_visited_pair = nullptr;
+  if (visited_pair == nullptr)
+    new_visited_pair = new simgrid::mc::VisitedPair(
+      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+      pair->graph_state);
+  else
+    new_visited_pair = visited_pair;
+
+  if (xbt_dynar_is_empty(visited_pairs)) {
+    xbt_dynar_push(visited_pairs, &new_visited_pair);
+    return -1;
+  }
+
+    int min = -1, max = -1, index;
+    //int res;
+    simgrid::mc::VisitedPair* pair_test;
+    int cursor;
+
+    index = get_search_interval(
+      (simgrid::mc::VisitedPair**) xbt_dynar_get_ptr(visited_pairs, 0),
+      xbt_dynar_length(visited_pairs), new_visited_pair, &min, &max);
+
+    if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
+      cursor = min;
+      while (cursor <= max) {
+        pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
+        if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+          if (xbt_automaton_propositional_symbols_compare_value(
+              pair_test->atomic_propositions.get(),
+              new_visited_pair->atomic_propositions.get()) == 0) {
+            if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+              if (pair_test->other_num == -1)
+                new_visited_pair->other_num = pair_test->num;
+              else
+                new_visited_pair->other_num = pair_test->other_num;
+              if (dot_output == nullptr)
+                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+              else
+                XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+              xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
+              xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
+              pair_test->visited_removed = 1;
+              if (!pair_test->acceptance_pair
+                  || pair_test->acceptance_removed == 1)
+                delete pair_test;
+              return new_visited_pair->other_num;
+            }
+          }
+        }
+        cursor++;
+      }
+      xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
+    } else {
+      pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
+      if (pair_test->nb_processes < new_visited_pair->nb_processes)
+        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
+      else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
+      else
+        xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
+    }
+
+    if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
+      int min2 = mc_stats->expanded_pairs;
+      unsigned int cursor2 = 0;
+      unsigned int index2 = 0;
+      xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
+        if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+            && pair_test->num < min2) {
+          index2 = cursor2;
+          min2 = pair_test->num;
+        }
+      }
+      xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
+      pair_test->visited_removed = 1;
+      if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+        delete pair_test;
+    }
+  return -1;
+}
+
 static int MC_modelcheck_liveness_main(void)
 {
   simgrid::mc::Pair* current_pair = nullptr;
@@ -375,8 +572,6 @@ static int MC_modelcheck_liveness_main(void)
 
 int modelcheck_liveness(void)
 {
-  if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
   MC_automaton_load(_sg_mc_property_file);
   mc_model_checker->wait_for_requests();