[mc] Remove standalone mode and remove MC_do_the_modelcheck_for_real()

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 112140d..ee2fc7c 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -582,6 +582,7 @@ set(MC_SRC_BASE
   src/mc/mc_base.cpp
   src/mc/mc_base.h
   src/mc/mc_record.h
+  src/mc/mc_replay.h
   src/mc/mc_record.cpp
   src/mc/mc_config.cpp
   src/mc/mc_global.cpp

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index 2cf3234..ff34bf3 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -10,6 +10,7 @@
 #include "xbt/asserts.h"
 #include "simgrid/modelchecker.h"
 #include <xbt/RngStream.h>
+#include "mc/mc_replay.h"
 
 /** @addtogroup MSG_examples
  *

diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh
index 0ebb4ec..cc85d75 100644 (file)
--- a/examples/smpi/mc/only_send_deterministic.tesh
+++ b/examples/smpi/mc/only_send_deterministic.tesh
@@ -2,7 +2,7 @@
 
 ! timeout 60
 $ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
-> [0.000000] [mc_global/INFO] Check communication determinism
+> [0.000000] [mc_comm_determinism/INFO] Check communication determinism
 > [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
 > [0.000000] [mc_global/INFO] ******************************************************
 > [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern ****

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 3cc7e2d..15b877d 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -17,17 +17,6 @@
 
 SG_BEGIN_DECL()
 
-/** Replay path (if any) in string representation
- *
- *  This is a path as generated by `MC_record_stack_to_string()`.
- */
-XBT_PUBLIC_DATA(char*) MC_record_path;
-
-/** Whether the replay mode is enabled */
-static inline bool MC_record_replay_is_active(void) {
-  return MC_record_path;
-}
-
 XBT_PUBLIC(int) MC_random(int min, int max);
 
 #ifdef HAVE_MC

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 23be47f..317ade9 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -73,7 +73,7 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos);
 void _mc_cfg_cb_send_determinism(const char *name, int pos);
 void _mc_cfg_cb_termination(const char *name, int pos);
 
-XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
+XBT_PUBLIC(void) MC_run(void);
 XBT_PUBLIC(void) MC_init(void);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index fd67dae..45a1b98 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -10,7 +10,8 @@
 
 #include "mc_base.h"
 #include "../simix/smx_private.h"
