X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/269fcd3a8b8e4ae311a99640e3993bdc30b98a5b..d0e460f14e1b5d882a2928eb754f95659bb12857:/src/mc/mc_liveness.cpp?ds=sidebyside

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 718fe43bb1..862eb6ae51 100644
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -6,14 +6,16 @@
 
 #include <cstring>
 
+#include <algorithm>
+
 #include <unistd.h>
 #include <sys/wait.h>
 
 #include <xbt/automaton.h>
 #include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
 #include <xbt/fifo.h>
 #include <xbt/log.h>
-#include <xbt/parmap.h>
 #include <xbt/sysdep.h>
 
 #include "src/mc/mc_request.h"
@@ -21,28 +23,26 @@
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/mc_client.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"
 
-extern "C" {
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
-}
-
 /********* 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)
 {}
@@ -52,6 +52,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;
@@ -64,57 +91,47 @@ 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)
 {
+  auto acceptance_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(::acceptance_pairs);
+
   simgrid::mc::VisitedPair* new_pair = new VisitedPair(
     pair->num, pair->automaton_state, pair->atomic_propositions.get(),
     pair->graph_state);
   new_pair->acceptance_pair = 1;
 
-  if (xbt_dynar_is_empty(acceptance_pairs))
-    xbt_dynar_push(acceptance_pairs, &new_pair);
-  else {
-
-    int min = -1, max = -1, index;
-    //int res;
-    simgrid::mc::VisitedPair* pair_test;
-    int cursor;
-
-    index = get_search_interval(acceptance_pairs, new_pair, &min, &max);
-
-    if (min != -1 && max != -1) {       // Acceptance pair with same number of processes and same heap bytes used exists
-
-      cursor = min;
-      if(pair->search_cycle == 1){
-        while (cursor <= max) {
-          pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, cursor, simgrid::mc::VisitedPair*);
-          if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
-            if (xbt_automaton_propositional_symbols_compare_value(
-                pair_test->atomic_propositions.get(),
-                new_pair->atomic_propositions.get()) == 0) {
-              if (snapshot_compare(pair_test, new_pair) == 0) {
-                XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
-                xbt_fifo_shift(mc_stack);
-                if (dot_output != nullptr)
-                  fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
-                return nullptr;
-              }
-            }
+  auto res = std::equal_range(acceptance_pairs.begin(), acceptance_pairs.end(),
+    new_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+  if (pair->search_cycle == 1)
+    for (auto i = res.first; i != res.second; ++i) {
+      simgrid::mc::VisitedPair* pair_test = *i;
+      if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
+        if (xbt_automaton_propositional_symbols_compare_value(
+            pair_test->atomic_propositions.get(),
+            new_pair->atomic_propositions.get()) == 0) {
+          if (snapshot_compare(pair_test, new_pair) == 0) {
+            XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
+            xbt_fifo_shift(mc_stack);
+            if (dot_output != nullptr)
+              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
+            return nullptr;
           }
-          cursor++;
         }
       }
-      xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
-    } else {
-      pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, index, simgrid::mc::VisitedPair*);
-      if (pair_test->nb_processes < new_pair->nb_processes)
-        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
-        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      else
-        xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
     }
-  }
+
+  xbt_dynar_insert_at(
+    ::acceptance_pairs, res.first - acceptance_pairs.begin(), &new_pair);
   return new_pair;
 }
 
@@ -213,6 +230,157 @@ 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 {
+      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;
@@ -379,8 +547,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();