[mc] Use shared_ptr for Snapshot

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 9f7c2a2..93be2c0 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -133,35 +133,37 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
 
     if (diff != NONE_DIFF) {
       if (comm->type == SIMIX_COMM_SEND){
-        initial_global_state->send_deterministic = 0;
-        if(initial_global_state->send_diff != nullptr)
-          xbt_free(initial_global_state->send_diff);
-        initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+        simgrid::mc::initial_global_state->send_deterministic = 0;
+        if(simgrid::mc::initial_global_state->send_diff != nullptr)
+          xbt_free(simgrid::mc::initial_global_state->send_diff);
+        simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
       }else{
-        initial_global_state->recv_deterministic = 0;
-        if(initial_global_state->recv_diff != nullptr)
-          xbt_free(initial_global_state->recv_diff);
-        initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+        simgrid::mc::initial_global_state->recv_deterministic = 0;
+        if(simgrid::mc::initial_global_state->recv_diff != nullptr)
+          xbt_free(simgrid::mc::initial_global_state->recv_diff);
+        simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
       }
-      if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){
+      if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
         XBT_INFO("*********************************************************");
         XBT_INFO("***** Non-send-deterministic communications pattern *****");
         XBT_INFO("*********************************************************");
-        XBT_INFO("%s", initial_global_state->send_diff);
-        xbt_free(initial_global_state->send_diff);
-        initial_global_state->send_diff = nullptr;
+        XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
+        xbt_free(simgrid::mc::initial_global_state->send_diff);
+        simgrid::mc::initial_global_state->send_diff = nullptr;
         MC_print_statistics(mc_stats);
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
-      }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
+      }else if(_sg_mc_comms_determinism
+          && (!simgrid::mc::initial_global_state->send_deterministic
+            && !simgrid::mc::initial_global_state->recv_deterministic)) {
         XBT_INFO("****************************************************");
         XBT_INFO("***** Non-deterministic communications pattern *****");
         XBT_INFO("****************************************************");
-        XBT_INFO("%s", initial_global_state->send_diff);
-        XBT_INFO("%s", initial_global_state->recv_diff);
-        xbt_free(initial_global_state->send_diff);
-        initial_global_state->send_diff = nullptr;
-        xbt_free(initial_global_state->recv_diff);
-        initial_global_state->recv_diff = nullptr;
+        XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
+        XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
+        xbt_free(simgrid::mc::initial_global_state->send_diff);
+        simgrid::mc::initial_global_state->send_diff = nullptr;
+        xbt_free(simgrid::mc::initial_global_state->recv_diff);
+        simgrid::mc::initial_global_state->recv_diff = nullptr;
         MC_print_statistics(mc_stats);
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       }
@@ -214,7 +216,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
         pattern->data, pattern->data_size, remote(synchro.comm.src_buff));
     }
     if(mpi_request.detached){
-      if (!initial_global_state->initial_communications_pattern_done) {
+      if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
         /* Store comm pattern */
         xbt_dynar_push(
           xbt_dynar_get_as(
@@ -282,7 +284,7 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
   mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
     initial_communications_pattern, issuer, mc_list_comm_pattern_t);
 
-  if (!initial_global_state->initial_communications_pattern_done)
+  if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
     /* Store comm pattern */
     xbt_dynar_push(pattern->list, &comm_pattern);
   else {
@@ -546,7 +548,7 @@ int CommunicationDeterminismChecker::run()
 
   this->prepare();
 
-  initial_global_state = xbt_new0(s_mc_global_t, 1);
+  initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->initial_communications_pattern_done = 0;
   initial_global_state->recv_deterministic = 1;
@@ -554,7 +556,9 @@ int CommunicationDeterminismChecker::run()
   initial_global_state->recv_diff = nullptr;
   initial_global_state->send_diff = nullptr;
 
-  return this->main();
+  int res = this->main();
+  initial_global_state = nullptr;
+  return res;
 }
 
 }

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 589a71d..e982672 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -150,8 +150,8 @@ simgrid::xbt::unique_ptr<s_xbt_dynar_t> LivenessChecker::getPropositionValues()
 
 int LivenessChecker::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;
+  simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get();
+  simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get();
   int num1 = state1->num;
   int num2 = state2->num;
   return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
@@ -619,10 +619,12 @@ int LivenessChecker::run()
   liveness_stack = xbt_fifo_new();
 
   /* Create the initial state */
-  initial_global_state = xbt_new0(s_mc_global_t, 1);
+  simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 
   this->prepare();
-  return this->main();
+  int res = this->main();
+  simgrid::mc::initial_global_state = nullptr;
+  return res;
 }
 
 }

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index a53e99a..274ace7 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -37,7 +37,7 @@ class ModelChecker {
   std::unique_ptr<Process> process_;
   Checker* checker_ = nullptr;
 public:
-  simgrid::mc::Snapshot* parent_snapshot_;
+  std::shared_ptr<simgrid::mc::Snapshot> parent_snapshot_;
 
 public:
   ModelChecker(ModelChecker const&) = delete;
@@ -57,7 +57,7 @@ public:
 
   bool is_important_snapshot(Snapshot const& snapshot) const
   {
-    return &snapshot == this->parent_snapshot_;
+    return &snapshot == this->parent_snapshot_.get();
   }
 
   void start();

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index a32a1a3..8903c28 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -46,8 +46,8 @@ static void MC_show_non_termination(void)
 
 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
 {
-  simgrid::mc::Snapshot* s1 = state1->system_state;
-  simgrid::mc::Snapshot* s2 = state2->system_state;
+  simgrid::mc::Snapshot* s1 = state1->system_state.get();
+  simgrid::mc::Snapshot* s2 = state2->system_state.get();
   int num1 = state1->num;
   int num2 = state2->num;
   return snapshot_compare(num1, s1, num2, s2);
@@ -285,6 +285,7 @@ int SafetyChecker::run()
 
   XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);
+  initial_global_state = nullptr;
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
@@ -328,7 +329,7 @@ void SafetyChecker::init()
   xbt_fifo_unshift(mc_stack, initial_state);
 
   /* Save the initial state */
-  initial_global_state = xbt_new0(s_mc_global_t, 1);
+  initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 }
 

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 485a5e3..7e1084b 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -415,7 +415,7 @@ static std::vector<s_mc_stack_frame_t> unwind_stack_frames(simgrid::mc::UnwindCo
   return std::move(result);
 };
 
