public:
/** @brief Seal your AS once you're done adding content, and before routing stuff through it */
- virtual void Seal();
+ virtual void seal();
char *name();
As *father();;
xbt_dict_t children(); // Sub AS
#include <system_error>
+#ifndef SIMGRID_MC_SYSTEM_ERROR_HPP
+#define SIMGRID_MC_SYSTEM_ERROR_HPP
+
namespace simgrid {
namespace xbt {
}
}
+
+#endif
extern XBT_PRIVATE char* _sg_mc_dot_output_file;
extern XBT_PUBLIC(int) _sg_mc_comms_determinism;
extern XBT_PUBLIC(int) _sg_mc_send_determinism;
-extern XBT_PRIVATE int _sg_mc_safety;
extern XBT_PRIVATE int _sg_mc_liveness;
extern XBT_PRIVATE int _sg_mc_snapshot_fds;
extern XBT_PRIVATE int _sg_mc_termination;
--- /dev/null
+/* Copyright (c) 2016. 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/Checker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+Checker::~Checker()
+{
+}
+
+FunctionalChecker::~FunctionalChecker()
+{
+}
+
+int FunctionalChecker::run()
+{
+ return function_(*session_);
+}
+
+}
+}
--- /dev/null
+/* Copyright (c) 2016. 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_CHECKER_HPP
+#define SIMGRID_MC_CHECKER_HPP
+
+#include <functional>
+#include <memory>
+
+#include "src/mc/mc_forward.hpp"
+
+namespace simgrid {
+namespace mc {
+
+/** A model-checking algorithm
+ *
+ * The goal is to move the data/state/configuration of a model-checking
+ * algorihms in subclasses. Implementing this interface will probably
+ * not be really mandatory, you might be able to write your
+ * model-checking algorithm as plain imperative code instead.
+ *
+ * It works by manipulating a model-checking Session.
+ */
+// abstract
+class Checker {
+ Session* session_;
+public:
+ Checker(Session& session) : session_(&session) {}
+
+ // No copy:
+ Checker(Checker const&) = delete;
+ Checker& operator=(Checker const&) = delete;
+
+ virtual ~Checker();
+ virtual int run() = 0;
+
+protected:
+ Session& getSession() { return *session_; }
+};
+
+/** Adapt a std::function to a checker */
+class FunctionalChecker : public Checker {
+ Session* session_;
+ std::function<int(Session& session)> function_;
+public:
+ FunctionalChecker(Session& session, std::function<int(Session& session)> f)
+ : Checker(session), function_(std::move(f)) {}
+ ~FunctionalChecker();
+ int run() override;
+};
+
+}
+}
+
+#endif
-/* Copyright (c) 2008-2015. The SimGrid Team.
+/* Copyright (c) 2016. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
#include "src/mc/mc_smx.h"
#include "src/mc/Client.hpp"
#include "src/mc/mc_exit.h"
+#include "src/mc/Checker.hpp"
+#include "src/mc/SafetyChecker.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
return 0;
}
-static void modelcheck_safety_init(void);
-
/**
* \brief Initialize the DPOR exploration algorithm
*/
-static void pre_modelcheck_safety()
+void SafetyChecker::pre()
{
simgrid::mc::visited_states.clear();
for (auto& p : mc_model_checker->process().simix_processes())
if (simgrid::mc::process_is_enabled(&p.copy)) {
MC_state_interleave_process(initial_state, &p.copy);
- if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
+ if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
xbt_fifo_unshift(mc_stack, initial_state);
}
-
-/** \brief Model-check the application using a DFS exploration
- * with DPOR (Dynamic Partial Order Reductions)
- */
-int modelcheck_safety(void)
+int SafetyChecker::run()
{
- modelcheck_safety_init();
+ this->init();
char *req_str = nullptr;
int value;
return SIMGRID_MC_EXIT_NON_TERMINATION;
}
- if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
+ if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
if (simgrid::mc::process_is_enabled(&p.copy)) {
MC_state_interleave_process(next_state, &p.copy);
- if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
+ if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
state that executed that previous request. */
while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
- if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::dpor) {
+ if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
req = MC_state_get_internal_request(state);
if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
xbt_die("Mutex is currently not supported with DPOR, "
"use --cfg=model-check/reduction:none");
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
- if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
+ if (reductionMode_ != simgrid::mc::ReductionMode::none
+ && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
return SIMGRID_MC_EXIT_SUCCESS;
}
-static void modelcheck_safety_init(void)
+void SafetyChecker::init()
{
- if(_sg_mc_termination)
- simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
- else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
- simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
- _sg_mc_safety = 1;
+ reductionMode_ = simgrid::mc::reduction_mode;
+ if( _sg_mc_termination)
+ reductionMode_ = simgrid::mc::ReductionMode::none;
+ else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
+ reductionMode_ = simgrid::mc::ReductionMode::dpor;
+
if (_sg_mc_termination)
XBT_INFO("Check non progressive cycles");
else
XBT_DEBUG("Starting the safety algorithm");
- _sg_mc_safety = 1;
-
/* Create exploration stack */
mc_stack = xbt_fifo_new();
- pre_modelcheck_safety();
+ this->pre();
/* Save the initial state */
initial_global_state = xbt_new0(s_mc_global_t, 1);
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
}
+SafetyChecker::SafetyChecker(Session& session) : Checker(session)
+{
+}
+
+SafetyChecker::~SafetyChecker()
+{
+}
+
}
}
--- /dev/null
+/* Copyright (c) 2008-2016. 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_SAFETY_CHECKER_HPP
+#define SIMGRID_MC_SAFETY_CHECKER_HPP
+
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/Checker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class SafetyChecker : public Checker {
+ simgrid::mc::ReductionMode reductionMode_ = simgrid::mc::ReductionMode::unset;
+public:
+ SafetyChecker(Session& session);
+ ~SafetyChecker();
+ int run() override;
+private:
+ // Temp
+ void init();
+ void pre();
+};
+
+}
+}
+
+#endif
--- /dev/null
+/* Copyright (c) 2015-2016. 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 <fcntl.h>
+#include <signal.h>
+
+#include <functional>
+
+#include <xbt/system_error.hpp>
+#include <simgrid/sg_config.h>
+#include <simgrid/modelchecker.h>
+
+#include "src/mc/Session.hpp"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
+
+namespace simgrid {
+namespace mc {
+
+static void setup_child_environment(int socket)
+{
+#ifdef __linux__
+ // Make sure we do not outlive our parent:
+ sigset_t mask;
+ sigemptyset (&mask);
+ if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
+ throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
+ if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
+ throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
+#endif
+
+ int res;
+
+ // Remove CLOEXEC in order to pass the socket to the exec-ed program:
+ int fdflags = fcntl(socket, F_GETFD, 0);
+ if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
+ throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
+
+ // Set environment:
+ setenv(MC_ENV_VARIABLE, "1", 1);
+
+ // Disable lazy relocation in the model-checked process.
+ // We don't want the model-checked process to modify its .got.plt during
+ // snapshot.
+ setenv("LC_BIND_NOW", "1", 1);
+
+ char buffer[64];
+ res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
+ if ((size_t) res >= sizeof(buffer) || res == -1)
+ std::abort();
+ setenv(MC_ENV_SOCKET_FD, buffer, 1);
+}
+
+/** Execute some code in a forked process */
+template<class F>
+static inline
+pid_t do_fork(F code)
+{
+ pid_t pid = fork();
+ if (pid < 0)
+ throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
+ if (pid != 0)
+ return pid;
+
+ // Child-process:
+ try {
+ code();
+ _exit(EXIT_SUCCESS);
+ }
+ catch(...) {
+ // The callback should catch exceptions:
+ std::terminate();
+ }
+}
+
+Session::Session(pid_t pid, int socket)
+{
+ std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(pid, socket));
+ // TODO, automatic detection of the config from the process
+ process->privatized(
+ sg_cfg_get_boolean("smpi/privatize_global_variables"));
+ modelChecker_ = std::unique_ptr<ModelChecker>(
+ new simgrid::mc::ModelChecker(std::move(process)));
+ xbt_assert(mc_model_checker == nullptr);
+ mc_model_checker = modelChecker_.get();
+ mc_model_checker->start();
+}
+
+Session::~Session()
+{
+ this->close();
+}
+
+// static
+Session* Session::fork(std::function<void(void)> code)
+{
+ // Create a AF_LOCAL socketpair used for exchanging messages
+ // bewteen the model-checker process (ourselves) and the model-checked
+ // process:
+ int res;
+ int sockets[2];
+ res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
+ if (res == -1)
+ throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
+
+ pid_t pid = do_fork([&] {
+ ::close(sockets[1]);
+ setup_child_environment(sockets[0]);
+ code();
+ xbt_die("The model-checked process failed to exec()");
+ });
+
+ // Parent (model-checker):
+ ::close(sockets[0]);
+
+ return new Session(pid, sockets[1]);
+}
+
+// static
+Session* Session::spawnv(const char *path, char *const argv[])
+{
+ return Session::fork([&] {
+ execv(path, argv);
+ });
+}
+
+// static
+Session* Session::spawnvp(const char *path, char *const argv[])
+{
+ return Session::fork([&] {
+ execvp(path, argv);
+ });
+}
+
+void Session::close()
+{
+ if (modelChecker_) {
+ modelChecker_->shutdown();
+ modelChecker_ = nullptr;
+ mc_model_checker = nullptr;
+ }
+}
+
+simgrid::mc::Session* session;
+
+}
+}
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2016. 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_SESSION_HPP
+#define SIMGRID_MC_SESSION_HPP
+
+#ifdef __linux__
+#include <sys/prctl.h>
+#endif
+
+#include <sys/types.h>
+#include <sys/socket.h>
+#include <xbt/sysdep.h>
+#include <xbt/system_error.hpp>
+
+#include <functional>
+
+#include <xbt/log.h>
+
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/ModelChecker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+/** A model-checking session
+ *
+ * This is expected to become the interface used by model-checking
+ * algorithms to control the execution of the model-checked process
+ * and the exploration of the execution graph. Model-checking
+ * algorithms should be able to be written in high-level languages
+ * (e.g. Python) using bindings on this interface.
+ */
+class Session {
+private:
+ std::unique_ptr<ModelChecker> modelChecker_;
+
+private: //
+ Session(pid_t pid, int socket);
+
+ // No copy:
+ Session(Session const&) = delete;
+ Session& operator=(Session const&) = delete;
+
+public:
+ ~Session();
+ void close();
+
+public: // static constructors
+
+ /** Create a new session by forking
+ *
+ * The code is expected to `exec` the model-checker program.
+ */
+ static Session* fork(std::function<void(void)> code);
+
+ /** Create a session using `execv` */
+ static Session* spawnv(const char *path, char *const argv[]);
+
+ /** Create a session using `execvp` */
+ static Session* spawnvp(const char *path, char *const argv[]);
+};
+
+// Temporary
+extern simgrid::mc::Session* session;
+
+}
+}
+
+#endif
xbt_fifo_unshift(mc_stack, initial_state);
}
+static inline
+bool all_communications_are_finished()
+{
+ for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
+ xbt_dynar_t pattern = xbt_dynar_get_as(
+ incomplete_communications_pattern, current_process, xbt_dynar_t);
+ if (!xbt_dynar_is_empty(pattern)) {
+ XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
+ return false;
+ }
+ }
+ return true;
+}
+
static int MC_modelcheck_comm_determinism_main(void)
{
/* Create the new expanded state */
next_state = MC_state_new();
- if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
+ /* If comm determinism verification, we cannot stop the exploration if
+ some communications are not finished (at least, data are transfered).
+ These communications are incomplete and they cannot be analyzed and
+ compared with the initial pattern. */
+ bool compare_snapshots = all_communications_are_finished()
+ && initial_global_state->initial_communications_pattern_done;
+
+ if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
/* Get enabled processes and insert them in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
int MC_modelcheck_comm_determinism(void)
{
XBT_INFO("Check communication determinism");
- simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
mc_model_checker->wait_for_requests();
if (mc_mode == MC_MODE_CLIENT)
using simgrid::mc::ComparisonState;
-extern "C" {
-
/************************** Snapshot comparison *******************************/
/******************************************************************************/
return 0;
}
-int snapshot_compare(void *state1, void *state2)
+namespace simgrid {
+namespace mc {
+
+int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2)
{
simgrid::mc::Process* process = &mc_model_checker->process();
- simgrid::mc::Snapshot* s1;
- simgrid::mc::Snapshot* s2;
- int num1, num2;
-
- if (_sg_mc_liveness) { /* Liveness MC */
- s1 = ((simgrid::mc::VisitedPair*) state1)->graph_state->system_state;
- s2 = ((simgrid::mc::VisitedPair*) state2)->graph_state->system_state;
- num1 = ((simgrid::mc::VisitedPair*) state1)->num;
- num2 = ((simgrid::mc::VisitedPair*) state2)->num;
- }else if (_sg_mc_termination) { /* Non-progressive cycle MC */
- s1 = ((mc_state_t) state1)->system_state;
- s2 = ((mc_state_t) state2)->system_state;
- num1 = ((mc_state_t) state1)->num;
- num2 = ((mc_state_t) state2)->num;
- } else { /* Safety or comm determinism MC */
- s1 = ((simgrid::mc::VisitedState*) state1)->system_state;
- s2 = ((simgrid::mc::VisitedState*) state2)->system_state;
- num1 = ((simgrid::mc::VisitedState*) state1)->num;
- num2 = ((simgrid::mc::VisitedState*) state2)->num;
- }
-
int errors = 0;
int res_init;
#endif
return errors > 0 || hash_result;
+}
+
+int snapshot_compare(mc_state_t state1, mc_state_t state2)
+{
+ simgrid::mc::Snapshot* s1 = state1->system_state;
+ simgrid::mc::Snapshot* s2 = state2->system_state;
+ int num1 = state1->num;
+ int num2 = state2->num;
+ return snapshot_compare(num1, s1, num2, s2);
+}
+int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
+{
+ simgrid::mc::Snapshot* s1 = state1->system_state;
+ simgrid::mc::Snapshot* s2 = state2->system_state;
+ int num1 = state1->num;
+ int num2 = state2->num;
+ return snapshot_compare(num1, s1, num2, s2);
}
}
+}
char *_sg_mc_dot_output_file = nullptr;
int _sg_mc_comms_determinism = 0;
int _sg_mc_send_determinism = 0;
-int _sg_mc_safety = 0;
int _sg_mc_liveness = 0;
int _sg_mc_snapshot_fds = 0;
int _sg_mc_termination = 0;
class Frame;
class SimixProcessInformation;
+class Session;
+class Checker;
+class FunctionalChecker;
+
}
}
XBT_DEBUG("**** End Replay ****");
}
-void MC_replay_liveness(xbt_fifo_t stack)
-{
- xbt_fifo_item_t item;
- simgrid::mc::Pair* pair = nullptr;
- mc_state_t state = nullptr;
- smx_simcall_t req = nullptr, saved_req = NULL;
- int value, depth = 1;
- char *req_str;
-
- XBT_DEBUG("**** Begin Replay ****");
-
- /* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0) {
- item = xbt_fifo_get_first_item(stack);
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
- if(pair->graph_state->system_state){
- simgrid::mc::restore_snapshot(pair->graph_state->system_state);
- return;
- }
- }
-
- /* Restore the initial state */
- simgrid::mc::restore_snapshot(initial_global_state->snapshot);
-
- /* Traverse the stack from the initial state and re-execute the transitions */
- for (item = xbt_fifo_get_last_item(stack);
- item != xbt_fifo_get_first_item(stack);
- item = xbt_fifo_get_prev_item(item)) {
-
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-
- state = (mc_state_t) pair->graph_state;
-
- if (pair->exploration_started) {
-
- saved_req = MC_state_get_executed_request(state, &value);
-
- if (saved_req != nullptr) {
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- req = &issuer->simcall;
-
- /* Debug information */
- if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
-
- }
-
- simgrid::mc::handle_simcall(req, value);
- mc_model_checker->wait_for_requests();
- }
-
- /* Update statistics */
- mc_stats->visited_pairs++;
- mc_stats->executed_transitions++;
-
- depth++;
-
- }
-
- XBT_DEBUG("**** End Replay ****");
-}
-
/**
* \brief Dumps the contents of a model-checker's stack and shows the actual
* execution trace
MC_print_statistics(mc_stats);
}
-namespace simgrid {
-namespace mc {
-
-void show_stack_liveness(xbt_fifo_t stack)
-{
- int value;
- simgrid::mc::Pair* pair;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(pair->graph_state, &value);
- if (req && req->call != SIMCALL_NONE) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-void dump_stack_liveness(xbt_fifo_t stack)
-{
- simgrid::mc::Pair* pair;
- while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
- delete pair;
-}
-
-}
-}
-
void MC_print_statistics(mc_stats_t stats)
{
if(_sg_mc_comms_determinism) {
#include <cstring>
+#include <algorithm>
+#include <memory>
+
#include <unistd.h>
#include <sys/wait.h>
#include <xbt/automaton.h>
#include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
#include <xbt/fifo.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include "src/mc/mc_record.h"
#include "src/mc/mc_smx.h"
#include "src/mc/Client.hpp"
+#include "src/mc/mc_private.h"
#include "src/mc/mc_replay.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
namespace simgrid {
namespace mc {
+static xbt_dynar_t visited_pairs;
+
Pair::Pair() : num(++mc_stats->expanded_pairs),
visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
{}
MC_state_delete(this->graph_state, 1);
}
+static void show_stack_liveness(xbt_fifo_t stack)
+{
+ int value;
+ simgrid::mc::Pair* pair;
+ xbt_fifo_item_t item;
+ smx_simcall_t req;
+ char *req_str = nullptr;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ item; item = xbt_fifo_get_prev_item(item)) {
+ pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+ req = MC_state_get_executed_request(pair->graph_state, &value);
+ if (req && req->call != SIMCALL_NONE) {
+ req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+static void dump_stack_liveness(xbt_fifo_t stack)
+{
+ simgrid::mc::Pair* pair;
+ while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
+ delete pair;
+}
+
static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
{
unsigned int cursor = 0;
return std::move(values);
}
+static int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
+{
+ simgrid::mc::Snapshot* s1 = state1->graph_state->system_state;
+ simgrid::mc::Snapshot* s2 = state2->graph_state->system_state;
+ int num1 = state1->num;
+ int num2 = state2->num;
+ return snapshot_compare(num1, s1, num2, s2);
+}
+
static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
{
- simgrid::mc::VisitedPair* new_pair = new VisitedPair(
- pair->num, pair->automaton_state, pair->atomic_propositions.get(),
- pair->graph_state);
+ auto acceptance_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(::acceptance_pairs);
+ auto new_pair =
+ std::unique_ptr<simgrid::mc::VisitedPair>(new VisitedPair(
+ pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+ pair->graph_state));
new_pair->acceptance_pair = 1;
- if (xbt_dynar_is_empty(acceptance_pairs))
- xbt_dynar_push(acceptance_pairs, &new_pair);
- else {
-
- int min = -1, max = -1, index;
- //int res;
- simgrid::mc::VisitedPair* pair_test;
- int cursor;
-
- index = get_search_interval(acceptance_pairs, new_pair, &min, &max);
-
- if (min != -1 && max != -1) { // Acceptance pair with same number of processes and same heap bytes used exists
-
- cursor = min;
- if(pair->search_cycle == 1){
- while (cursor <= max) {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, cursor, simgrid::mc::VisitedPair*);
- if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value(
- pair_test->atomic_propositions.get(),
- new_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_pair) == 0) {
- XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
- xbt_fifo_shift(mc_stack);
- if (dot_output != nullptr)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
- return nullptr;
- }
- }
+ auto res = std::equal_range(acceptance_pairs.begin(), acceptance_pairs.end(),
+ new_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+ if (pair->search_cycle == 1)
+ for (auto i = res.first; i != res.second; ++i) {
+ simgrid::mc::VisitedPair* pair_test = *i;
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(
+ pair_test->atomic_propositions.get(),
+ new_pair->atomic_propositions.get()) == 0) {
+ if (snapshot_compare(pair_test, new_pair.get()) == 0) {
+ XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
+ xbt_fifo_shift(mc_stack);
+ if (dot_output != nullptr)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
+ return nullptr;
}
- cursor++;
}
}
- xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
- } else {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, index, simgrid::mc::VisitedPair*);
- if (pair_test->nb_processes < new_pair->nb_processes)
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
- else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
- else
- xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
}
- }
- return new_pair;
+
+ auto new_raw_pair = new_pair.release();
+ xbt_dynar_insert_at(
+ ::acceptance_pairs, res.first - acceptance_pairs.begin(), &new_raw_pair);
+ return new_raw_pair;
}
static void remove_acceptance_pair(int pair_num)
}
}
+static void MC_replay_liveness(xbt_fifo_t stack)
+{
+ xbt_fifo_item_t item;
+ simgrid::mc::Pair* pair = nullptr;
+ mc_state_t state = nullptr;
+ smx_simcall_t req = nullptr, saved_req = NULL;
+ int value, depth = 1;
+ char *req_str;
+
+ XBT_DEBUG("**** Begin Replay ****");
+
+ /* Intermediate backtracking */
+ if(_sg_mc_checkpoint > 0) {
+ item = xbt_fifo_get_first_item(stack);
+ pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+ if(pair->graph_state->system_state){
+ simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+ return;
+ }
+ }
+
+ /* Restore the initial state */
+ simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+
+ /* Traverse the stack from the initial state and re-execute the transitions */
+ for (item = xbt_fifo_get_last_item(stack);
+ item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
+
+ pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+
+ state = (mc_state_t) pair->graph_state;
+
+ if (pair->exploration_started) {
+
+ saved_req = MC_state_get_executed_request(state, &value);
+
+ if (saved_req != nullptr) {
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ req = &issuer->simcall;
+
+ /* Debug information */
+ if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
+ req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+ xbt_free(req_str);
+ }
+
+ }
+
+ simgrid::mc::handle_simcall(req, value);
+ mc_model_checker->wait_for_requests();
+ }
+
+ /* Update statistics */
+ mc_stats->visited_pairs++;
+ mc_stats->executed_transitions++;
+
+ depth++;
+
+ }
+
+ XBT_DEBUG("**** End Replay ****");
+}
+
+/**
+ * \brief Checks whether a given pair has already been visited by the algorithm.
+ */
+static
+int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+{
+ if (_sg_mc_visited == 0)
+ return -1;
+
+ simgrid::mc::VisitedPair* new_visited_pair = nullptr;
+ if (visited_pair == nullptr)
+ new_visited_pair = new simgrid::mc::VisitedPair(
+ pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+ pair->graph_state);
+ else
+ new_visited_pair = visited_pair;
+
+ auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(simgrid::mc::visited_pairs);
+
+ auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
+ new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+ for (auto i = range.first; i != range.second; ++i) {
+ simgrid::mc::VisitedPair* pair_test = *i;
+ std::size_t cursor = i - visited_pairs.begin();
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(
+ pair_test->atomic_propositions.get(),
+ new_visited_pair->atomic_propositions.get()) == 0) {
+ if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+ if (pair_test->other_num == -1)
+ new_visited_pair->other_num = pair_test->num;
+ else
+ new_visited_pair->other_num = pair_test->other_num;
+ if (dot_output == nullptr)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+ xbt_dynar_remove_at(simgrid::mc::visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(simgrid::mc::visited_pairs, cursor, &new_visited_pair);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair
+ || pair_test->acceptance_removed == 1)
+ delete pair_test;
+ return new_visited_pair->other_num;
+ }
+ }
+ }
+ }
+
+ xbt_dynar_insert_at(simgrid::mc::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+
+ if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+ int min2 = mc_stats->expanded_pairs;
+ unsigned int index2 = 0;
+ for (std::size_t i = 0; i != visited_pairs.size(); ++i) {
+ simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
+ if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+ && pair_test->num < min2) {
+ index2 = i;
+ min2 = pair_test->num;
+ }
+ }
+ simgrid::mc::VisitedPair* pair_test = nullptr;
+ xbt_dynar_remove_at(simgrid::mc::visited_pairs, index2, &pair_test);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+ delete pair_test;
+ }
+
+ return -1;
+}
+
static int MC_modelcheck_liveness_main(void)
{
simgrid::mc::Pair* current_pair = nullptr;
int modelcheck_liveness(void)
{
- if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
- simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
mc_model_checker->wait_for_requests();
};
int modelcheck_liveness(void);
-XBT_PRIVATE void show_stack_liveness(xbt_fifo_t stack);
-XBT_PRIVATE void dump_stack_liveness(xbt_fifo_t stack);
-
-XBT_PRIVATE extern xbt_dynar_t visited_pairs;
-XBT_PRIVATE int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair);
}
}
#include "src/mc/mc_protocol.h"
+#ifdef __cplusplus
+namespace simgrid {
+namespace mc {
+
+struct DerefAndCompareByNbProcessesAndUsedHeap {
+ template<class X, class Y>
+ bool operator()(X const& a, Y const& b)
+ {
+ return std::make_pair(a->nb_processes, a->heap_bytes_used) <
+ std::make_pair(b->nb_processes, b->heap_bytes_used);
+ }
+};
+
+}
+}
+#endif
+
SG_BEGIN_DECL()
/********************************* MC Global **********************************/
XBT_PRIVATE extern int user_max_depth_reached;
XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
-XBT_PRIVATE void MC_replay_liveness(xbt_fifo_t stack);
XBT_PRIVATE void MC_show_deadlock(smx_simcall_t req);
XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);
*/
XBT_PRIVATE extern xbt_fifo_t mc_stack;
-XBT_PRIVATE int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
-
-
/****************************** Statistics ************************************/
typedef struct mc_stats {
/********************************** Snapshot comparison **********************************/
-XBT_PRIVATE int snapshot_compare(void *state1, void *state2);
-
//#define MC_DEBUG 1
#define MC_VERBOSE 1
XBT_PRIVATE void MC_report_assertion_error(void);
XBT_PRIVATE void MC_report_crash(int status);
+SG_END_DECL()
+
#ifdef __cplusplus
namespace simgrid {
XBT_PRIVATE void find_object_address(
std::vector<simgrid::xbt::VmMap> const& maps, simgrid::mc::ObjectInformation* result);
+XBT_PRIVATE
+int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2);
+
}
}
#endif
-SG_END_DECL()
-
#endif
// Those are MC_state_get_internal_request(state)
bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
{
- if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::none)
- return true;
-
if (r1->issuer == r2->issuer)
return false;
extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
-int modelcheck_safety(void);
-
struct XBT_PRIVATE VisitedState {
simgrid::mc::Snapshot* system_state = nullptr;
size_t heap_bytes_used = 0;
};
extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
-XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state);
+XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots);
+XBT_PRIVATE int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2);
}
}
SG_END_DECL()
+namespace simgrid {
+namespace mc {
+
+XBT_PRIVATE int snapshot_compare(mc_state_t state1, mc_state_t state2);
+
+}
+}
+
#endif
#include <sys/wait.h>
#include <memory>
+#include <algorithm>
#include <xbt/automaton.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
#include <xbt/fifo.h>
#include "src/mc/mc_comm_pattern.h"
namespace simgrid {
namespace mc {
-xbt_dynar_t visited_pairs;
std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
MC_state_delete(this->graph_state, 1);
}
-}
-}
-
-/**
- * \brief Find a suitable subrange of candidate duplicates for a given state
- * \param list dynamic array of states/pairs with candidate duplicates of the current state;
- * \param ref current state/pair;
- * \param min (output) index of the beginning of the the subrange
- * \param max (output) index of the enf of the subrange
- *
- * Given a suitably ordered array of states/pairs, this function extracts a subrange
- * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
- * This function uses only fast discriminating criterions and does not use the
- * full state/pair comparison algorithms.
- *
- * The states/pairs in list MUST be ordered using a (given) weak order
- * (based on nb_processes and heap_bytes_used).
- * The subrange is the subrange of "equivalence" of the given state/pair.
- */
-int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
-{
- int cursor = 0, previous_cursor;
- int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
- void *ref_test;
-
- if (_sg_mc_liveness) {
- nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes;
- heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used;
- } else {
- nb_processes = ((simgrid::mc::VisitedState*) ref)->nb_processes;
- heap_bytes_used = ((simgrid::mc::VisitedState*) ref)->heap_bytes_used;
- }
-
- int start = 0;
- int end = xbt_dynar_length(list) - 1;
-
- while (start <= end) {
- cursor = (start + end) / 2;
- if (_sg_mc_liveness) {
- ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*);
- nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
- heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
- } else {
- ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*);
- nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
- heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
- }
- if (nb_processes_test < nb_processes)
- start = cursor + 1;
- else if (nb_processes_test > nb_processes)
- end = cursor - 1;
- else if (heap_bytes_used_test < heap_bytes_used)
- start = cursor + 1;
- else if (heap_bytes_used_test > heap_bytes_used)
- end = cursor - 1;
- else {
- *min = *max = cursor;
- previous_cursor = cursor - 1;
- while (previous_cursor >= 0) {
- if (_sg_mc_liveness) {
- ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*);
- nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
- heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
- } else {
- ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*);
- nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
- heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
- }
- if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
- break;
- *min = previous_cursor;
- previous_cursor--;
- }
- size_t next_cursor = cursor + 1;
- while (next_cursor < xbt_dynar_length(list)) {
- if (_sg_mc_liveness) {
- ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*);
- nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
- heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
- } else {
- ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*);
- nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
- heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
- }
- if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
- break;
- *max = next_cursor;
- next_cursor++;
- }
- return -1;
- }
- }
- return cursor;
-}
-
-// TODO, it would make sense to use std::set instead
-template<class T>
-int get_search_interval(std::vector<std::unique_ptr<T>> const& list, T *ref, int *min, int *max)
-{
- int nb_processes = ref->nb_processes;
- int heap_bytes_used = ref->heap_bytes_used;
-
- int cursor = 0;
- int start = 0;
- int end = list.size() - 1;
- while (start <= end) {
- cursor = (start + end) / 2;
- int nb_processes_test = list[cursor]->nb_processes;
- int heap_bytes_used_test = list[cursor]->heap_bytes_used;
-
- if (nb_processes_test < nb_processes)
- start = cursor + 1;
- else if (nb_processes_test > nb_processes)
- end = cursor - 1;
- else if (heap_bytes_used_test < heap_bytes_used)
- start = cursor + 1;
- else if (heap_bytes_used_test > heap_bytes_used)
- end = cursor - 1;
- else {
- *min = *max = cursor;
- int previous_cursor = cursor - 1;
- while (previous_cursor >= 0) {
- nb_processes_test = list[previous_cursor]->nb_processes;
- heap_bytes_used_test = list[previous_cursor]->heap_bytes_used;
- if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
- break;
- *min = previous_cursor;
- previous_cursor--;
- }
- size_t next_cursor = cursor + 1;
- while (next_cursor < list.size()) {
- nb_processes_test = list[next_cursor]->nb_processes;
- heap_bytes_used_test = list[next_cursor]->heap_bytes_used;
- if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
- break;
- *max = next_cursor;
- next_cursor++;
- }
- return -1;
- }
- }
- return cursor;
-}
-
-static
-bool some_communications_are_not_finished()
+static void prune_visited_states()
{
- for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
- xbt_dynar_t pattern = xbt_dynar_get_as(
- incomplete_communications_pattern, current_process, xbt_dynar_t);
- if (!xbt_dynar_is_empty(pattern)) {
- XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
- return true;
- }
+ while (visited_states.size() > (std::size_t) _sg_mc_visited) {
+ XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
+ auto min_element = std::min_element(visited_states.begin(), visited_states.end(),
+ [](std::unique_ptr<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& b) {
+ return a->num < b->num;
+ });
+ xbt_assert(min_element != visited_states.end());
+ // and drop it:
+ visited_states.erase(min_element);
+ XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
- return false;
}
-namespace simgrid {
-namespace mc {
-
/**
* \brief Checks whether a given state has already been visited by the algorithm.
*/
-std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state)
+std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots)
{
- if (_sg_mc_visited == 0)
- return nullptr;
- /* If comm determinism verification, we cannot stop the exploration if some
- communications are not finished (at least, data are transfered). These communications
- are incomplete and they cannot be analyzed and compared with the initial pattern. */
- int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
- some_communications_are_not_finished();
std::unique_ptr<simgrid::mc::VisitedState> new_state =
std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
graph_state->in_visited_states = 1;
XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
- if (visited_states.empty()) {
- visited_states.push_back(std::move(new_state));
- return nullptr;
- }
-
- int min = -1, max = -1, index;
-
- index = get_search_interval(visited_states, new_state.get(), &min, &max);
-
- if (min != -1 && max != -1) {
+ auto range = std::equal_range(visited_states.begin(), visited_states.end(),
+ new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
- if (_sg_mc_safety || (!partial_comm
- && initial_global_state->initial_communications_pattern_done)) {
+ if (compare_snpashots) {
- int cursor = min;
- while (cursor <= max) {
- if (snapshot_compare(visited_states[cursor].get(), new_state.get()) == 0) {
+ for (auto i = range.first; i != range.second; ++i) {
+ auto& visited_state = *i;
+ if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
// The state has been visited:
std::unique_ptr<simgrid::mc::VisitedState> old_state =
- std::move(visited_states[cursor]);
+ std::move(visited_state);
if (old_state->other_num == -1)
new_state->other_num = old_state->num;
XBT_DEBUG("Replace visited state %d with the new visited state %d",
old_state->num, new_state->num);
- simgrid::mc::visited_states[cursor] = std::move(new_state);
+ visited_state = std::move(new_state);
return std::move(old_state);
}
- cursor++;
}
}
-
- XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
- visited_states.insert(visited_states.begin() + min, std::move(new_state));
-
- } else {
-
- // The state has not been visited: insert the state in the dynamic array.
- simgrid::mc::VisitedState* state_test = &*visited_states[index];
- std::size_t position;
- if (state_test->nb_processes < new_state->nb_processes)
- position = index + 1;
- else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
- position = index + 1;
- else
- position = index;
- visited_states.insert(visited_states.begin() + position, std::move(new_state));
- XBT_DEBUG("Insert new visited state %d (total : %lu)",
- visited_states[index]->num,
- (unsigned long) visited_states.size());
-
- }
-
- if (visited_states.size() <= (std::size_t) _sg_mc_visited)
- return nullptr;
- // We have reached the maximum number of stored states;
-
- XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
-
- // Find the (index of the) older state (with the smallest num):
- int min2 = mc_stats->expanded_states;
- unsigned int index2 = 0;
-
- for (std::size_t cursor2 = 0; cursor2 != visited_states.size(); ++cursor2)
- if (!mc_model_checker->is_important_snapshot(
- *visited_states[cursor2]->system_state)
- && visited_states[cursor2]->num < min2) {
- index2 = cursor2;
- min2 = visited_states[cursor2]->num;
- }
-
- // and drop it:
- visited_states.erase(visited_states.begin() + index2);
- XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
-
- return nullptr;
-}
-
-/**
- * \brief Checks whether a given pair has already been visited by the algorithm.
- */
-int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
-
- if (_sg_mc_visited == 0)
- return -1;
-
- simgrid::mc::VisitedPair* new_visited_pair = nullptr;
- if (visited_pair == nullptr)
- new_visited_pair = new simgrid::mc::VisitedPair(
- pair->num, pair->automaton_state, pair->atomic_propositions.get(),
- pair->graph_state);
- else
- new_visited_pair = visited_pair;
-
- if (xbt_dynar_is_empty(visited_pairs)) {
- xbt_dynar_push(visited_pairs, &new_visited_pair);
- return -1;
- }
-
- int min = -1, max = -1, index;
- //int res;
- simgrid::mc::VisitedPair* pair_test;
- int cursor;
-
- index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
-
- if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
- cursor = min;
- while (cursor <= max) {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
- if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value(
- pair_test->atomic_propositions.get(),
- new_visited_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_visited_pair) == 0) {
- if (pair_test->other_num == -1)
- new_visited_pair->other_num = pair_test->num;
- else
- new_visited_pair->other_num = pair_test->other_num;
- if (dot_output == nullptr)
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
- else
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
- xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
- xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
- pair_test->visited_removed = 1;
- if (!pair_test->acceptance_pair
- || pair_test->acceptance_removed == 1)
- delete pair_test;
- return new_visited_pair->other_num;
- }
- }
- }
- cursor++;
- }
- xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
- } else {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
- if (pair_test->nb_processes < new_visited_pair->nb_processes)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
- else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
- else
- xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
- }
-
- if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
- int min2 = mc_stats->expanded_pairs;
- unsigned int cursor2 = 0;
- unsigned int index2 = 0;
- xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
- if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
- && pair_test->num < min2) {
- index2 = cursor2;
- min2 = pair_test->num;
- }
- }
- xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
- pair_test->visited_removed = 1;
- if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
- delete pair_test;
- }
- return -1;
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
+ visited_states.insert(range.first, std::move(new_state));
+ prune_visited_states();
+ return nullptr;
}
}
#include <utility>
-#include <fcntl.h>
-#include <signal.h>
-#include <poll.h>
-
#include <unistd.h>
-#include <sys/types.h>
-#include <sys/socket.h>
-#include <sys/wait.h>
-#include <sys/ptrace.h>
-
-#ifdef __linux__
-#include <sys/prctl.h>
-#endif
-
#include <xbt/log.h>
-#include <xbt/sysdep.h>
-#include <xbt/system_error.hpp>
#include "simgrid/sg_config.h"
#include "src/xbt_modinter.h"
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_liveness.h"
#include "src/mc/mc_exit.h"
+#include "src/mc/Session.hpp"
+#include "src/mc/Checker.hpp"
+#include "src/mc/SafetyChecker.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
-/** Execute some code in a forked process */
-template<class F>
static inline
-pid_t do_fork(F f)
-{
- pid_t pid = fork();
- if (pid < 0)
- throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
- if (pid != 0)
- return pid;
-
- // Child-process:
- try {
- f();
- _exit(EXIT_SUCCESS);
- }
- catch(...) {
- // The callback should catch exceptions:
- abort();
- }
-}
-
-static
-int exec_model_checked(int socket, char** argv)
-{
- XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
-
-#ifdef __linux__
- // Make sure we do not outlive our parent:
- sigset_t mask;
- sigemptyset (&mask);
- if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
- throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
- if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
- throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
-#endif
-
- int res;
-
- // Remove CLOEXEC in order to pass the socket to the exec-ed program:
- int fdflags = fcntl(socket, F_GETFD, 0);
- if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
- throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
-
- // Set environment:
- setenv(MC_ENV_VARIABLE, "1", 1);
-
- // Disable lazy relocation in the model-checked process.
- // We don't want the model-checked process to modify its .got.plt during
- // snapshot.
- setenv("LC_BIND_NOW", "1", 1);
-
- char buffer[64];
- res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
- if ((size_t) res >= sizeof(buffer) || res == -1)
- std::abort();
- setenv(MC_ENV_SOCKET_FD, buffer, 1);
-
- execvp(argv[1], argv+1);
-
- XBT_ERROR("Could not run the model-checked program");
- // This is the value used by system() and popen() in this case:
- return 127;
-}
-
-static
-std::pair<pid_t, int> create_model_checked(char** argv)
-{
- // Create a AF_LOCAL socketpair used for exchanging messages
- // bewteen the model-checker process (ourselves) and the model-checked
- // process:
- int res;
- int sockets[2];
- res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
- if (res == -1)
- throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
-
- pid_t pid = do_fork([&] {
- close(sockets[1]);
- int res = exec_model_checked(sockets[0], argv);
- XBT_DEBUG("Error in the child process creation");
- _exit(res);
- });
-
- // Parent (model-checker):
- close(sockets[0]);
- return std::make_pair(pid, sockets[1]);
-}
-
-static
char** argvdup(int argc, char** argv)
{
char** argv_copy = xbt_new(char*, argc+1);
return argv_copy;
}
+static
+std::unique_ptr<simgrid::mc::Checker> createChecker(simgrid::mc::Session& session)
+{
+ using simgrid::mc::Session;
+ using simgrid::mc::FunctionalChecker;
+
+ std::function<int(Session& session)> code;
+ if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+ code = [](Session& session) {
+ return MC_modelcheck_comm_determinism(); };
+ else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
+ return std::unique_ptr<simgrid::mc::Checker>(
+ new simgrid::mc::SafetyChecker(session));
+ else
+ code = [](Session& session) {
+ return simgrid::mc::modelcheck_liveness(); };
+
+ return std::unique_ptr<simgrid::mc::Checker>(
+ new FunctionalChecker(session, std::move(code)));
+}
+
int main(int argc, char** argv)
{
+ using simgrid::mc::Session;
+
try {
if (argc < 2)
xbt_die("Missing arguments.\n");
+ // Currently, we need this before sg_config_init:
_sg_do_model_check = 1;
+ mc_mode = MC_MODE_SERVER;
// The initialisation function can touch argv.
- // We need to keep the original parameters in order to pass them to the
- // model-checked process so we make a copy of them:
- int argc_copy = argc;
+ // We make a copy of argv before modifying it in order to pass the original
+ // value to the model-checked:
char** argv_copy = argvdup(argc, argv);
- xbt_log_init(&argc_copy, argv_copy);
- sg_config_init(&argc_copy, argv_copy);
+ xbt_log_init(&argc, argv);
+ sg_config_init(&argc, argv);
- int sock;
- pid_t model_checked_pid;
- std::tie(model_checked_pid, sock) = create_model_checked(argv);
- XBT_DEBUG("Inside the parent process");
- if (mc_model_checker)
- xbt_die("MC server already present");
+ std::unique_ptr<Session> session =
+ std::unique_ptr<Session>(Session::spawnvp(argv_copy[1], argv_copy+1));
+ free(argv_copy);
- mc_mode = MC_MODE_SERVER;
- std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(model_checked_pid, sock));
- process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
- mc_model_checker = new simgrid::mc::ModelChecker(std::move(process));
- mc_model_checker->start();
- int res = 0;
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- res = MC_modelcheck_comm_determinism();
- else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
- res = simgrid::mc::modelcheck_safety();
- else
- res = simgrid::mc::modelcheck_liveness();
- mc_model_checker->shutdown();
+ simgrid::mc::session = session.get();
+ std::unique_ptr<simgrid::mc::Checker> checker = createChecker(*session);
+ int res = checker->run();
+ session->close();
return res;
}
catch(std::exception& e) {
: name_(xbt_strdup(name))
{
}
- void As::Seal()
+ void As::seal()
{
sealed_ = true;
}
namespace simgrid {
namespace surf {
-void AsDijkstra::Seal()
+void AsDijkstra::seal()
{
xbt_node_t node = NULL;
unsigned int cursor2, cursor;
class XBT_PRIVATE AsDijkstra : public AsRoutedGraph {
public:
AsDijkstra(const char*name, bool cached);
- void Seal() override;
+ void seal() override;
~AsDijkstra();
xbt_node_t routeGraphNewNode(int id, int graph_id);
}
}
-void AsFloyd::Seal(){
+void AsFloyd::seal(){
/* set the size of table routing */
size_t table_size = xbt_dynar_length(vertices_);
void getRouteAndLatency(NetCard *src, NetCard *dst, sg_platf_route_cbarg_t into, double *latency) override;
void addRoute(sg_platf_route_cbarg_t route) override;
- void Seal() override;
+ void seal() override;
private:
/* vars to compute the Floyd algorithm. */
{
}
-void AsFull::Seal() {
+void AsFull::seal() {
int i;
sg_platf_route_cbarg_t e_route;
public:
AsFull(const char*name);
- void Seal() override;
+ void seal() override;
~AsFull();
void getRouteAndLatency(NetCard *src, NetCard *dst, sg_platf_route_cbarg_t into, double *latency) override;
//get the onelinks from the parsed platform
xbt_dynar_t onelink_routes = routing_platf->getOneLinkRoutes();
- if (!onelink_routes)
- xbt_die("There is no routes!");
- XBT_DEBUG("Have get_onelink_routes, found %ld routes",onelink_routes->used);
+
+ XBT_DEBUG("There is %ld one-link routes",onelink_routes->used);
//save them in trace file
simgrid::surf::Onelink *onelink;
unsigned int iter;
xbt_dynar_foreach(onelink_routes, iter, onelink) {
char *src = onelink->src_->name();
char *dst = onelink->dst_->name();
- simgrid::surf::LinkNS3 *link =
- static_cast<simgrid::surf::LinkNS3 *>(onelink->link_);
+ simgrid::surf::LinkNS3 *link = static_cast<simgrid::surf::LinkNS3 *>(onelink->link_);
if (strcmp(src,dst) && link->m_created){
XBT_DEBUG("Route from '%s' to '%s' with link '%s'", src, dst, link->getName());
}
}
-static void parse_ns3_end_platform(void)
-{
- ns3_end_platform();
-}
-
-static void define_callbacks_ns3(void)
-{
- simgrid::s4u::Host::onCreation.connect(simgrid_ns3_add_host);
- simgrid::surf::netcardCreatedCallbacks.connect(simgrid_ns3_add_router);
- simgrid::surf::on_link.connect (parse_ns3_add_link);
- simgrid::surf::on_cluster.connect (&parse_ns3_add_cluster);
- simgrid::surf::asCreatedCallbacks.connect(parse_ns3_add_AS);
- simgrid::surf::on_postparse.connect(&create_ns3_topology); //get_one_link_routes
- simgrid::surf::on_postparse.connect(&parse_ns3_end_platform); //InitializeRoutes
-}
-
/*********
* Model *
*********/
-static void free_ns3_link(void * elmts)
-{
- delete static_cast<simgrid::surf::LinkNS3*>(elmts);
-}
-
-static void free_ns3_host(void * elmts)
-{
- ns3_node_t host = static_cast<ns3_node_t>(elmts);
- free(host);
-}
-
void surf_network_model_init_NS3()
{
if (surf_network_model)
return;
surf_network_model = new simgrid::surf::NetworkNS3Model();
-
xbt_dynar_push(all_existing_models, &surf_network_model);
}
xbt_die("Impossible to initialize NS3 interface");
}
routing_model_create(NULL);
- define_callbacks_ns3();
+ simgrid::s4u::Host::onCreation.connect(simgrid_ns3_add_host);
+ simgrid::surf::netcardCreatedCallbacks.connect(simgrid_ns3_add_router);
+ simgrid::surf::on_link.connect (parse_ns3_add_link);
+ simgrid::surf::on_cluster.connect (&parse_ns3_add_cluster);
+ simgrid::surf::asCreatedCallbacks.connect(parse_ns3_add_AS);
+ simgrid::surf::on_postparse.connect(&create_ns3_topology); //get_one_link_routes
+ simgrid::surf::on_postparse.connect(&ns3_end_platform); //InitializeRoutes
- NS3_EXTENSION_ID = simgrid::s4u::Host::extension_create(free_ns3_host);
- NS3_ASR_LEVEL = xbt_lib_add_level(as_router_lib, free_ns3_host);
+ NS3_EXTENSION_ID = simgrid::s4u::Host::extension_create(xbt_free_f);
+ NS3_ASR_LEVEL = xbt_lib_add_level(as_router_lib, xbt_free_f);
}
NetworkNS3Model::~NetworkNS3Model() {
void sg_platf_new_AS_end()
{
xbt_assert(current_routing, "Cannot seal the current AS: none under construction");
- current_routing->Seal();
+ current_routing->seal();
current_routing = static_cast<simgrid::surf::AsImpl*>(current_routing->father());
if (TRACE_is_enabled())
static void new_state(char* id, int src){
- char* id_state = xbt_strdup(id);
- char* first_part = strtok(id,"_");
+ char* id_copy = xbt_strdup(id);
+ char* first_part = strtok(id_copy,"_");
int type = 0 ; // -1=initial state; 0=intermediate state; 1=final state
if(strcmp(first_part,"accept")==0){
type = -1;
}
}
+ free(id_copy);
xbt_automaton_state_t state = NULL;
- state = xbt_automaton_state_exists(parsed_automaton, id_state);
+ state = xbt_automaton_state_exists(parsed_automaton, id);
if(state == NULL){
- state = xbt_automaton_state_new(parsed_automaton, type, id_state);
+ state = xbt_automaton_state_new(parsed_automaton, type, id);
}
if(type==-1)
parsed_automaton->current_state = state;
- if(src)
- state_id_src = xbt_strdup(id_state);
-
+ if(src) {
+ if (state_id_src)
+ free(state_id_src);
+ state_id_src = xbt_strdup(id);
+ }
}
-static void new_transition(char* id, xbt_automaton_exp_label_t label){
-
- char* id_state = xbt_strdup(id);
+static void new_transition(char* id, xbt_automaton_exp_label_t label)
+{
xbt_automaton_state_t state_dst = NULL;
new_state(id, 0);
- state_dst = xbt_automaton_state_exists(parsed_automaton, id_state);
+ state_dst = xbt_automaton_state_exists(parsed_automaton, id);
xbt_automaton_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);
//xbt_transition_t trans = NULL;
src/mc/AddressSpace.cpp
src/mc/Channel.cpp
src/mc/Channel.hpp
+ src/mc/Checker.cpp
+ src/mc/Checker.hpp
src/mc/Client.cpp
src/mc/Client.hpp
src/mc/Frame.hpp
src/mc/ObjectInformation.cpp
src/mc/PageStore.hpp
src/mc/PageStore.cpp
+ src/mc/SafetyChecker.cpp
+ src/mc/SafetyChecker.hpp
src/mc/ChunkedData.hpp
src/mc/ChunkedData.cpp
src/mc/RegionSnapshot.cpp
src/mc/mc_forward.hpp
src/mc/Process.hpp
src/mc/Process.cpp
+ src/mc/Session.cpp
+ src/mc/Session.hpp
src/mc/mc_unw.h
src/mc/mc_unw.cpp
src/mc/mc_unw_vmread.cpp
src/mc/mc_request.h
src/mc/mc_request.cpp
src/mc/mc_safety.h
- src/mc/mc_safety.cpp
src/mc/mc_state.h
src/mc/mc_state.cpp
src/mc/mc_visited.cpp
