Finally kill the now empty ModelChecker class

diff --git a/MANIFEST.in b/MANIFEST.in
index 24bc955..3bd5a10 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2147,8 +2147,6 @@ include src/kernel/xml/simgrid.dtd
 include src/kernel/xml/simgrid_dtd.c
 include src/kernel/xml/simgrid_dtd.h
 include src/mc/AddressSpace.hpp
-include src/mc/ModelChecker.cpp
-include src/mc/ModelChecker.hpp
 include src/mc/VisitedState.cpp
 include src/mc/VisitedState.hpp
 include src/mc/api/ActorState.hpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
deleted file mode 100644 (file)
index a1b1a81..0000000
--- a/src/mc/ModelChecker.cpp
+++ /dev/null
@@ -1,28 +0,0 @@
-/* Copyright (c) 2008-2023. 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 "src/mc/ModelChecker.hpp"
-#include "src/mc/explo/Exploration.hpp"
-#include "src/mc/explo/LivenessChecker.hpp"
-#include "src/mc/mc_config.hpp"
-#include "src/mc/mc_exit.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/sosp/RemoteProcessMemory.hpp"
-#include "src/mc/transition/TransitionComm.hpp"
-#include "xbt/automaton.hpp"
-#include "xbt/system_error.hpp"
-
-#include <array>
-#include <csignal>
-#include <sys/ptrace.h>
-#include <sys/wait.h>
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
-
-::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
-
-namespace simgrid::mc {
-
-} // namespace simgrid::mc

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
deleted file mode 100644 (file)
index d881e64..0000000
--- a/src/mc/ModelChecker.hpp
+++ /dev/null
@@ -1,30 +0,0 @@
-/* Copyright (c) 2007-2023. 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_MODEL_CHECKER_HPP
-#define SIMGRID_MC_MODEL_CHECKER_HPP
-
-#include "src/mc/remote/CheckerSide.hpp"
-#include "src/mc/remote/RemotePtr.hpp"
-#include "src/mc/sosp/PageStore.hpp"
-#include "xbt/base.h"
-
-#include <memory>
-
-namespace simgrid::mc {
-
-/** State of the model-checker (global variables for the model checker)
- */
-class ModelChecker {
-
-public:
-  ModelChecker(ModelChecker const&) = delete;
-  ModelChecker& operator=(ModelChecker const&) = delete;
-  explicit ModelChecker()                      = default;
-};
-
-} // namespace simgrid::mc
-
-#endif

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index c680ae4..131aec5 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -123,12 +123,8 @@ RemoteApp::RemoteApp(const std::vector<char*>& args)
   // Parent (model-checker):
   ::close(sockets[0]);
 
-  xbt_assert(mc_model_checker == nullptr, "Did you manage to start the MC twice in this process?");
-
   auto memory      = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid);
-  model_checker_   = std::make_unique<simgrid::mc::ModelChecker>();
-  mc_model_checker = model_checker_.get();
-  checker_side_    = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], std::move(memory), model_checker_.get());
+  checker_side_    = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], std::move(memory));
 
   start();
 