-static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(simgrid::mc::Snapshot* * snapshot)
+static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(simgrid::mc::Snapshot* snapshot)
 {
   std::vector<s_mc_snapshot_stack_t> res;
 
@@ -439,7 +439,7 @@ static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(simgrid::mc::Snap
 
     size_t stack_size =
       (char*) stack.address + stack.size - (char*) sp;
-    (*snapshot)->stack_sizes.push_back(stack_size);
+    snapshot->stack_sizes.push_back(stack_size);
   }
 
   return std::move(res);
@@ -561,20 +561,21 @@ static std::vector<s_fd_infos_t> get_current_fds(pid_t pid)
   return std::move(fds);
 }
 
-simgrid::mc::Snapshot* take_snapshot(int num_state)
+std::shared_ptr<simgrid::mc::Snapshot> take_snapshot(int num_state)
 {
   XBT_DEBUG("Taking snapshot %i", num_state);
 
   simgrid::mc::Process* mc_process = &mc_model_checker->process();
 
-  simgrid::mc::Snapshot* snapshot = new simgrid::mc::Snapshot(mc_process);
+  std::shared_ptr<simgrid::mc::Snapshot> snapshot =
+    std::make_shared<simgrid::mc::Snapshot>(mc_process);
 
   snapshot->num_state = num_state;
 
   for (auto& p : mc_model_checker->process().simix_processes())
     snapshot->enabled_processes.insert(p.copy.pid);
 
-  snapshot_handle_ignore(snapshot);
+  snapshot_handle_ignore(snapshot.get());
 
   if (_sg_mc_snapshot_fds)
     snapshot->current_fds = get_current_fds(mc_model_checker->process().pid());
@@ -582,15 +583,14 @@ simgrid::mc::Snapshot* take_snapshot(int num_state)
   const bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty;
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
-  get_memory_regions(mc_process, snapshot);
+  get_memory_regions(mc_process, snapshot.get());
   if (use_soft_dirty)
     mc_process->reset_soft_dirty();
 
   snapshot->to_ignore = mc_model_checker->process().ignored_heap();
 
   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
-    snapshot->stacks =
-        take_snapshot_stacks(&snapshot);
+    snapshot->stacks = take_snapshot_stacks(snapshot.get());
     if (_sg_mc_hash)
       snapshot->hash = simgrid::mc::hash(*snapshot);
     else
@@ -598,7 +598,7 @@ simgrid::mc::Snapshot* take_snapshot(int num_state)
   } else
     snapshot->hash = 0;
 
