further simpify the MC initialization on app side

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 5bc5651..19decad 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -9,13 +9,6 @@
 #include <simgrid/forward.h>
 #include <simgrid/modelchecker.h> /* our public interface (and definition of SIMGRID_HAVE_MC) */
 
-SG_BEGIN_DECL
-
-/********************************* Global *************************************/
-XBT_ATTRIB_NORETURN XBT_PUBLIC void MC_run();
-
-SG_END_DECL
-
 #ifdef __cplusplus
 XBT_PUBLIC void MC_process_clock_add(const simgrid::kernel::actor::ActorImpl*, double);
 XBT_PUBLIC double MC_process_clock_get(const simgrid::kernel::actor::ActorImpl*);

diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp
index 686871d..8036e2e 100644 (file)
--- a/src/kernel/EngineImpl.cpp
+++ b/src/kernel/EngineImpl.cpp
@@ -687,6 +687,15 @@ void EngineImpl::run(double max_date)
 {
   seal_platform();
 
+  if (MC_is_active()) {
+#if SIMGRID_HAVE_MC
+    mc::AppSide::get()->main_loop();
+#else
+    xbt_die("MC_is_active() is not supposed to return true in non-MC settings");
+#endif
+    return;
+  }
+
   if (MC_record_replay_is_active()) {
     mc::RecordTrace::replay(MC_record_path());
     empty_trash();

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 5a75da0..e733950 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -41,23 +41,9 @@ std::vector<double> processes_time;
 
 #if SIMGRID_HAVE_MC
 
-/* Liveness */
-
-namespace simgrid {
-namespace mc {
-
-xbt_automaton_t property_automaton = nullptr;
-
-}
-}
-
 /* Dot output */
 FILE *dot_output = nullptr;
 
-
-/*******************************  Initialization of MC *******************************/
-/*********************************************************************************/
-
 void MC_init_dot_output()
 {
   dot_output = fopen(_sg_mc_dot_output_file.get().c_str(), "w");
@@ -67,20 +53,15 @@ void MC_init_dot_output()
           "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
 }
 
-/*******************************  Core of MC *******************************/
-/**************************************************************************/
-
-void MC_run()
-{
-  simgrid::mc::processes_time.resize(simgrid::kernel::actor::get_maxpid());
-  MC_ignore_heap(simgrid::mc::processes_time.data(),
-    simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
-  simgrid::mc::AppSide::get()->main_loop();
-}
 
 namespace simgrid {
 namespace mc {
 
+/* Liveness */
+xbt_automaton_t property_automaton = nullptr;
+
+/*******************************  Core of MC *******************************/
+/**************************************************************************/
 void dumpStack(FILE* file, unw_cursor_t* cursor)
 {
   int nframe = 0;

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index f477165..7fb6628 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -200,6 +200,10 @@ void AppSide::handle_messages() const
 
 void AppSide::main_loop() const
 {
+  simgrid::mc::processes_time.resize(simgrid::kernel::actor::get_maxpid());
+  MC_ignore_heap(simgrid::mc::processes_time.data(),
+                 simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
+
   coverage_checkpoint();
   while (true) {
     simgrid::mc::execute_actors();

diff --git a/src/s4u/s4u_Engine.cpp b/src/s4u/s4u_Engine.cpp
index c66e54a..b7152fa 100644 (file)
--- a/src/s4u/s4u_Engine.cpp
+++ b/src/s4u/s4u_Engine.cpp
@@ -346,11 +346,7 @@ void Engine::run_until(double max_date) const
   fflush(stdout);
   fflush(stderr);
 
-  if (MC_is_active()) {
-    MC_run();
-  } else {
-    pimpl->run(max_date);
-  }
+  pimpl->run(max_date);
 }
 
 void Engine::track_vetoed_activities(std::set<Activity*>* vetoed_activities) const

diff --git a/src/smpi/internals/smpi_global.cpp b/src/smpi/internals/smpi_global.cpp
index 681c183..548bee4 100644 (file)
--- a/src/smpi/internals/smpi_global.cpp
+++ b/src/smpi/internals/smpi_global.cpp
@@ -575,14 +575,11 @@ int smpi_main(const char* executable, int argc, char* argv[])
   fflush(stdout);
   fflush(stderr);
 
-  if (MC_is_active()) {
-    MC_run();
-  } else {
-    engine.get_impl()->run(-1);
+  engine.get_impl()->run(-1);
+
+  xbt_os_walltimer_stop(global_timer);
+  simgrid::smpi::utils::print_time_analysis(xbt_os_timer_elapsed(global_timer));
 
-    xbt_os_walltimer_stop(global_timer);
-    simgrid::smpi::utils::print_time_analysis(xbt_os_timer_elapsed(global_timer));
-  }
   SMPI_finalize();
 
 #if SMPI_IFORT