smx processes are now called actors, avoiding confusions in MC

[simgrid.git] / src / mc / SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 5e106ad..47e2e70 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -59,8 +59,7 @@ bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
 {
   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
     if (snapshot_compare(i->get(), current_state) == 0){
-      XBT_INFO("Non-progressive cycle : state %d -> state %d",
-        (*i)->num, current_state->num);
+      XBT_INFO("Non-progressive cycle: state %d -> state %d", (*i)->num, current_state->num);
       return true;
     }
   return false;
@@ -97,8 +96,6 @@ void SafetyChecker::logState() // override
 
 int SafetyChecker::run()
 {
-  this->init();
-
   while (!stack_.empty()) {
 
     /* Get current state */
@@ -142,7 +139,7 @@ int SafetyChecker::run()
 
     /* Create the new expanded state */
     std::unique_ptr<simgrid::mc::State> next_state =
-      std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+        std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
         MC_show_non_termination();
@@ -153,9 +150,9 @@ int SafetyChecker::run()
         || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, 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)) {
-          next_state->interleave(&p.copy);
+      for (auto& p : mc_model_checker->process().actors())
+        if (simgrid::mc::actor_is_enabled(p.copy.getBuffer())) {
+          next_state->interleave(p.copy.getBuffer());
           if (reductionMode_ != simgrid::mc::ReductionMode::none)
             break;
         }
@@ -174,7 +171,6 @@ int SafetyChecker::run()
 
   XBT_INFO("No property violation found.");
   simgrid::mc::session->logState();
-  initial_global_state = nullptr;
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
@@ -217,11 +213,10 @@ int SafetyChecker::backtrack()
       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);
+      const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         simgrid::mc::State* prev_state = i->get();
-        if (reductionMode_ != simgrid::mc::ReductionMode::none
-            && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
+        if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("Dependent Transitions:");
             int value = prev_state->transition.argument;
@@ -252,7 +247,7 @@ int SafetyChecker::backtrack()
 
         } else {
 
-          const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
+          const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
                     req->call, issuer->pid, state->num,
                     prev_state->internal_req.call,
@@ -269,7 +264,7 @@ int SafetyChecker::backtrack()
       XBT_DEBUG("Back-tracking to state %d at depth %zi",
         state->num, stack_.size() + 1);
       stack_.push_back(std::move(state));
-      simgrid::mc::replay(stack_);
+      this->restoreState();
       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
         stack_.back()->num, stack_.size());
       break;
@@ -281,10 +276,35 @@ int SafetyChecker::backtrack()
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
-void SafetyChecker::init()
+void SafetyChecker::restoreState()
+{
+  /* Intermediate backtracking */
+  {
+    simgrid::mc::State* state = stack_.back().get();
+    if (state->system_state) {
+      simgrid::mc::restore_snapshot(state->system_state);
+      return;
+    }
+  }
+
+  /* Restore the initial state */
+  simgrid::mc::session->restoreInitialState();
+
+  /* Traverse the stack from the state at position start and re-execute the transitions */
+  for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
+    if (state == stack_.back())
+      break;
+    session->execute(state->transition);
+    /* Update statistics */
+    mc_model_checker->visited_states++;
+    mc_model_checker->executed_transitions++;
+  }
+}
+
+SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 {
   reductionMode_ = simgrid::mc::reduction_mode;
-  if( _sg_mc_termination)
+  if (_sg_mc_termination)
     reductionMode_ = simgrid::mc::ReductionMode::none;
   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
     reductionMode_ = simgrid::mc::ReductionMode::dpor;
@@ -293,33 +313,25 @@ void SafetyChecker::init()
     XBT_INFO("Check non progressive cycles");
   else
     XBT_INFO("Check a safety property");
-  mc_model_checker->wait_for_requests();
+  simgrid::mc::session->initialize();
 
   XBT_DEBUG("Starting the safety algorithm");
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
 
-  /* 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)) {
-      initial_state->interleave(&p.copy);
+  /* Get an enabled actor and insert it in the interleave set of the initial state */
+  for (auto& actor : mc_model_checker->process().actors())
+    if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
+      initial_state->interleave(actor.copy.getBuffer());
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
 
   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());
-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
-}
-
-SafetyChecker::SafetyChecker(Session& session) : Checker(session)
-{
 }
 
 SafetyChecker::~SafetyChecker()