MC: inline a function, kill a file

diff --git a/MANIFEST.in b/MANIFEST.in
index baaaced..d7aef58 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2271,7 +2271,6 @@ include src/mc/mc_request.cpp
 include src/mc/mc_request.hpp
 include src/mc/mc_safety.hpp
 include src/mc/mc_smx.cpp
-include src/mc/mc_smx.hpp
 include src/mc/mc_state.cpp
 include src/mc/mc_state.hpp
 include src/mc/remote/AppSide.cpp

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 68a5565..2411431 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -8,9 +8,8 @@
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_pattern.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_smx.hpp"
-
 #include "src/mc/remote/RemoteSimulation.hpp"
+
 #include <xbt/asserts.h>
 #include <xbt/log.h>
 #include "simgrid/s4u/Host.hpp"
@@ -366,7 +365,12 @@ bool Api::actor_is_enabled(aid_t pid) const
 
 unsigned long Api::get_maxpid() const
 {
-  return MC_smx_get_maxpid();
+  unsigned long maxpid;
+  const char* name = "simgrid::kernel::actor::maxpid";
+  if (mc_model_checker->get_remote_simulation().find_variable(name) == nullptr)
+    name = "maxpid"; // We seem to miss the namespaces when compiling with GCC
+  mc_model_checker->get_remote_simulation().read_variable(name, &maxpid, sizeof(maxpid));
+  return maxpid;
 }
 
 int Api::get_actors_size() const

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 0ae988e..5192439 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -9,11 +9,6 @@
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_request.hpp"
-#include "src/mc/mc_smx.hpp"
-
-#if HAVE_SMPI
-#include "smpi_request.hpp"
-#endif
 
 #include <cstdint>
 

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 41ddff8..3171b6d 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -8,7 +8,6 @@
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_request.hpp"
-#include "src/mc/mc_smx.hpp"
 
 #include <boost/range/algorithm.hpp>
 #include <cstring>

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index daa7217..0c109f9 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -21,7 +21,6 @@
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
 #include "src/mc/mc_request.hpp"
-#include "src/mc/mc_smx.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 

diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp
index 72113c8..f97b598 100644 (file)
--- a/src/mc/compare.cpp
+++ b/src/mc/compare.cpp
@@ -7,7 +7,6 @@
 
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_smx.hpp"
 #include "src/mc/sosp/Snapshot.hpp"
 
 #include <algorithm>

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 53dec30..1549e4e 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -15,7 +15,6 @@
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_safety.hpp"
-#include "src/mc/mc_smx.hpp"
 #include "src/mc/remote/AppSide.hpp"
 #include "src/mc/sosp/Snapshot.hpp"
 

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index 6e3fd31..2afb21b 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -14,7 +14,6 @@
 #include "src/mc/checker/Checker.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_request.hpp"
-#include "src/mc/mc_smx.hpp"
 #include "src/mc/mc_state.hpp"
 #endif
 

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index a453f05..6c271aa 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -9,7 +9,8 @@
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/checker/SimcallObserver.hpp"
-#include "src/mc/mc_smx.hpp"
+#include "src/mc/remote/RemoteSimulation.hpp"
+
 #include <array>
 
 using simgrid::mc::remote;

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index 3079827..a1b7d6c 100644 (file)
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -6,9 +6,28 @@
 #include "simgrid/s4u/Host.hpp"
 
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/mc_smx.hpp"
+#include "src/mc/remote/RemoteSimulation.hpp"
 
 using simgrid::mc::remote;