@@ -140,11 +136,7 @@ RemoteApp::RemoteApp(const std::vector<char*>& args)
 RemoteApp::~RemoteApp()
 {
   initial_snapshot_ = nullptr;
-  if (model_checker_) {
-    shutdown();
-    model_checker_   = nullptr;
-    mc_model_checker = nullptr;
-  }
+  shutdown();
 }
 void RemoteApp::start()
 {

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 948cb53..026353c 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -7,9 +7,10 @@
 #define SIMGRID_MC_REMOTE_APP_HPP
 
 #include "simgrid/forward.h"
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/api/ActorState.hpp"
+#include "src/mc/remote/CheckerSide.hpp"
 #include "src/mc/remote/RemotePtr.hpp"
+#include "src/mc/sosp/PageStore.hpp"
 
 #include <functional>
 
@@ -26,7 +27,6 @@ namespace simgrid::mc {
 class XBT_PUBLIC RemoteApp {
 private:
   std::unique_ptr<CheckerSide> checker_side_;
-  std::unique_ptr<ModelChecker> model_checker_;
   PageStore page_store_{500};
   std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
 

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index 02a0016..2440c09 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -38,6 +38,7 @@ Exploration::~Exploration()
 {
   if (dot_output_ != nullptr)
     fclose(dot_output_);
+  instance_ = nullptr;
 }
 
 void Exploration::dot_output(const char* fmt, ...)

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index c21dc14..acd042d 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -13,7 +13,6 @@
 #include "src/mc/mc_replay.hpp"
 
 #if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/api/RemoteApp.hpp"
 #include "src/mc/remote/AppSide.hpp"
 #include "src/mc/sosp/RemoteProcessMemory.hpp"

diff --git a/src/mc/mc_forward.hpp b/src/mc/mc_forward.hpp
index 45fefd7..6922bd7 100644 (file)
--- a/src/mc/mc_forward.hpp
+++ b/src/mc/mc_forward.hpp
@@ -15,7 +15,6 @@ namespace simgrid::mc {
 
 class PageStore;
 class ChunkedData;
-class ModelChecker;
 class AddressSpace;
 class RemoteProcessMemory;
 class Snapshot;
@@ -30,7 +29,4 @@ class Session;
 class Exploration;
 } // namespace simgrid::mc
 
-// TODO, try to get rid of the global ModelChecker variable
-extern simgrid::mc::ModelChecker* mc_model_checker;
-
 #endif

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index 5f04d15..b455df1 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -4,7 +4,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/remote/CheckerSide.hpp"
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/sosp/RemoteProcessMemory.hpp"
 #include "xbt/system_error.hpp"
 #include <csignal>
@@ -13,7 +12,7 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkerside, mc, "MC communication with the application");
 
 namespace simgrid::mc {
-CheckerSide::CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> memory, ModelChecker* mc)
+CheckerSide::CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> memory)
     : remote_memory_(std::move(memory)), channel_(sockfd)
 {
   auto* base = event_base_new();

diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp
index 2d0aa94..0c32948 100644 (file)
--- a/src/mc/remote/CheckerSide.hpp
+++ b/src/mc/remote/CheckerSide.hpp
@@ -23,7 +23,7 @@ class CheckerSide {
   Channel channel_;
 
 public:
-  explicit CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> mem, ModelChecker* mc);
+  explicit CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> mem);
 
   // No copy:
   CheckerSide(CheckerSide const&) = delete;

diff --git a/src/mc/sosp/Region.cpp b/src/mc/sosp/Region.cpp
index f8161c3..acbc080 100644 (file)
--- a/src/mc/sosp/Region.cpp
+++ b/src/mc/sosp/Region.cpp
@@ -4,7 +4,6 @@
  * 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/sosp/RemoteProcessMemory.hpp"

diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp
index 6fde410..04e871c 100644 (file)
--- a/src/mc/sosp/Snapshot.hpp
+++ b/src/mc/sosp/Snapshot.hpp
@@ -6,7 +6,6 @@
 #ifndef SIMGRID_MC_SNAPSHOT_HPP
 #define SIMGRID_MC_SNAPSHOT_HPP
 
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/inspect/mc_unw.hpp"
 #include "src/mc/sosp/Region.hpp"
 #include "src/mc/sosp/RemoteProcessMemory.hpp"

diff --git a/src/mc/sosp/Snapshot_test.cpp b/src/mc/sosp/Snapshot_test.cpp
index a5cefbc..0883e1e 100644 (file)
--- a/src/mc/sosp/Snapshot_test.cpp
+++ b/src/mc/sosp/Snapshot_test.cpp
@@ -152,13 +152,15 @@ void snap_test_helper::compare_region_parts()
   }
 }
 
+int some_global_variable  = 42;
+void* some_global_pointer = &some_global_variable;
 void snap_test_helper::read_pointer()
 {
   prologue_return ret = prologue(1);
-  memcpy(ret.src, &mc_model_checker, sizeof(void*));
+  memcpy(ret.src, &some_global_pointer, sizeof(void*));
   const simgrid::mc::Region region2(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, ret.src, ret.size);
   INFO("Mismtach in MC_region_read_pointer()");
-  REQUIRE(MC_region_read_pointer(&region2, ret.src) == mc_model_checker);
+  REQUIRE(MC_region_read_pointer(&region2, ret.src) == some_global_pointer);
 
   munmap(ret.dstn, ret.size);
   munmap(ret.src, ret.size);

diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp
index 70d94bb..f2ce4ab 100644 (file)
--- a/src/mc/transition/Transition.cpp
+++ b/src/mc/transition/Transition.cpp
@@ -10,7 +10,6 @@
 #include <simgrid/config.h>
 
 #if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/transition/TransitionActorJoin.hpp"
 #include "src/mc/transition/TransitionAny.hpp"

diff --git a/src/mc/transition/TransitionActorJoin.cpp b/src/mc/transition/TransitionActorJoin.cpp
index ef9874a..49331de 100644 (file)
--- a/src/mc/transition/TransitionActorJoin.cpp
+++ b/src/mc/transition/TransitionActorJoin.cpp
@@ -8,7 +8,6 @@
 #include "xbt/asserts.h"
 #include "xbt/string.hpp"
 #if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/api/RemoteApp.hpp"
 #include "src/mc/api/State.hpp"
 #endif

diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp
index 20f28d7..0f10bb1 100644 (file)
--- a/src/mc/transition/TransitionAny.cpp
+++ b/src/mc/transition/TransitionAny.cpp
@@ -8,7 +8,6 @@
 #include "xbt/asserts.h"
 #include "xbt/string.hpp"
 #if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/api/RemoteApp.hpp"
 #include "src/mc/api/State.hpp"
 #endif

diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp
index 512519b..376c301 100644 (file)
--- a/src/mc/transition/TransitionComm.cpp
+++ b/src/mc/transition/TransitionComm.cpp
@@ -8,7 +8,6 @@
 #include "xbt/asserts.h"
 #include "xbt/string.hpp"
 #if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
 #include "src/mc/api/RemoteApp.hpp"
 #include "src/mc/api/State.hpp"
 #endif

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 6bd5ec3..6ed5d73 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -607,8 +607,6 @@ set(MC_SRC
   src/mc/api/RemoteApp.hpp
 
   src/mc/AddressSpace.hpp
-  src/mc/ModelChecker.cpp
-  src/mc/ModelChecker.hpp
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp
   src/mc/compare.cpp