[mc] Move some liveness code in the liveness file (private/static)

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 825113f..6d208dd 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -349,7 +349,6 @@ static int compare_local_variables(int process_index,
 namespace simgrid {
 namespace mc {
 
 namespace simgrid {
 namespace mc {
 

-static

 int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();
 int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();


@@ -543,15 +542,6 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
   return errors > 0 || hash_result;
 }
 
   return errors > 0 || hash_result;
 }
 

-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);
-}
-

 int snapshot_compare(mc_state_t state1, mc_state_t state2)
 {
   simgrid::mc::Snapshot* s1 = state1->system_state;
 int snapshot_compare(mc_state_t state1, mc_state_t state2)
 {
   simgrid::mc::Snapshot* s1 = state1->system_state;

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index dbd4677..090fe45 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -283,39 +283,6 @@ void MC_show_non_termination(void){
   MC_print_statistics(mc_stats);
 }
 
   MC_print_statistics(mc_stats);
 }
 

-namespace simgrid {
-namespace mc {
-
-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);
-    }
-  }
-}
-
-void dump_stack_liveness(xbt_fifo_t stack)
-{
-  simgrid::mc::Pair* pair;
-  while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
-    delete pair;
-}
-
-}
-}
-

 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {
 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 2266c83..b65314f 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -21,6 +21,7 @@
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_smx.h"
 #include "src/mc/Client.hpp"
 #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"
 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_exit.h"


@@ -37,6 +38,8 @@ xbt_dynar_t acceptance_pairs;
 namespace simgrid {
 namespace mc {
 
 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)
 {}
 Pair::Pair() : num(++mc_stats->expanded_pairs),
   visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
 {}


@@ -46,6 +49,33 @@ Pair::~Pair() {
     MC_state_delete(this->graph_state, 1);
 }
 
     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;
 static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
 {
   unsigned int cursor = 0;


@@ -58,6 +88,15 @@ static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
   return std::move(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(
 static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
 {
   simgrid::mc::VisitedPair* new_pair = new VisitedPair(


@@ -274,6 +313,94 @@ static void MC_replay_liveness(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
   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(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;
 static int MC_modelcheck_liveness_main(void)
 {
   simgrid::mc::Pair* current_pair = nullptr;

diff --git a/src/mc/mc_liveness.h b/src/mc/mc_liveness.h
index 0b5b2da..c722183 100644 (file)
--- a/src/mc/mc_liveness.h
+++ b/src/mc/mc_liveness.h
@@ -61,13 +61,6 @@ struct XBT_PRIVATE VisitedPair {
 };
 
 int modelcheck_liveness(void);
 };
 
 int modelcheck_liveness(void);

-XBT_PRIVATE void show_stack_liveness(xbt_fifo_t stack);
-XBT_PRIVATE void dump_stack_liveness(xbt_fifo_t stack);
-
-XBT_PRIVATE extern xbt_dynar_t visited_pairs;
-XBT_PRIVATE int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair);
-
-XBT_PRIVATE int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);

 
 }
 }
 
 }
 }

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 23c17b0..a40308d 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -88,6 +88,8 @@ XBT_PRIVATE void MC_print_statistics(mc_stats_t stats);
 XBT_PRIVATE void MC_report_assertion_error(void);
 XBT_PRIVATE void MC_report_crash(int status);
 
 XBT_PRIVATE void MC_report_assertion_error(void);
 XBT_PRIVATE void MC_report_crash(int status);
 

+SG_END_DECL()
+

 #ifdef __cplusplus
 
 namespace simgrid {
 #ifdef __cplusplus
 
 namespace simgrid {


@@ -96,11 +98,12 @@ namespace mc {
 XBT_PRIVATE void find_object_address(
   std::vector<simgrid::xbt::VmMap> const& maps, simgrid::mc::ObjectInformation* result);
 
 XBT_PRIVATE void find_object_address(
   std::vector<simgrid::xbt::VmMap> const& maps, simgrid::mc::ObjectInformation* result);
 

+XBT_PRIVATE
+int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2);
+

 }
 }
 
 #endif
 
 }
 }
 
 #endif
 

-SG_END_DECL()
-

 #endif
 #endif

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 19a9e2e..f030a59 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -28,7 +28,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
 namespace simgrid {
 namespace mc {
 
 namespace simgrid {
 namespace mc {
 

-xbt_dynar_t visited_pairs;

 std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
 
 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
 std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
 
 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){


@@ -391,92 +390,5 @@ std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_sta
     return nullptr;
 }
 
     return nullptr;
 }
 

-/**
- * \brief Checks whether a given pair has already been visited by the algorithm.
- */
-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(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;
-}
-

 }
 }
\ No newline at end of file
 }
 }
\ No newline at end of file