+/** @file
+ *  @brief (Cross-process, MCer/MCed) Access to SMX structures
+ *
+ *  We copy some C data structure from the MCed process in the MCer process.
+ *  This is implemented by:
+ *
+ *   - `model_checker->process.smx_process_infos`
+ *      (copy of `simix_global->process_list`);
+ *
+ *   - `model_checker->process.smx_old_process_infos`
+ *      (copy of `simix_global->actors_to_destroy`);
+ *
+ *   - `model_checker->hostnames`.
+ *
+ * The process lists are currently refreshed each time MCed code is executed.
+ * We don't try to give a persistent MCer address for a given MCed process.
+ * For this reason, a MCer simgrid::mc::Process* is currently not reusable after
+ * MCed code.
+ */
 
 /** Load the remote list of processes into a vector
  *
@@ -71,13 +90,3 @@ void RemoteSimulation::refresh_simix()
 
 }
 }
-
-unsigned long MC_smx_get_maxpid()
-{
-  unsigned long maxpid;
-  const char* name = "simgrid::kernel::actor::maxpid";
-  if (mc_model_checker->get_remote_simulation().find_variable(name) == nullptr)
-    name = "maxpid"; // We seem to miss the namespaces when compiling with GCC
-  mc_model_checker->get_remote_simulation().read_variable(name, &maxpid, sizeof(maxpid));
-  return maxpid;
-}

diff --git a/src/mc/mc_smx.hpp b/src/mc/mc_smx.hpp
deleted file mode 100644 (file)
index a9a5a30..0000000
--- a/src/mc/mc_smx.hpp
+++ /dev/null
@@ -1,33 +0,0 @@
-/* Copyright (c) 2015-2021. 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. */
-
-#ifndef SIMGRID_MC_SMX_HPP
-#define SIMGRID_MC_SMX_HPP
-
-#include "src/mc/remote/RemoteSimulation.hpp"
-
-/** @file
- *  @brief (Cross-process, MCer/MCed) Access to SMX structures
- *
- *  We copy some C data structure from the MCed process in the MCer process.
- *  This is implemented by:
- *
- *   - `model_checker->process.smx_process_infos`
- *      (copy of `simix_global->process_list`);
- *
- *   - `model_checker->process.smx_old_process_infos`
- *      (copy of `simix_global->actors_to_destroy`);
- *
- *   - `model_checker->hostnames`.
- *
- * The process lists are currently refreshed each time MCed code is executed.
- * We don't try to give a persistent MCer address for a given MCed process.
- * For this reason, a MCer simgrid::mc::Process* is currently not reusable after
- * MCed code.
- */
-
-XBT_PRIVATE unsigned long MC_smx_get_maxpid();
-
-#endif

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index a0a16e6..91be2f5 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -7,6 +7,7 @@
 #include "src/internal_config.h"
 #include "src/kernel/actor/ActorImpl.hpp"
 #include "src/mc/checker/SimcallObserver.hpp"
+#include "src/mc/remote/RemoteSimulation.hpp"
 #include <simgrid/modelchecker.h>
 
 #include <cerrno>
@@ -17,9 +18,6 @@
 #include <sys/socket.h>
 #include <sys/types.h>
 
-// We won't need those once the separation MCer/MCed is complete:
-#include "src/mc/mc_smx.hpp"
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
 namespace simgrid {

diff --git a/src/mc/remote/RemoteSimulation.cpp b/src/mc/remote/RemoteSimulation.cpp
index 4024675..f2a3430 100644 (file)
--- a/src/mc/remote/RemoteSimulation.cpp
+++ b/src/mc/remote/RemoteSimulation.cpp
@@ -7,7 +7,6 @@
 
 #include "src/mc/remote/RemoteSimulation.hpp"
 
-#include "src/mc/mc_smx.hpp"
 #include "src/mc/sosp/Snapshot.hpp"
 #include "xbt/file.hpp"
 #include "xbt/log.h"

diff --git a/src/mc/sosp/Region.cpp b/src/mc/sosp/Region.cpp
index 89d0fdc..86d3452 100644 (file)
--- a/src/mc/sosp/Region.cpp
+++ b/src/mc/sosp/Region.cpp
@@ -3,12 +3,11 @@
 /* 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/sosp/Region.hpp"
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_forward.hpp"
-
-#include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/Region.hpp"
+#include "src/mc/remote/RemoteSimulation.hpp"
 
 #include <cstdlib>
 #include <sys/mman.h>

diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp
index 3dd017d..96ee900 100644 (file)
--- a/src/mc/sosp/Snapshot.cpp
+++ b/src/mc/sosp/Snapshot.cpp
@@ -6,7 +6,6 @@
 #include "src/mc/sosp/Snapshot.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_hash.hpp"
-#include "src/mc/mc_smx.hpp"
 
 #include <cstddef> /* std::size_t */
 

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 1a1c886..312882d 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -658,7 +658,6 @@ set(MC_SRC
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp
   src/mc/mc_client_api.cpp
-  src/mc/mc_smx.hpp
   src/mc/mc_smx.cpp
   src/mc/mc_exit.hpp
   src/mc/Transition.hpp