-  snapshot_ignore_restore(snapshot);
+  snapshot_ignore_restore(snapshot.get());
   if (use_soft_dirty)
     mc_model_checker->parent_snapshot_ = snapshot;
   return snapshot;
@@ -645,16 +645,16 @@ void restore_snapshot_fds(simgrid::mc::Snapshot* snapshot)
   }
 }
 
-void restore_snapshot(simgrid::mc::Snapshot* snapshot)
+void restore_snapshot(std::shared_ptr<simgrid::mc::Snapshot> snapshot)
 {
   XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
   const bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty;
-  restore_snapshot_regions(snapshot);
+  restore_snapshot_regions(snapshot.get());
   if (_sg_mc_snapshot_fds)
-    restore_snapshot_fds(snapshot);
+    restore_snapshot_fds(snapshot.get());
   if (use_soft_dirty)
     mc_model_checker->process().reset_soft_dirty();
-  snapshot_ignore_restore(snapshot);
+  snapshot_ignore_restore(snapshot.get());
   mc_model_checker->process().clear_cache();
   if (use_soft_dirty)
     mc_model_checker->parent_snapshot_ = snapshot;

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 7731b41..187a69b 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -61,7 +61,6 @@ simgrid::mc::State* mc_current_state = nullptr;
 char mc_replay_mode = false;
 
 mc_stats_t mc_stats = nullptr;
-mc_global_t initial_global_state = nullptr;
 xbt_fifo_t mc_stack = nullptr;
 
 /* Liveness */
@@ -69,6 +68,7 @@ xbt_fifo_t mc_stack = nullptr;
 namespace simgrid {
 namespace mc {
 
+std::unique_ptr<s_mc_global_t> initial_global_state = nullptr;
 xbt_automaton_t property_automaton = nullptr;
 
 }
@@ -140,7 +140,7 @@ void MC_replay(xbt_fifo_t stack)
 
 
   /* Restore the initial state */
-  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+  simgrid::mc::restore_snapshot(simgrid::mc::initial_global_state->snapshot);
   /* At the moment of taking the snapshot the raw heap was set, so restoring
    * it will set it back again, we have to unset it to continue  */
 
@@ -217,16 +217,18 @@ void MC_show_deadlock(void)
 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {
-    if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){
+    if (!simgrid::mc::initial_global_state->recv_deterministic &&
+        simgrid::mc::initial_global_state->send_deterministic){
       XBT_INFO("******************************************************");
       XBT_INFO("**** Only-send-deterministic communication pattern ****");
       XBT_INFO("******************************************************");
-      XBT_INFO("%s", initial_global_state->recv_diff);
-    }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) {
+      XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
+    }else if(!simgrid::mc::initial_global_state->send_deterministic &&
+        simgrid::mc::initial_global_state->recv_deterministic) {
       XBT_INFO("******************************************************");
       XBT_INFO("**** Only-recv-deterministic communication pattern ****");
       XBT_INFO("******************************************************");
-      XBT_INFO("%s", initial_global_state->send_diff);
+      XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
     }
   }
 
@@ -242,10 +244,13 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
-  if (initial_global_state != nullptr && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
-    XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
+  if (simgrid::mc::initial_global_state != nullptr
+      && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
+    XBT_INFO("Send-deterministic : %s",
+      !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
     if (_sg_mc_comms_determinism)
-      XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
+      XBT_INFO("Recv-deterministic : %s",
+        !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
   }
   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
     int ret=system("free");

diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h
index 0214389..60c177f 100644 (file)
--- a/src/mc/mc_safety.h
+++ b/src/mc/mc_safety.h
@@ -32,7 +32,7 @@ enum class ReductionMode {
 extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
 
 struct XBT_PRIVATE VisitedState {
-  simgrid::mc::Snapshot* system_state = nullptr;
+  std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
   size_t heap_bytes_used = 0;
   int nb_processes = 0;
   int num = 0;

diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h
index 2711b69..a7b4b00 100644 (file)
--- a/src/mc/mc_snapshot.h
+++ b/src/mc/mc_snapshot.h
@@ -129,14 +129,14 @@ typedef struct XBT_PRIVATE s_mc_snapshot_stack {
 } s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
 
 typedef struct s_mc_global_t {
-  simgrid::mc::Snapshot* snapshot;
-  int prev_pair;
-  char *prev_req;
-  int initial_communications_pattern_done;
-  int recv_deterministic;
-  int send_deterministic;
-  char *send_diff;
-  char *recv_diff;
+  std::shared_ptr<simgrid::mc::Snapshot> snapshot;
+  int prev_pair = 0;
+  char *prev_req = nullptr;
+  int initial_communications_pattern_done = 0;
+  int recv_deterministic = 0;
+  int send_deterministic = 0;
+  char *send_diff = nullptr;
+  char *recv_diff = nullptr;
 }s_mc_global_t, *mc_global_t;
 
 namespace simgrid {
@@ -186,8 +186,8 @@ static const void* mc_snapshot_get_heap_end(simgrid::mc::Snapshot* snapshot);
 namespace simgrid {
 namespace mc {
 
-XBT_PRIVATE simgrid::mc::Snapshot* take_snapshot(int num_state);
-XBT_PRIVATE void restore_snapshot(simgrid::mc::Snapshot*);
+XBT_PRIVATE std::shared_ptr<simgrid::mc::Snapshot> take_snapshot(int num_state);
+XBT_PRIVATE void restore_snapshot(std::shared_ptr<simgrid::mc::Snapshot> snapshot);
 
 }
 }

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index be66f53..35fc678 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -72,8 +72,6 @@ State::~State()
  */
 void MC_state_delete(simgrid::mc::State* state, int free_snapshot)
 {
-  if (state->system_state && free_snapshot)
-    delete state->system_state;
   delete state;
 }
 

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index f607996..8fcbde4 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -7,6 +7,8 @@
 #ifndef SIMGRID_MC_STATE_H
 #define SIMGRID_MC_STATE_H
 
+#include <memory>
+
 #include <xbt/base.h>
 #include <xbt/dynar.h>
 
@@ -14,8 +16,6 @@
 #include "src/simix/smx_private.h"
 #include "src/mc/mc_snapshot.h"
 
-extern XBT_PRIVATE mc_global_t initial_global_state;
-
 /* Possible exploration status of a process in a state */
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */
@@ -34,6 +34,8 @@ typedef struct mc_procstate{
 namespace simgrid {
 namespace mc {
 
+extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
+
 /* An exploration state.
  *
  *  The `executed_state` is sometimes transformed into another `internal_req`.
@@ -48,7 +50,7 @@ struct XBT_PRIVATE State {
   s_smx_simcall_t executed_req;         /* The executed request of the state */
   int req_num = 0;                      /* The request number (in the case of a
                                        multi-request like waitany ) */
-  simgrid::mc::Snapshot* system_state = 0;      /* Snapshot of system state */
+  std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;      /* Snapshot of system state */
   int num = 0;
   int in_visited_states = 0;
   // comm determinism verification (xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>):

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 564a240..e802ccb 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -65,8 +65,6 @@ VisitedState::VisitedState()
 
 VisitedState::~VisitedState()
 {
-  if(!is_exploration_stack_state(this))
-    delete this->system_state;
 }
 
 static void prune_visited_states()
@@ -86,8 +84,8 @@ static void prune_visited_states()
 
 static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
 {
-  simgrid::mc::Snapshot* s1 = state1->system_state;
-  simgrid::mc::Snapshot* s2 = state2->system_state;
+  simgrid::mc::Snapshot* s1 = state1->system_state.get();
+  simgrid::mc::Snapshot* s2 = state2->system_state.get();
   int num1 = state1->num;
   int num2 = state2->num;
   return snapshot_compare(num1, s1, num2, s2);