/* 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");
#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 {
/* 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");
#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 {
static Session* spawnvp(const char *file, char *const argv[]);
};
-// Temporary
+// Temporary :)
extern simgrid::mc::Session* session;
}
/* 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 {
/* 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 {
#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"
#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"
/* 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
/* 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");
#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 {
#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"
#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 {
* 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>
#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"
/* 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
*
#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;
#include <vector>
#include "smpi/smpi.h"
-
#include "src/mc/mc_state.hpp"
namespace simgrid {
/* 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
/* 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)");
#ifndef SIMGRID_MC_IGNORE_HPP
#define SIMGRID_MC_IGNORE_HPP
+#include "simgrid/forward.h"
#include "src/internal_config.h"
#if HAVE_UCONTEXT_H
*/
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;
#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 {
/* 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>
#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"
#define SIMGRID_MC_REMOTE_PTR_HPP
#include "src/simix/smx_private.hpp"
-#include <type_traits>
namespace simgrid {
namespace mc {
/* 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
* 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 {