-#include "mc_record.h"
+#include "mc/mc_record.h"
+#include "mc/mc_replay.h"
 
 #ifdef HAVE_MC
 #include "mc_process.h"

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index e180720..192770f 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -25,12 +25,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
 void MC_assert(int prop)
 {
   if (MC_is_active() && !prop) {
-    if (mc_mode == MC_MODE_STANDALONE) {
-      MC_report_assertion_error();
-    } else {
-      MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
-      MC_client_handle_messages();
-    }
+    MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
+    MC_client_handle_messages();
   }
 }
 

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index ab30d5c..61b2027 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -501,6 +501,10 @@ static void MC_modelcheck_comm_determinism_main(void)
 
 void MC_modelcheck_comm_determinism(void)
 {
+  XBT_INFO("Check communication determinism");
+  mc_reduce_kind = e_mc_reduce_none;
+  MC_wait_for_requests();
+
   if (mc_mode == MC_MODE_CLIENT) {
     // This will move somehwere else:
     MC_client_handle_messages();

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 9239ba8..1169f2d 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -10,6 +10,7 @@
 #include <xbt/config.h>
 
 #include <mc/mc.h>
+#include "mc/mc_replay.h"
 
 #include <simgrid/sg_config.h>
 

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 28cbc9d..353eb42 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -106,17 +106,6 @@ static void MC_init_dot_output()
 
 }
 
-static void MC_init_mode(void)
-{
-  if (mc_mode == MC_MODE_NONE) {
-    if (getenv(MC_ENV_SOCKET_FD)) {
-      mc_mode = MC_MODE_CLIENT;
-    } else {
-      mc_mode = MC_MODE_STANDALONE;
-    }
-  }
-}
-
 #ifdef HAVE_MC
 void MC_init()
 {
@@ -196,7 +185,7 @@ void MC_init_pid(pid_t pid, int socket)
     /* SIMIX */
     MC_ignore_global_variable("smx_total_comms");
 
-    if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+    if (mc_mode == MC_MODE_CLIENT) {
       /* Those requests are handled on the client side and propagated by message
        * to the server: */
 
@@ -217,58 +206,13 @@ void MC_init_pid(pid_t pid, int socket)
 /*******************************  Core of MC *******************************/
 /**************************************************************************/
 
-void MC_do_the_modelcheck_for_real()
+void MC_run()
 {
-  MC_init_mode();
-
-  switch(mc_mode) {
-  default:
-    xbt_die("Unexpected mc mode");
-    break;
-  case MC_MODE_CLIENT:
-    MC_init();
-    MC_client_main_loop();
-    return;
-  case MC_MODE_SERVER:
-    break;
-  case MC_MODE_STANDALONE:
-    MC_init();
-    break;
-  }
-
-  if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    XBT_INFO("Check communication determinism");
-    mc_reduce_kind = e_mc_reduce_none;
-    MC_wait_for_requests();
-    MC_modelcheck_comm_determinism();
-  }
-
-  else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
-    if(_sg_mc_termination)
-      mc_reduce_kind = e_mc_reduce_none;
-    else if (mc_reduce_kind == e_mc_reduce_unset)
-      mc_reduce_kind = e_mc_reduce_dpor;
-    _sg_mc_safety = 1;
-    if (_sg_mc_termination)
-      XBT_INFO("Check non progressive cycles");
-    else
-      XBT_INFO("Check a safety property");
-    MC_wait_for_requests();
-    MC_modelcheck_safety();
-  }
-
-  else {
-    if (mc_reduce_kind == e_mc_reduce_unset)
-      mc_reduce_kind = e_mc_reduce_none;
-    XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
-    MC_automaton_load(_sg_mc_property_file);
-    MC_wait_for_requests();
-    MC_modelcheck_liveness();
-  }
-
+  mc_mode = MC_MODE_CLIENT;
+  MC_init();
+  MC_client_main_loop();
 }
 
-
 void MC_exit(void)
 {
   xbt_free(mc_time);

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 293eebd..41be27f 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -16,6 +16,8 @@
 #include "mc_record.h"
 #include "mc_smx.h"
 #include "mc_client.h"
+#include "mc_replay.h"
+#include "mc_safety.h"
 
 extern "C" {
 
@@ -405,6 +407,12 @@ static void MC_modelcheck_liveness_main(void)
 
 void MC_modelcheck_liveness(void)
 {
+  if (mc_reduce_kind == e_mc_reduce_unset)
+    mc_reduce_kind = e_mc_reduce_none;
+  XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
+  MC_automaton_load(_sg_mc_property_file);
+  MC_wait_for_requests();
+
   XBT_DEBUG("Starting the liveness algorithm");
   _sg_mc_liveness = 1;
 

diff --git a/src/mc/mc_model_checker.cpp b/src/mc/mc_model_checker.cpp
index 45b13b2..0484dd2 100644 (file)
--- a/src/mc/mc_model_checker.cpp
+++ b/src/mc/mc_model_checker.cpp
@@ -33,9 +33,6 @@ void MC_model_checker_delete(mc_model_checker_t mc)
 
 unsigned long MC_smx_get_maxpid(void)
 {
-  if (mc_mode == MC_MODE_STANDALONE)
-    return simix_process_maxpid;
-
   unsigned long maxpid;
   MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
     &maxpid, sizeof(maxpid));

diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp
index 2e5ffd3..01c4f9d 100644 (file)
--- a/src/mc/mc_protocol.cpp
+++ b/src/mc/mc_protocol.cpp
@@ -119,8 +119,6 @@ const char* MC_mode_name(e_mc_mode_t mode)
   switch(mode) {
   case MC_MODE_NONE:
     return "NONE";
-  case MC_MODE_STANDALONE:
-    return "STANDALONE";
   case MC_MODE_CLIENT:
     return "CLIENT";
   case MC_MODE_SERVER:

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index 6ad420b..722c71d 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -27,7 +27,6 @@ SG_BEGIN_DECL()
 
 typedef enum {
   MC_MODE_NONE = 0,
-  MC_MODE_STANDALONE,
   MC_MODE_CLIENT,
   MC_MODE_SERVER
 } e_mc_mode_t;

diff --git a/src/mc/mc_replay.h b/src/mc/mc_replay.h
new file mode 100644 (file)
index 0000000..2918305
--- /dev/null
+++ b/src/mc/mc_replay.h
@@ -0,0 +1,29 @@
+/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid    */
+
+/* Copyright (c) 2008-2014. 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 <xbt/misc.h>
+
+#ifndef SIMGRID_MC_REPLAY_H
+#define SIMGRID_MC_REPLAY_H
+
+SG_BEGIN_DECL()
+
+/** Replay path (if any) in string representation
+ *
+ *  This is a path as generated by `MC_record_stack_to_string()`.
+ */
+XBT_PUBLIC_DATA(char*) MC_record_path;
+
+/** Whether the replay mode is enabled */
+static inline int MC_record_replay_is_active(void) {
+  return MC_record_path != 0;
+}
+
+SG_END_DECL()
+
+#endif

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index 4717ab9..f05de06 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -272,6 +272,17 @@ static void MC_modelcheck_safety_main(void)
 
 void MC_modelcheck_safety(void)
 {
+  if(_sg_mc_termination)
+    mc_reduce_kind = e_mc_reduce_none;
+  else if (mc_reduce_kind == e_mc_reduce_unset)
+    mc_reduce_kind = e_mc_reduce_dpor;
+  _sg_mc_safety = 1;
+  if (_sg_mc_termination)
+    XBT_INFO("Check non progressive cycles");
+  else
+    XBT_INFO("Check a safety property");
+  MC_wait_for_requests();
+
   XBT_DEBUG("Starting the safety algorithm");
 
   _sg_mc_safety = 1;

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 71d0388..1e9d352 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -31,6 +31,8 @@
 #include "mc_server.h"
 #include "mc_model_checker.h"
 #include "mc_safety.h"
+#include "mc_comm_pattern.h"
+#include "mc_liveness.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 
@@ -82,7 +84,12 @@ static int do_parent(int socket, pid_t child)
     mc_server = new s_mc_server(child, socket);
     mc_server->start();
     MC_init_pid(child, socket);
-    MC_do_the_modelcheck_for_real();
+    if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+      MC_modelcheck_comm_determinism();
+    else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
+      MC_modelcheck_safety();
+    else
+      MC_modelcheck_liveness();
     mc_server->shutdown();
     mc_server->exit();
   }

diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index b9351e8..6deb895 100644 (file)
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -122,7 +122,7 @@ msg_error_t MSG_main(void)
   fflush(stderr);
 
   if (MC_is_active()) {
-    MC_do_the_modelcheck_for_real();
+    MC_run();
   } else {
     SIMIX_run();
   }

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index ad2bbb8..0ff07a2 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -22,6 +22,7 @@
 #include "mc/mc.h"
 #include "mc/mc_record.h"
 #include "simgrid/instr.h"
+#include "mc/mc_replay.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf,
                                 "About the configuration of simgrid");

diff --git a/src/simix/libsmx.c b/src/simix/libsmx.c
index 35b3c8e..17ff1ba 100644 (file)
--- a/src/simix/libsmx.c
+++ b/src/simix/libsmx.c
@@ -10,6 +10,7 @@
 /* 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 "mc/mc_replay.h"
 #include "smx_private.h"
 #include "mc/mc_interface.h"
 #include "xbt/ex.h"

diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index 0011f97..d0ba274 100644 (file)
--- a/src/simix/smx_global.c
+++ b/src/simix/smx_global.c
@@ -13,6 +13,7 @@
 #include "xbt/str.h"
 #include "xbt/ex.h"             /* ex_backtrace_display */
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "simgrid/sg_config.h"
 
 #ifdef HAVE_MC
@@ -220,8 +221,6 @@ void SIMIX_global_init(int *argc, char **argv)
       MC_client_init();
       MC_client_hello();
       MC_client_handle_messages();
-    } else {
-      mc_mode = MC_MODE_STANDALONE;
     }
   }
 #endif

diff --git a/src/simix/smx_host.c b/src/simix/smx_host.c
index be58fe5..20e7abb 100644 (file)
--- a/src/simix/smx_host.c
+++ b/src/simix/smx_host.c
@@ -9,6 +9,7 @@
 #include "xbt/log.h"
 #include "xbt/dict.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_host, simix,
                                 "SIMIX hosts");

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 942deb5..fbeb548 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -7,10 +7,10 @@
 #include "smx_private.h"
 #include "xbt/log.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "xbt/dict.h"
 #include "smpi/private.h"
 
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_network, simix,
                                 "SIMIX network-related synchronization");
 

diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c
index 8fa3c6b..8771f6e 100644 (file)
--- a/src/simix/smx_process.c
+++ b/src/simix/smx_process.c
@@ -9,6 +9,7 @@
 #include "xbt/log.h"
 #include "xbt/dict.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "mc/mc_client.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,

diff --git a/src/smpi/smpi_base.c b/src/smpi/smpi_base.c
index c75e51d..af7deeb 100644 (file)
--- a/src/smpi/smpi_base.c
+++ b/src/smpi/smpi_base.c
@@ -7,6 +7,7 @@
 #include "private.h"
 #include "xbt/virtu.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "xbt/replay.h"
 #include <errno.h>
 #include "simix/smx_private.h"

diff --git a/src/smpi/smpi_bench.c b/src/smpi/smpi_bench.c
index 35971e2..b6b56e8 100644 (file)
--- a/src/smpi/smpi_bench.c
+++ b/src/smpi/smpi_bench.c
@@ -13,6 +13,7 @@
 #include "surf/surf.h"
 #include "simgrid/sg_config.h"
 #include "simgrid/modelchecker.h"
+#include "mc/mc_replay.h"
 
 #ifndef WIN32
 #include <sys/mman.h>

diff --git a/src/smpi/smpi_global.c b/src/smpi/smpi_global.c
index ac3cd86..f47536e 100644 (file)
--- a/src/smpi/smpi_global.c
+++ b/src/smpi/smpi_global.c
@@ -12,6 +12,7 @@
 #include "surf/surf.h"
 #include "simix/smx_private.h"
 #include "simgrid/sg_config.h"
+#include "mc/mc_replay.h"
 
 #include <float.h>              /* DBL_MAX */
 #include <stdint.h>
@@ -666,7 +667,7 @@ int smpi_main(int (*realmain) (int argc, char *argv[]), int argc, char *argv[])
   fflush(stderr);
 
   if (MC_is_active()) {
-    MC_do_the_modelcheck_for_real();
+    MC_run();
   } else {
   
     SIMIX_run();