[mc] Use std::unique_ptr for States

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 541a001..7075a2e 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -316,9 +316,9 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (simgrid::mc::State* state : stack_) {
+  for (auto const& state : stack_) {
     int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
     const int pid = issuer->pid;
     res.push_back(RecordTraceElement(pid, value));
@@ -330,9 +330,9 @@ RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
-  for (simgrid::mc::State* state : stack_) {
+  for (auto const& state : stack_) {
     int value;
-    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
     if (req) {
       char* req_str = simgrid::mc::request_to_string(
         req, value, simgrid::mc::RequestType::executed);
@@ -345,7 +345,7 @@ std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // o
 
 void CommunicationDeterminismChecker::prepare()
 {
-  simgrid::mc::State* initial_state = nullptr;
+
   int i;
   const int maxpid = MC_smx_get_maxpid();
 
@@ -365,7 +365,8 @@ void CommunicationDeterminismChecker::prepare()
     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }
 
-  initial_state = MC_state_new();
+  std::unique_ptr<simgrid::mc::State> initial_state =
+    std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
@@ -375,9 +376,9 @@ void CommunicationDeterminismChecker::prepare()
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy))
-      MC_state_interleave_process(initial_state, &p.copy);
+      MC_state_interleave_process(initial_state.get(), &p.copy);
 
-  stack_.push_back(initial_state);
+  stack_.push_back(std::move(initial_state));
 }
 
 static inline
@@ -401,12 +402,11 @@ int CommunicationDeterminismChecker::main(void)
   int value;
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
   smx_simcall_t req = nullptr;
-  simgrid::mc::State* next_state = nullptr;
 
   while (!stack_.empty()) {
 
     /* Get current state */
-    simgrid::mc::State* state = stack_.back();
+    simgrid::mc::State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)",
@@ -447,7 +447,8 @@ int CommunicationDeterminismChecker::main(void)
       mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
-      next_state = MC_state_new();
+      std::unique_ptr<simgrid::mc::State> next_state =
+        std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
       /* If comm determinism verification, we cannot stop the exploration if
          some communications are not finished (at least, data are transfered).
@@ -456,12 +457,13 @@ int CommunicationDeterminismChecker::main(void)
       bool compare_snapshots = all_communications_are_finished()
         && initial_global_state->initial_communications_pattern_done;
 
-      if (_sg_mc_visited == 0 || (visited_state = visitedStates_.addVisitedState(next_state, compare_snapshots)) == nullptr) {
+      if (_sg_mc_visited == 0
+          || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
           if (simgrid::mc::process_is_enabled(&p.copy))
-            MC_state_interleave_process(next_state, &p.copy);
+            MC_state_interleave_process(next_state.get(), &p.copy);
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
@@ -470,7 +472,7 @@ int CommunicationDeterminismChecker::main(void)
         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
           state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
-      stack_.push_back(next_state);
+      stack_.push_back(std::move(next_state));
 
       if (dot_output != nullptr)
         xbt_free(req_str);
@@ -489,10 +491,9 @@ int CommunicationDeterminismChecker::main(void)
         initial_global_state->initial_communications_pattern_done = 1;
 
       /* Trash the current state, no longer needed */
-      stack_.pop_back();
-      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
       XBT_DEBUG("Delete state %d at depth %zi",
-        state->num, stack_.size() + 1);
+        state->num, stack_.size());
+      stack_.pop_back();
 
       visited_state = nullptr;
 
@@ -503,25 +504,24 @@ int CommunicationDeterminismChecker::main(void)
       }
 
       while (!stack_.empty()) {
-        simgrid::mc::State* state = stack_.back();
+        std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
         stack_.pop_back();
-        if (MC_state_interleave_size(state)
+        if (MC_state_interleave_size(state.get())
             && stack_.size() < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %zi",
             state->num, stack_.size() + 1);
-          stack_.push_back(state);
+          stack_.push_back(std::move(state));
 
           simgrid::mc::replay(stack_);
 
           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
-            state->num, stack_.size());
+            stack_.back()->num, stack_.size());
 
           break;
         } else {
           XBT_DEBUG("Delete state %d at depth %zi",
             state->num, stack_.size() + 1);
-          MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }
     }

diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp
index c345af7..a33c5ce 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.hpp
+++ b/src/mc/CommunicationDeterminismChecker.hpp
@@ -28,7 +28,7 @@ private:
   int main();
 private:
   /** Stack representing the position in the exploration graph */
-  std::list<simgrid::mc::State*> stack_;
+  std::list<std::unique_ptr<simgrid::mc::State>> stack_;
   simgrid::mc::VisitedStates visitedStates_;
 };
 

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 58e9a16..4f527cb 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -57,7 +57,7 @@ static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat
 bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
 {
   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
-    if(snapshot_compare(*i, current_state) == 0){
+    if (snapshot_compare(i->get(), current_state) == 0){
       XBT_INFO("Non-progressive cycle : state %d -> state %d",
         (*i)->num, current_state->num);
       return true;
@@ -68,9 +68,9 @@ bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
 RecordTrace SafetyChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (simgrid::mc::State* state : stack_) {
+  for (auto const& state : stack_) {
     int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
     const int pid = issuer->pid;
     res.push_back(RecordTraceElement(pid, value));
@@ -81,9 +81,9 @@ RecordTrace SafetyChecker::getRecordTrace() // override
 std::vector<std::string> SafetyChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
-  for (simgrid::mc::State* state : stack_) {
+  for (auto const& state : stack_) {
     int value;
-    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
     if (req) {
       char* req_str = simgrid::mc::request_to_string(
         req, value, simgrid::mc::RequestType::executed);
@@ -102,14 +102,13 @@ int SafetyChecker::run()
   int value;
   smx_simcall_t req = nullptr;
   simgrid::mc::State* prev_state = nullptr;
-  simgrid::mc::State* next_state = nullptr;
   xbt_fifo_item_t item = nullptr;
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 
   while (!stack_.empty()) {
 
     /* Get current state */
-    simgrid::mc::State* state = stack_.back();
+    simgrid::mc::State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG(
@@ -143,20 +142,21 @@ int SafetyChecker::run()
       mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
-      next_state = MC_state_new();
+      std::unique_ptr<simgrid::mc::State> next_state =
+        std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
-      if (_sg_mc_termination && this->checkNonDeterminism(next_state)){
+      if (_sg_mc_termination && this->checkNonDeterminism(next_state.get())){
           MC_show_non_termination();
           return SIMGRID_MC_EXIT_NON_TERMINATION;
       }
 
       if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(next_state, true)) == nullptr) {
+          || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
           if (simgrid::mc::process_is_enabled(&p.copy)) {
-            MC_state_interleave_process(next_state, &p.copy);
+            MC_state_interleave_process(next_state.get(), &p.copy);
             if (reductionMode_ != simgrid::mc::ReductionMode::none)
               break;
           }
@@ -167,7 +167,7 @@ int SafetyChecker::run()
       } else if (dot_output != nullptr)
         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
-      stack_.push_back(next_state);
+      stack_.push_back(std::move(next_state));
 
       if (dot_output != nullptr)
         xbt_free(req_str);
@@ -192,9 +192,8 @@ int SafetyChecker::run()
           stack_.size() + 1);
 
       /* Trash the current state, no longer needed */
+      XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
       stack_.pop_back();
-      XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1);
-      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 
       visited_state = nullptr;
 
@@ -212,16 +211,16 @@ int SafetyChecker::run()
          state that executed that previous request. */
 
       while (!stack_.empty()) {
-        state = stack_.back();
+        std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
         stack_.pop_back();
         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
-          req = MC_state_get_internal_request(state);
+          req = MC_state_get_internal_request(state.get());
           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
             xbt_die("Mutex is currently not supported with DPOR, "
               "use --cfg=model-check/reduction:none");
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
-            simgrid::mc::State* prev_state = *i;
+            simgrid::mc::State* prev_state = i->get();
             if (reductionMode_ != simgrid::mc::ReductionMode::none
                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
@@ -230,7 +229,7 @@ int SafetyChecker::run()
                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
                 xbt_free(req_str);
-                prev_req = MC_state_get_executed_request(state, &value);
+                prev_req = MC_state_get_executed_request(state.get(), &value);
                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
                 xbt_free(req_str);
@@ -261,20 +260,19 @@ int SafetyChecker::run()
           }
         }
 
-        if (MC_state_interleave_size(state)
+        if (MC_state_interleave_size(state.get())
             && stack_.size() < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %zi",
             state->num, stack_.size() + 1);
-          stack_.push_back(state);
+          stack_.push_back(std::move(state));
           simgrid::mc::replay(stack_);
           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
-            state->num, stack_.size());
+            stack_.back()->num, stack_.size());
           break;
         } else {
           XBT_DEBUG("Delete state %d at depth %zi",
             state->num, stack_.size() + 1);
-          MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }
     }
@@ -302,7 +300,8 @@ void SafetyChecker::init()
 
   XBT_DEBUG("Starting the safety algorithm");
 
-  simgrid::mc::State* initial_state = MC_state_new();
+  std::unique_ptr<simgrid::mc::State> initial_state =
+    std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
@@ -313,12 +312,12 @@ void SafetyChecker::init()
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy)) {
-      MC_state_interleave_process(initial_state, &p.copy);
+      MC_state_interleave_process(initial_state.get(), &p.copy);
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
 
-  stack_.push_back(initial_state);
+  stack_.push_back(std::move(initial_state));
 
   /* Save the initial state */
   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index 1435182..4f60b79 100644 (file)
--- a/src/mc/SafetyChecker.hpp
+++ b/src/mc/SafetyChecker.hpp
@@ -8,6 +8,7 @@
 #define SIMGRID_MC_SAFETY_CHECKER_HPP
 
 #include <list>
+#include <memory>
 
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/Checker.hpp"
@@ -30,7 +31,7 @@ private:
   bool checkNonDeterminism(simgrid::mc::State* current_state);
 private:
   /** Stack representing the position in the exploration graph */
-  std::list<simgrid::mc::State*> stack_;
+  std::list<std::unique_ptr<simgrid::mc::State>> stack_;
   simgrid::mc::VisitedStates visitedStates_;
 };
 

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 9d7073c..cf23f62 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -118,13 +118,13 @@ namespace mc {
  * \param stack The stack with the transitions to execute.
  * \param start Start index to begin the re-execution.
  */
-void replay(std::list<simgrid::mc::State*> const& stack)
+void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
 {
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
-    simgrid::mc::State* state = stack.back();
+    simgrid::mc::State* state = stack.back().get();
     if (state->system_state) {
       simgrid::mc::restore_snapshot(state->system_state);
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
@@ -153,12 +153,12 @@ void replay(std::list<simgrid::mc::State*> const& stack)
   int count = 1;
 
   /* Traverse the stack from the state at position start and re-execute the transitions */
-  for (simgrid::mc::State* state : stack) {
+  for (std::unique_ptr<simgrid::mc::State> const& state : stack) {
     if (state == stack.back())
       break;
 
     int value;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     
     if (saved_req) {
       /* because we got a copy of the executed request, we have to fetch the  
@@ -170,7 +170,7 @@ void replay(std::list<simgrid::mc::State*> const& stack)
       /* Debug information */
       if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
         char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-        XBT_DEBUG("Replay: %s (%p)", req_str, state);
+        XBT_DEBUG("Replay: %s (%p)", req_str, state.get());
         xbt_free(req_str);
       }
 

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index 68acc45..94c7201 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -62,7 +62,7 @@ struct XBT_PRIVATE State {
   ~State();
 };
 
-XBT_PRIVATE void replay(std::list<simgrid::mc::State*> const& stack);
+XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
 
 }
 }