Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
further tidy the includes in MC
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 26 May 2019 21:17:00 +0000 (23:17 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 26 May 2019 21:17:00 +0000 (23:17 +0200)
28 files changed:
src/mc/ModelChecker.cpp
src/mc/ModelChecker.hpp
src/mc/Session.cpp
src/mc/Session.hpp
src/mc/VisitedState.cpp
src/mc/checker/Checker.cpp
src/mc/checker/Checker.hpp
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/checker/CommunicationDeterminismChecker.hpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/LivenessChecker.hpp
src/mc/checker/SafetyChecker.cpp
src/mc/checker/SafetyChecker.hpp
src/mc/checker/simgrid_mc.cpp
src/mc/mc_base.cpp
src/mc/mc_client_api.cpp
src/mc/mc_comm_pattern.cpp
src/mc/mc_comm_pattern.hpp
src/mc/mc_config.cpp
src/mc/mc_global.cpp
src/mc/mc_ignore.hpp
src/mc/mc_mmu.hpp
src/mc/mc_record.hpp
src/mc/mc_state.cpp
src/mc/mc_state.hpp
src/mc/remote/RemotePtr.hpp
src/mc/sosp/mc_snapshot.cpp
src/mc/sosp/mc_snapshot_test.cpp

index 26ec1db..2f38676 100644 (file)
@@ -3,26 +3,19 @@
 /* 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 <sys/types.h>
-#include <sys/wait.h>
-#include <sys/socket.h>
-#include <sys/ptrace.h>
-
-#include <memory>
-#include <system_error>
-
-#include "xbt/automaton.h"
-#include "xbt/automaton.hpp"
-#include "xbt/log.h"
-#include "xbt/system_error.hpp"
-
-#include "simgrid/sg_config.hpp"
-
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/Session.hpp"
 #include "src/mc/Transition.hpp"
 #include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/remote/RemoteClient.hpp"
+#include "xbt/automaton.hpp"
+#include "xbt/system_error.hpp"
+
+#include <sys/ptrace.h>
+#include <sys/wait.h>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
 
index d4de670..fec9f99 100644 (file)
@@ -6,7 +6,8 @@
 #ifndef SIMGRID_MC_MODEL_CHECKER_HPP
 #define SIMGRID_MC_MODEL_CHECKER_HPP
 
-#include <sys/types.h>
+#include "src/mc/sosp/PageStore.hpp"
+#include "xbt/base.h"
 
 #include <memory>
 #include <set>
 
 #include <event2/event.h>
 
-#include <sys/types.h>
-
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/remote/mc_protocol.h"
-#include "src/mc/sosp/PageStore.hpp"
-
 namespace simgrid {
 namespace mc {
 
index 3d62b73..8bb58f6 100644 (file)
@@ -3,23 +3,18 @@
 /* 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 <csignal>
-#include <fcntl.h>
-
-#include <functional>
-
-#include "xbt/log.h"
-#include "xbt/system_error.hpp"
-#include <mc/mc.h>
-#include <simgrid/modelchecker.h>
-#include <simgrid/sg_config.hpp>
-
 #include "src/mc/Session.hpp"
 #include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_state.hpp"
+#include "xbt/log.h"
+#include "xbt/system_error.hpp"
 
-#include "src/smpi/include/private.hpp"
+#include <fcntl.h>
+#ifdef __linux__
+#include <sys/prctl.h>
+#endif
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
 
index ddc75db..6806c0c 100644 (file)
@@ -6,22 +6,10 @@
 #ifndef SIMGRID_MC_SESSION_HPP
 #define SIMGRID_MC_SESSION_HPP
 
-#ifdef __linux__
-#include <sys/prctl.h>
-#endif
-
-#include "xbt/sysdep.h"
-#include "xbt/system_error.hpp"
-#include <sys/socket.h>
-#include <sys/types.h>
+#include "src/mc/ModelChecker.hpp"
 
 #include <functional>
 
-#include "xbt/log.h"
-
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/ModelChecker.hpp"
-
 namespace simgrid {
 namespace mc {
 
@@ -80,7 +68,7 @@ public:
   static Session* spawnvp(const char *file, char *const argv[]);
 };
 
-// Temporary
+// Temporary :)
 extern simgrid::mc::Session* session;
 
 }
index a17dbb4..5e4f99c 100644 (file)
@@ -3,22 +3,14 @@
 /* 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/VisitedState.hpp"
+#include "src/mc/mc_private.hpp"
+
 #include <unistd.h>
 #include <sys/wait.h>
-
 #include <memory>
-
 #include <boost/range/algorithm.hpp>
 
-#include "xbt/log.h"
-#include "xbt/sysdep.h"
-
-#include "src/mc/VisitedState.hpp"
-#include "src/mc/mc_comm_pattern.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_smx.hpp"
-#include "src/mc/remote/RemoteClient.hpp"
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state equality detection mechanisms");
 
 namespace simgrid {
index 6ca26a6..b34fbce 100644 (file)
@@ -4,12 +4,9 @@
 /* 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 <string>
-
-#include <xbt/asserts.h>
-
 #include "src/mc/checker/Checker.hpp"
 #include "src/mc/ModelChecker.hpp"
+#include "xbt/asserts.h"
 
 namespace simgrid {
 namespace mc {
index 96f5c36..96a1f20 100644 (file)
@@ -7,11 +7,7 @@
 #ifndef SIMGRID_MC_CHECKER_HPP
 #define SIMGRID_MC_CHECKER_HPP
 
-#include <functional>
-#include <memory>
-#include <string>
-
-#include "src/mc/Session.hpp"
+//#include "src/mc/Session.hpp"
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/mc_record.hpp"
 
index d08d529..c3bf8b1 100644 (file)
@@ -5,14 +5,12 @@
 
 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
 #include "src/kernel/activity/MailboxImpl.hpp"
-#include "src/mc/VisitedState.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #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/mc/mc_state.hpp"
-#include "src/mc/remote/Client.hpp"
 
 #if HAVE_SMPI
 #include "smpi_request.hpp"
index 72b4931..66181d8 100644 (file)
@@ -3,15 +3,12 @@
 /* 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 <list>
-#include <memory>
-#include <string>
-#include <vector>
-
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/checker/Checker.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
-#include "src/mc/mc_forward.hpp"
+
+#include <string>
+#include <vector>
 
 #ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
 #define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
index cd49a87..d70ac11 100644 (file)
@@ -3,32 +3,16 @@
 /* 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 <cstring>
-
-#include <memory>
-#include <list>
-
-#include <boost/range/algorithm.hpp>
-
-#include <unistd.h>
-#include <sys/wait.h>
-
-#include <xbt/automaton.h>
-#include <xbt/dynar.h>
-#include <xbt/log.h>
-#include <xbt/sysdep.h>
-
-#include "src/mc/Session.hpp"
-#include "src/mc/Transition.hpp"
 #include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_record.hpp"
-#include "src/mc/mc_replay.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_smx.hpp"
-#include "src/mc/remote/Client.hpp"
+
+#include <boost/range/algorithm.hpp>
+#include <cstring>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
 
index 25517a0..b37b475 100644 (file)
@@ -7,19 +7,14 @@
 #ifndef SIMGRID_MC_LIVENESS_CHECKER_HPP
 #define SIMGRID_MC_LIVENESS_CHECKER_HPP
 
-#include <cstddef>
+#include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_state.hpp"
+#include "xbt/automaton.hpp"
 
-#include <string>
 #include <list>
 #include <memory>
 #include <vector>
 
-#include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_state.hpp"
-#include <simgrid/config.h>
-#include <xbt/automaton.h>
-#include <xbt/base.h>
-
 namespace simgrid {
 namespace mc {
 
index faca5d2..e3c741b 100644 (file)
@@ -17,6 +17,7 @@
 #include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
index d7b5ce8..f615e6f 100644 (file)
@@ -7,16 +7,15 @@
 #ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
 #define SIMGRID_MC_SAFETY_CHECKER_HPP
 
+#include "src/mc/VisitedState.hpp"
+#include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_safety.hpp"
+
 #include <list>
 #include <memory>
 #include <string>
 #include <vector>
 
-#include "src/mc/VisitedState.hpp"
-#include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/mc_safety.hpp"
-
 namespace simgrid {
 namespace mc {
 
index d491627..0a713b8 100644 (file)
@@ -5,7 +5,9 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "simgrid/sg_config.hpp"
+#include "src/mc/Session.hpp"
 #include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 
 #include <cstring>
index ff7dbe3..76b2721 100644 (file)
@@ -5,11 +5,8 @@
 
 #include "src/mc/mc_base.h"
 #include "mc/mc.h"
-#include "simgrid/config.h"
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
-#include "src/mc/mc_config.hpp"
-#include "src/mc/mc_forward.hpp"
 #include "src/mc/mc_replay.hpp"
 #include "src/simix/smx_private.hpp"
 
index 2bfe6b5..bbce30f 100644 (file)
@@ -4,17 +4,13 @@
 /* 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/log.h"
-#include "xbt/sysdep.h"
-#include <simgrid/modelchecker.h>
-
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/mc_ignore.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
 #include "src/mc/mc_replay.hpp"
 #include "src/mc/remote/Client.hpp"
-#include "src/mc/remote/mc_protocol.h"
+#include "xbt/asserts.h"
 
 /** @file mc_client_api.cpp
  *
index 4cb33e3..8182faf 100644 (file)
@@ -5,11 +5,7 @@
 
 #include <cstring>
 
-#include "xbt/dynar.h"
-#include "xbt/sysdep.h"
-
 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
-#include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_smx.hpp"
 
 using simgrid::mc::remote;
index 204889e..15b9a72 100644 (file)
@@ -9,7 +9,6 @@
 #include <vector>
 
 #include "smpi/smpi.h"
-
 #include "src/mc/mc_state.hpp"
 
 namespace simgrid {
index b8de285..5f6568b 100644 (file)
@@ -3,22 +3,12 @@
 /* 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/config.hpp"
-#include "xbt/log.h"
-#include <xbt/sysdep.h>
-
 #include "src/mc/mc_replay.hpp"
-#include <mc/mc.h>
-
 #include <simgrid/sg_config.hpp>
-
 #if SIMGRID_HAVE_MC
-#include "src/mc/mc_private.hpp"
 #include "src/mc/mc_safety.hpp"
 #endif
 
-#include "src/mc/mc_record.hpp"
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, "Configuration of the Model Checker");
 
 #if SIMGRID_HAVE_MC
index 96a7012..b81b215 100644 (file)
@@ -3,30 +3,12 @@
 /* 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 <cinttypes>
-#include <cassert>
-#include <cstddef>
-#include <cstdint>
-
-#include <cxxabi.h>
-
-#include <vector>
-
-#include "xbt/automaton.h"
-#include "xbt/backtrace.hpp"
-#include "xbt/dynar.h"
-
-#include "mc_base.h"
-
 #include "mc/mc.h"
-
-#ifndef _WIN32
-#include <unistd.h>
-#include <sys/wait.h>
-#include <sys/time.h>
-#endif
-
 #include "src/kernel/actor/ActorImpl.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_config.hpp"
+#include "src/mc/remote/Client.hpp"
+#include "xbt/backtrace.hpp"
 
 #if SIMGRID_HAVE_MC
 #include "src/mc/checker/Checker.hpp"
 #include <libunwind.h>
 #endif
 
-#include "src/mc/Transition.hpp"
-#include "src/mc/mc_record.hpp"
-#include "src/mc/remote/Client.hpp"
-#include "src/mc/remote/mc_protocol.h"
+#ifndef _WIN32
+#include <sys/time.h>
+#include <sys/wait.h>
+#include <unistd.h>
+#endif
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
 
index bef60ce..1ede97a 100644 (file)
@@ -6,6 +6,7 @@
 #ifndef SIMGRID_MC_IGNORE_HPP
 #define SIMGRID_MC_IGNORE_HPP
 
+#include "simgrid/forward.h"
 #include "src/internal_config.h"
 
 #if HAVE_UCONTEXT_H
index cd920ce..21975e6 100644 (file)
@@ -35,7 +35,7 @@ static int chunk_size()
  */
 static XBT_ALWAYS_INLINE std::size_t chunk_count(std::size_t size)
 {
-  size_t page_count = size >> xbt_pagebits;
+  std::size_t page_count = size >> xbt_pagebits;
   if (size & (xbt_pagesize - 1))
     page_count++;
   return page_count;
index d4ead6f..85bf484 100644 (file)
 #ifndef SIMGRID_MC_RECORD_HPP
 #define SIMGRID_MC_RECORD_HPP
 
-#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_forward.hpp"
 #include "xbt/base.h"
 
+#include <string>
 #include <vector>
 
 namespace simgrid {
index 7f8fa6b..1dd1bda 100644 (file)
@@ -3,10 +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/mc_state.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_smx.hpp"
-#include "src/mc/mc_state.hpp"
 
 #include <boost/range/algorithm.hpp>
 
index bfdce90..a7a0fb3 100644 (file)
@@ -6,12 +6,7 @@
 #ifndef SIMGRID_MC_STATE_HPP
 #define SIMGRID_MC_STATE_HPP
 
-#include <list>
-#include <memory>
-
-#include "src/mc/mc_record.hpp"
 #include "src/mc/sosp/mc_snapshot.hpp"
-
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/mc/Transition.hpp"
 
index 2f51118..f7a87ca 100644 (file)
@@ -7,7 +7,6 @@
 #define SIMGRID_MC_REMOTE_PTR_HPP
 
 #include "src/simix/smx_private.hpp"
-#include <type_traits>
 
 namespace simgrid {
 namespace mc {
index e8d20cf..876f4cb 100644 (file)
@@ -3,24 +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 <cstddef>
+#include <cstddef> /* std::size_t */
 
-#include <memory>
-#include <utility>
-
-#include "xbt/asserts.h"
-#include "xbt/sysdep.h"
-
-#include "src/internal_config.h"
-#include "src/smpi/include/private.hpp"
-
-#include "src/mc/mc_mmu.hpp"
-#include "src/mc/mc_private.hpp"
 #include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/PageStore.hpp"
 #include "src/mc/sosp/mc_snapshot.hpp"
 
-
 /** @brief Read memory from a snapshot region broken across fragmented pages
  *
  *  @param addr    Process (non-snapshot) address of the data
index eb8a84d..1480c21 100644 (file)
@@ -4,18 +4,13 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/include/catch.hpp"
+#include "src/mc/mc_config.hpp"
+#include "src/mc/sosp/mc_snapshot.hpp"
 
-#include <cstdlib>
-#include <cstring>
+#include <cstddef>
 #include <random>
-
 #include <sys/mman.h>
 
-#include "src/mc/mc_config.hpp"
-#include "src/mc/mc_mmu.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
-
 /**************** Class BOOST_tests *************************/
 using simgrid::mc::RegionSnapshot;
 class snap_test_helper {