MC: various cleanups done while debugging something

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 7a51253..8079ed7 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -27,6 +27,10 @@ namespace mc {
 
 static void setup_child_environment(int socket)
 {
+  /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
+   * env variable is set. If so, MC mode is assumed, and the client is setup from its side
+   */
+
 #ifdef __linux__
   // Make sure we do not outlive our parent
   sigset_t mask;
@@ -75,7 +79,7 @@ Session::Session(const std::function<void()>& code)
     ::close(sockets[1]);
     setup_child_environment(sockets[0]);
     code();
-    xbt_die("The model-checked process failed to exec()");
+    xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
   }
 
   // Parent (model-checker):
@@ -95,6 +99,7 @@ Session::~Session()
   this->close();
 }
 
+/** Take the initial snapshot of the application, that must be stopped. */
 void Session::initialize()
 {
   xbt_assert(initial_snapshot_ == nullptr);
@@ -123,7 +128,8 @@ void Session::log_state()
   }
   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
     int ret=system("free");
-    if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
+    if (ret != 0)
+      XBT_WARN("Call to system(free) did not return 0, but %d", ret);
   }
 }
 

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 070192e..ebd1a91 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -525,7 +525,6 @@ void CommunicationDeterminismChecker::run()
   mc::session->initialize();
 
   this->prepare();
-
   this->real_run();
 }
 

diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp
index 07c0541..d8544e5 100644 (file)
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/checker/simgrid_mc.cpp
@@ -47,12 +47,11 @@ int main(int argc, char** argv)
   _sg_do_model_check = 1;
 
   // The initialization function can touch argv.
-  // We make a copy of argv before modifying it in order to pass the original
-  // value to the model-checked:
+  // We make a copy of argv before modifying it in order to pass the original value to the model-checked application:
   char** argv_copy = argvdup(argc, argv);
   xbt_log_init(&argc, argv);
 #if HAVE_SMPI
-  smpi_init_options();//only performed once
+  smpi_init_options(); // only performed once
 #endif
   sg_config_init(&argc, argv);
   simgrid::mc::session = new simgrid::mc::Session([argv_copy] {
@@ -65,8 +64,8 @@ int main(int argc, char** argv)
   });
   delete[] argv_copy;
 
-  std::unique_ptr<simgrid::mc::Checker> checker = create_checker(*simgrid::mc::session);
-  int res                                       = SIMGRID_MC_EXIT_SUCCESS;
+  auto checker = create_checker(*simgrid::mc::session);
+  int res      = SIMGRID_MC_EXIT_SUCCESS;
   try {
     checker->run();
   } catch (const simgrid::mc::DeadlockError&) {

diff --git a/src/mc/remote/RemoteClient.cpp b/src/mc/remote/RemoteClient.cpp
index fae0571..93e655a 100644 (file)
--- a/src/mc/remote/RemoteClient.cpp
+++ b/src/mc/remote/RemoteClient.cpp
@@ -220,16 +220,13 @@ void RemoteClient::init()
   this->init_memory_map_info();
 
   int fd = open_vm(this->pid_, O_RDWR);
-  if (fd < 0)
-    xbt_die("Could not open file for process virtual address space");
+  xbt_assert(fd >= 0, "Could not open file for process virtual address space");
   this->memory_file = fd;
 
   // Read std_heap (is a struct mdesc*):
   const simgrid::mc::Variable* std_heap_var = this->find_variable("__mmalloc_default_mdp");
-  if (not std_heap_var)
-    xbt_die("No heap information in the target process");
-  if (not std_heap_var->address)
-    xbt_die("No constant address for this variable");
+  xbt_assert(std_heap_var, "No heap information in the target process");
+  xbt_assert(std_heap_var->address, "No constant address for this variable");
   this->read_bytes(&this->heap_address, sizeof(mdesc*), remote(std_heap_var->address));
 
   this->smx_actors_infos.clear();