[mc] Move the (main) safety code as methods of SafetyChecker

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index d6a24e1..ea0b775 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -47,12 +47,10 @@ static int is_exploration_stack_state(mc_state_t current_state){
   return 0;
 }
 
-static void modelcheck_safety_init(void);
-
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
-static void pre_modelcheck_safety()
+void SafetyChecker::pre()
 {
   simgrid::mc::visited_states.clear();
 
@@ -68,20 +66,16 @@ static void pre_modelcheck_safety()
   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);
-      if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
+      if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
 
   xbt_fifo_unshift(mc_stack, initial_state);
 }
 
-
-/** \brief Model-check the application using a DFS exploration
- *         with DPOR (Dynamic Partial Order Reductions)
- */
-static int modelcheck_safety(void)
+int SafetyChecker::run()
 {
-  modelcheck_safety_init();
+  this->init();
 
   char *req_str = nullptr;
   int value;
@@ -140,7 +134,7 @@ static int modelcheck_safety(void)
         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);
-            if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
+            if (reductionMode_ != simgrid::mc::ReductionMode::none)
               break;
           }
 
@@ -194,14 +188,14 @@ static int modelcheck_safety(void)
          state that executed that previous request. */
 
       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
-        if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::dpor) {
+        if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
           req = MC_state_get_internal_request(state);
           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);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
-            if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none
+            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)) {
                 XBT_DEBUG("Dependent Transitions:");
@@ -260,13 +254,16 @@ static int modelcheck_safety(void)
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
-static void modelcheck_safety_init(void)
+void SafetyChecker::init()
 {
-  if(_sg_mc_termination)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
-  else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
+  reductionMode_ = simgrid::mc::reduction_mode;
+  if( _sg_mc_termination)
+    reductionMode_ = simgrid::mc::ReductionMode::none;
+  else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
+    reductionMode_ = simgrid::mc::ReductionMode::dpor;
+
   _sg_mc_safety = 1;
+
   if (_sg_mc_termination)
     XBT_INFO("Check non progressive cycles");
   else
@@ -275,12 +272,10 @@ static void modelcheck_safety_init(void)
 
   XBT_DEBUG("Starting the safety algorithm");
 
-  _sg_mc_safety = 1;
-
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
-  pre_modelcheck_safety();
+  this->pre();
 
   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);
@@ -294,11 +289,6 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 SafetyChecker::~SafetyChecker()
 {
 }
-
-int SafetyChecker::run()
-{
-  return simgrid::mc::modelcheck_safety();
-}
   
 }
 }

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index 597af14..3c559a7 100644 (file)
--- a/src/mc/SafetyChecker.hpp
+++ b/src/mc/SafetyChecker.hpp
@@ -14,10 +14,15 @@ namespace simgrid {
 namespace mc {
 
 class SafetyChecker : public Checker {
+  simgrid::mc::ReductionMode reductionMode_ = simgrid::mc::ReductionMode::unset;
 public:
   SafetyChecker(Session& session);
   ~SafetyChecker();
   int run() override;
+private:
+  // Temp
+  void init();
+  void pre();
 };
 
 }

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 961a9ab..223bfc0 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -144,5 +144,7 @@ void Session::close()
   }
 }
 
+simgrid::mc::Session* session;
+
 }
 }
\ No newline at end of file

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 47c10e7..f53d948 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -64,6 +64,9 @@ public: // static constructors
   static Session* spawnvp(const char *path, char *const argv[]);
 };
 
+// Temporary
+extern simgrid::mc::Session* session;
+
 }
 }
 

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 3d3017d..8c48f73 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -84,6 +84,7 @@ int main(int argc, char** argv)
 
     std::unique_ptr<Session> session =
       std::unique_ptr<Session>(Session::spawnvp(argv[1], argv+1));
+    simgrid::mc::session = session.get();
     std::unique_ptr<simgrid::mc::Checker> checker = createChecker(*session);
     int res = checker->run();
     session->close();