[mc] Move main communication determinism code in a CommunicationDeterminismChecker...

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/CommunicationDeterminismChecker.cpp
similarity index 97%
rename from src/mc/mc_comm_determinism.cpp
rename to src/mc/CommunicationDeterminismChecker.cpp
index 3870c38..5262982 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -20,6 +20,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/CommunicationDeterminismChecker.hpp"

 #include "src/mc/mc_exit.h"
 
 using simgrid::mc::remote;
 #include "src/mc/mc_exit.h"
 
 using simgrid::mc::remote;


@@ -27,8 +28,6 @@ using simgrid::mc::remote;
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
                                 "Logging specific to MC communication determinism detection");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
                                 "Logging specific to MC communication determinism detection");
 

-extern "C" {
-

 /********** Global variables **********/
 
 xbt_dynar_t initial_communications_pattern;
 /********** Global variables **********/
 
 xbt_dynar_t initial_communications_pattern;


@@ -165,10 +164,10 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
         initial_global_state->recv_diff = nullptr;
         MC_print_statistics(mc_stats);
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
         initial_global_state->recv_diff = nullptr;
         MC_print_statistics(mc_stats);
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);

-      } 
+      }

     }
   }
     }
   }

-    
+

   MC_comm_pattern_free(comm);
 
 }
   MC_comm_pattern_free(comm);
 
 }


@@ -231,7 +230,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
       }
       return;
     }
       }
       return;
     }

-  } else if (call_type == MC_CALL_TYPE_RECV) {                      
+  } else if (call_type == MC_CALL_TYPE_RECV) {

     pattern->type = SIMIX_COMM_RECEIVE;
     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 
     pattern->type = SIMIX_COMM_RECEIVE;
     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 


@@ -296,16 +295,28 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
 
 /************************ Main algorithm ************************/
 
 
 /************************ Main algorithm ************************/
 

-static int MC_modelcheck_comm_determinism_main(void);
+namespace simgrid {
+namespace mc {
+
+CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
+  : Checker(session)
+{
+
+}
+
+CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
+{
+
+}

 
 

-static void MC_pre_modelcheck_comm_determinism(void)
+void CommunicationDeterminismChecker::prepare()

 {
   mc_state_t initial_state = nullptr;
   int i;
   const int maxpid = MC_smx_get_maxpid();
 
   simgrid::mc::visited_states.clear();
 {
   mc_state_t initial_state = nullptr;
   int i;
   const int maxpid = MC_smx_get_maxpid();
 
   simgrid::mc::visited_states.clear();

- 
+

   // Create initial_communications_pattern elements:
   initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
   for (i=0; i < maxpid; i++){
   // Create initial_communications_pattern elements:
   initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
   for (i=0; i < maxpid; i++){


@@ -323,7 +334,7 @@ static void MC_pre_modelcheck_comm_determinism(void)
   }
 
   initial_state = MC_state_new();
   }
 
   initial_state = MC_state_new();

-  
+

   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */
   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */


@@ -351,7 +362,7 @@ bool all_communications_are_finished()
   return true;
 }
 
   return true;
 }
 

-static int MC_modelcheck_comm_determinism_main(void)
+int CommunicationDeterminismChecker::main(void)

 {
 
   char *req_str = nullptr;
 {
 
   char *req_str = nullptr;


@@ -380,7 +391,7 @@ static int MC_modelcheck_comm_determinism_main(void)
       req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
       req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);

-      
+

       if (dot_output != nullptr)
         req_str = simgrid::mc::request_get_dot_output(req, value);
 
       if (dot_output != nullptr)
         req_str = simgrid::mc::request_get_dot_output(req, value);
 


@@ -441,7 +452,7 @@ static int MC_modelcheck_comm_determinism_main(void)
       else
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
 
       else
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
 

-      if (!initial_global_state->initial_communications_pattern_done) 
+      if (!initial_global_state->initial_communications_pattern_done)

         initial_global_state->initial_communications_pattern_done = 1;
 
       /* Trash the current state, no longer needed */
         initial_global_state->initial_communications_pattern_done = 1;
 
       /* Trash the current state, no longer needed */


@@ -480,7 +491,7 @@ static int MC_modelcheck_comm_determinism_main(void)
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 

-int MC_modelcheck_comm_determinism(void)
+int CommunicationDeterminismChecker::run()

 {
   XBT_INFO("Check communication determinism");
   mc_model_checker->wait_for_requests();
 {
   XBT_INFO("Check communication determinism");
   mc_model_checker->wait_for_requests();


@@ -492,7 +503,7 @@ int MC_modelcheck_comm_determinism(void)
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 

-  MC_pre_modelcheck_comm_determinism();
+  this->prepare();

 
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);


@@ -502,7 +513,8 @@ int MC_modelcheck_comm_determinism(void)
   initial_global_state->recv_diff = nullptr;
   initial_global_state->send_diff = nullptr;
 
   initial_global_state->recv_diff = nullptr;
   initial_global_state->send_diff = nullptr;
 

-  return MC_modelcheck_comm_determinism_main();
+  return this->main();

 }
 
 }
 }
 
 }

+}
\ No newline at end of file

diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp
new file mode 100644 (file)
index 0000000..d23c95c
--- /dev/null
+++ b/src/mc/CommunicationDeterminismChecker.hpp
@@ -0,0 +1,29 @@
+/* Copyright (c) 2016. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/Checker.hpp"
+
+#ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
+#define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
+
+namespace simgrid {
+namespace mc {
+
+class CommunicationDeterminismChecker : public Checker {
+public:
+  CommunicationDeterminismChecker(Session& session);
+  ~CommunicationDeterminismChecker();
+  int run() override;
+private:
+  void prepare();
+  int main();
+};
+
+#endif
+
+}
+}

diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h
index 83c386a..926e933 100644 (file)
--- a/src/mc/mc_comm_pattern.h
+++ b/src/mc/mc_comm_pattern.h
@@ -90,7 +90,6 @@ XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_
 XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p);
 XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p);
 XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
 XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p);
 XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p);
 XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);

-int MC_modelcheck_comm_determinism(void);

 
 XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state);
 
 
 XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state);
 

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index ac45108..949ed65 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -28,6 +28,7 @@
 #include "src/mc/mc_exit.h"
 #include "src/mc/Session.hpp"
 #include "src/mc/Checker.hpp"
 #include "src/mc/mc_exit.h"
 #include "src/mc/Session.hpp"
 #include "src/mc/Checker.hpp"

+#include "src/mc/CommunicationDeterminismChecker.hpp"

 #include "src/mc/SafetyChecker.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 #include "src/mc/SafetyChecker.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");


@@ -49,8 +50,8 @@ std::unique_ptr<simgrid::mc::Checker> createChecker(simgrid::mc::Session& sessio
 
   std::function<int(Session& session)> code;
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 
   std::function<int(Session& session)> code;
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)

-    code = [](Session& session) {
-      return MC_modelcheck_comm_determinism(); };
+    return std::unique_ptr<simgrid::mc::Checker>(
+      new simgrid::mc::CommunicationDeterminismChecker(session));

   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
     return std::unique_ptr<simgrid::mc::Checker>(
       new simgrid::mc::SafetyChecker(session));
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
     return std::unique_ptr<simgrid::mc::Checker>(
       new simgrid::mc::SafetyChecker(session));

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index ca3b2be..9b9dc68 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -554,6 +554,8 @@ set(MC_SRC
   src/mc/Checker.hpp
   src/mc/Client.cpp
   src/mc/Client.hpp
   src/mc/Checker.hpp
   src/mc/Client.cpp
   src/mc/Client.hpp

+  src/mc/CommunicationDeterminismChecker.cpp
+  src/mc/CommunicationDeterminismChecker.hpp

   src/mc/Frame.hpp
   src/mc/Frame.cpp
   src/mc/ModelChecker.hpp
   src/mc/Frame.hpp
   src/mc/Frame.cpp
   src/mc/ModelChecker.hpp


@@ -585,7 +587,6 @@ set(MC_SRC
   src/mc/mc_page_snapshot.cpp
   src/mc/mc_comm_pattern.h
   src/mc/mc_comm_pattern.cpp
   src/mc/mc_page_snapshot.cpp
   src/mc/mc_comm_pattern.h
   src/mc/mc_comm_pattern.cpp

-  src/mc/mc_comm_determinism.cpp

   src/mc/mc_compare.cpp
   src/mc/mc_diff.cpp
   src/mc/mc_dwarf.hpp
   src/mc/mc_compare.cpp
   src/mc/mc_diff.cpp
   src/mc/mc_dwarf.hpp