[mc] Remove redundant 'mc_mode' global variable

diff --git a/src/mc/Channel.cpp b/src/mc/Channel.cpp
index b368eaf..6902497 100644 (file)
--- a/src/mc/Channel.cpp
+++ b/src/mc/Channel.cpp
@@ -27,10 +27,8 @@ Channel::~Channel()
 
 int Channel::send(const void* message, size_t size) const
 {
-  XBT_DEBUG("Protocol [%s] send %s",
-    MC_mode_name(mc_mode),
+  XBT_DEBUG("Send %s",
     MC_message_type_name(*(e_mc_message_type*) message));
-
   while (::send(this->socket_, message, size, 0) == -1)
     if (errno == EINTR)
       continue;
@@ -43,8 +41,7 @@ ssize_t Channel::receive(void* message, size_t size, bool block) const
 {
   int res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
   if (res != -1)
-    XBT_DEBUG("Protocol [%s] received %s",
-      MC_mode_name(mc_mode),
+    XBT_DEBUG("Receive %s",
       MC_message_type_name(*(e_mc_message_type*) message));
   return res;
 }

diff --git a/src/mc/Client.cpp b/src/mc/Client.cpp
index c05696f..cf7398d 100644 (file)
--- a/src/mc/Client.cpp
+++ b/src/mc/Client.cpp
@@ -16,6 +16,8 @@
 #include <xbt/mmalloc.h>
 #include <xbt/swag.h>
 
+#include <simgrid/modelchecker.h>
+
 #include "src/internal_config.h"
 
 #include "src/mc/mc_protocol.h"
@@ -44,10 +46,7 @@ Client* Client::initialize()
   if (client_)
     return client_.get();
 
-  // Check and set the mode:
-  if (mc_mode != MC_MODE_NONE)
-    abort();
-  mc_mode = MC_MODE_CLIENT;
+  _sg_do_model_check = 1;
 
   // Fetch socket from MC_ENV_SOCKET_FD:
   char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
@@ -144,8 +143,7 @@ void Client::handleMessages()
       break;
 
     default:
-      xbt_die("%s received unexpected message %s (%i)",
-        MC_mode_name(mc_mode),
+      xbt_die("Received unexpected message %s (%i)",
         MC_message_type_name(message.type),
         message.type
       );

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index ea14a19..61a946d 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -476,9 +476,8 @@ bool ModelChecker::checkDeadlock()
   if (s == -1)
     xbt_die("Could not receive message");
   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
-    xbt_die("%s received unexpected message %s (%i, size=%i) "
+    xbt_die("Received unexpected message %s (%i, size=%i) "
       "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
-      MC_mode_name(mc_mode),
       MC_message_type_name(message.type), (int) message.type, (int) s,
       (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
       );

diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp
index 10bd3b5..8b96b0c 100644 (file)
--- a/src/mc/Process.hpp
+++ b/src/mc/Process.hpp
@@ -219,7 +219,7 @@ public:
   simgrid::mc::SimixProcessInformation* resolveProcessInfo(
     simgrid::mc::RemotePtr<s_smx_process_t> process)
   {
-    xbt_assert(mc_mode == MC_MODE_SERVER);
+    xbt_assert(mc_model_checker != nullptr);
     if (!process)
       return nullptr;
     this->refresh_simix();

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 42906fe..8112d2c 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -35,7 +35,7 @@ XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 
 int MC_random(int min, int max)
 {
-  xbt_assert(mc_mode != MC_MODE_SERVER);
+  xbt_assert(mc_model_checker == nullptr);
   /* TODO, if the MC is disabled we do not really need to make a simcall for
    * this :) */
   return simcall_mc_random(min, max);
@@ -46,7 +46,7 @@ namespace mc {
 
 void wait_for_requests(void)
 {
-  assert(mc_mode != MC_MODE_SERVER);
+  xbt_assert(mc_model_checker == nullptr);
 
   smx_process_t process;
   smx_simcall_t req;
@@ -81,7 +81,7 @@ bool request_is_enabled(smx_simcall_t req)
 
 #if HAVE_MC
     // Fetch from MCed memory:
-    if (mc_mode == MC_MODE_SERVER) {
+    if (mc_model_checker != nullptr) {
       mc_model_checker->process().read(&temp_synchro, remote(act));
       act = &temp_synchro;
     }
@@ -105,7 +105,7 @@ bool request_is_enabled(smx_simcall_t req)
 
     s_xbt_dynar_t comms_buffer;
     size_t buffer_size = 0;
-    if (mc_mode == MC_MODE_SERVER) {
+    if (mc_model_checker != nullptr) {
       // Read dynar:
       mc_model_checker->process().read(
         &comms_buffer, remote(simcall_comm_waitany__get__comms(req)));
@@ -117,7 +117,7 @@ bool request_is_enabled(smx_simcall_t req)
 
     // Read all the dynar buffer:
     char buffer[buffer_size];
-    if (mc_mode == MC_MODE_SERVER)
+    if (mc_model_checker != nullptr)
       mc_model_checker->process().read_bytes(buffer, sizeof(buffer),
         remote(comms->data));
 #else
@@ -127,7 +127,7 @@ bool request_is_enabled(smx_simcall_t req)
     for (index = 0; index < comms->used; ++index) {
 #if HAVE_MC
       // Fetch act from MCed memory:
-      if (mc_mode == MC_MODE_SERVER) {
+      if (mc_model_checker != nullptr) {
         memcpy(&act, buffer + comms->elmsize * index, sizeof(act));
         mc_model_checker->process().read(&temp_synchro, remote(act));
         act = &temp_synchro;
@@ -148,7 +148,7 @@ bool request_is_enabled(smx_simcall_t req)
     smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
 #if HAVE_MC
     s_smx_mutex_t temp_mutex;
-    if (mc_mode == MC_MODE_SERVER) {
+    if (mc_model_checker != nullptr) {
       mc_model_checker->process().read(&temp_mutex, remote(mutex));
       mutex = &temp_mutex;
     }
@@ -157,7 +157,7 @@ bool request_is_enabled(smx_simcall_t req)
     if(mutex->owner == nullptr)
       return true;
 #if HAVE_MC
-    else if (mc_mode == MC_MODE_SERVER) {
+    else if (mc_model_checker != nullptr) {
       simgrid::mc::Process& modelchecked = mc_model_checker->process();
       // TODO, *(mutex->owner) :/
       return modelchecked.resolveProcess(simgrid::mc::remote(mutex->owner))->pid

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index d8c9343..20d7248 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -618,8 +618,7 @@ void restore_snapshot_regions(simgrid::mc::Snapshot* snapshot)
 static inline
 void restore_snapshot_fds(simgrid::mc::Snapshot* snapshot)
 {
-  if (mc_mode == MC_MODE_SERVER)
-    xbt_die("FD snapshot not implemented in client/server mode.");
+  xbt_die("FD snapshot not implemented in client/server mode.");
 
   for (auto const& fd : snapshot->current_fds) {
     

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index d3fdc26..d12eeff 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -28,39 +28,41 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
 
 void MC_assert(int prop)
 {
+  xbt_assert(mc_model_checker == nullptr);
   if (MC_is_active() && !prop)
     simgrid::mc::Client::get()->reportAssertionFailure();
 }
 
 void MC_cut(void)
 {
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
+    return;
   // FIXME, We want to do this in the model-checker:
   xbt_die("MC_cut() not implemented");
 }
 
 void MC_ignore(void* addr, size_t size)
 {
-  xbt_assert(mc_mode != MC_MODE_SERVER);
-  if (mc_mode != MC_MODE_CLIENT)
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
     return;
   simgrid::mc::Client::get()->ignoreMemory(addr, size);
 }
 
 void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
 {
-  xbt_assert(mc_mode != MC_MODE_SERVER);
-  if (mc_mode != MC_MODE_CLIENT)
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
     return;
-
   xbt_die("Support for client-side function proposition is not implemented: "
-    "use MC_automaton_new_propositional_symbol_pointer instead."
-  );
+    "use MC_automaton_new_propositional_symbol_pointer instead.");
 }
 
 void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
 {
-  xbt_assert(mc_mode != MC_MODE_SERVER);
-  if (mc_mode != MC_MODE_CLIENT)
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
     return;
   simgrid::mc::Client::get()->declareSymbol(name, value);
 }
@@ -78,27 +80,33 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
  */
 void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size)
 {
-  if (mc_mode != MC_MODE_CLIENT)
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
     return;
   simgrid::mc::Client::get()->declareStack(stack, size, process, context);
 }
 
 void MC_ignore_global_variable(const char *name)
 {
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
+    return;
   // TODO, send a message to the model_checker
   xbt_die("Unimplemented");
 }
 
 void MC_ignore_heap(void *address, size_t size)
 {
-  if (mc_mode != MC_MODE_CLIENT)
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
     return;
   simgrid::mc::Client::get()->ignoreHeap(address, size);
 }
 
 void MC_remove_ignore_heap(void *address, size_t size)
 {
-  if (mc_mode != MC_MODE_CLIENT)
+  xbt_assert(mc_model_checker == nullptr);
+  if (!MC_is_active())
     return;
   simgrid::mc::Client::get()->unignoreHeap(address, size);
 }

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 5813e62..92d6e70 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -48,8 +48,6 @@
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
 
-e_mc_mode_t mc_mode;
-
 namespace simgrid {
 namespace mc {
 

diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp
index b19f993..b420e44 100644 (file)
--- a/src/mc/mc_protocol.cpp
+++ b/src/mc/mc_protocol.cpp
@@ -50,17 +50,3 @@ const char* MC_message_type_name(e_mc_message_type type)
     return "?";
   }
 }
-
-const char* MC_mode_name(e_mc_mode_t mode)
-{
-  switch(mode) {
-  case MC_MODE_NONE:
-    return "NONE";
-  case MC_MODE_CLIENT:
-    return "CLIENT";
-  case MC_MODE_SERVER:
-    return "SERVER";
-  default:
-    return "?";
-  }
-}

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index ac3c0db..e93295a 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -25,16 +25,6 @@ SG_BEGIN_DECL()
 /** Environment variable name used to pass the communication socket */
 #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
 
-// ***** MC mode
-
-typedef enum {
-  MC_MODE_NONE = 0,
-  MC_MODE_CLIENT,
-  MC_MODE_SERVER
-} e_mc_mode_t;
-
-extern e_mc_mode_t mc_mode;
-
 // ***** Messages
 
 typedef enum {
@@ -115,7 +105,6 @@ typedef struct s_mc_restore_message {
 } s_mc_restore_message_t, *mc_restore_message_t;
 
 XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);
-XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode);
 
 SG_END_DECL()
 

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index f3aaa70..a1c4361 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -205,7 +205,7 @@ static char *buff_size_to_string(size_t buff_size)
 
 std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
 {
-  xbt_assert(mc_mode == MC_MODE_SERVER);
+  xbt_assert(mc_model_checker != nullptr);
 
   bool use_remote_comm = true;
   switch(request_type) {

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index f1df2aa..8f821f4 100644 (file)
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -108,7 +108,7 @@ void Process::refresh_simix()
  */
 smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req)
 {
-  xbt_assert(mc_mode == MC_MODE_SERVER);
+  xbt_assert(mc_model_checker != nullptr);
 
   // This is the address of the smx_process in the MCed process:
   auto address = simgrid::mc::remote(req->issuer);
@@ -126,7 +126,7 @@ smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req)
 
 const char* MC_smx_process_get_host_name(smx_process_t p)
 {
-  if (mc_mode == MC_MODE_CLIENT)
+  if (mc_model_checker == nullptr)
     return sg_host_get_name(p->host);
 
   simgrid::mc::Process* process = &mc_model_checker->process();
@@ -164,7 +164,7 @@ const char* MC_smx_process_get_host_name(smx_process_t p)
 const char* MC_smx_process_get_name(smx_process_t p)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();
-  if (mc_mode == MC_MODE_CLIENT)
+  if (mc_model_checker == nullptr)
     return p->name;
   if (!p->name)
     return nullptr;
@@ -178,7 +178,7 @@ const char* MC_smx_process_get_name(smx_process_t p)
 #if HAVE_SMPI
 int MC_smpi_process_count(void)
 {
-  if (mc_mode == MC_MODE_CLIENT)
+  if (mc_model_checker == nullptr)
     return smpi_process_count();
   int res;
   mc_model_checker->process().read_variable("process_count",

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 9f85d7a..a115825 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -63,7 +63,6 @@ int main(int argc, char** argv)
 
     // Currently, we need this before sg_config_init:
     _sg_do_model_check = 1;
-    mc_mode = MC_MODE_SERVER;
 
     // The initialisation function can touch argv.
     // We make a copy of argv before modifying it in order to pass the original

diff --git a/src/simix/smx_global.cpp b/src/simix/smx_global.cpp
index 018b957..06f6dc8 100644 (file)
--- a/src/simix/smx_global.cpp
+++ b/src/simix/smx_global.cpp
@@ -190,7 +190,9 @@ void SIMIX_set_maestro(void (*code)(void*), void* data)
 void SIMIX_global_init(int *argc, char **argv)
 {
 #if HAVE_MC
-  _sg_do_model_check = getenv(MC_ENV_VARIABLE) != NULL;
+  // The communication initialization is done ASAP.
+  // We need to communicate  initialization of the different layers to the model-checker.
+  simgrid::mc::Client::initialize();
 #endif
 
   s_smx_process_t proc;
@@ -261,12 +263,6 @@ void SIMIX_global_init(int *argc, char **argv)
   if (xbt_cfg_get_boolean("clean-atexit"))
     atexit(SIMIX_clean);
 
-#if HAVE_MC
-  // The communication initialization is done ASAP.
-  // We need to communicate  initialization of the different layers to the model-checker.
-  simgrid::mc::Client::initialize();
-#endif
-
   if (_sg_cfg_exit_asap)
     exit(0);
 }