include src/mc/explo/UdporChecker.cpp
include src/mc/explo/UdporChecker.hpp
include src/mc/explo/simgrid_mc.cpp
+include src/mc/explo/udpor/Comb.hpp
include src/mc/explo/udpor/Configuration.cpp
include src/mc/explo/udpor/Configuration.hpp
include src/mc/explo/udpor/Configuration_test.cpp
int main(int argc, char** argv)
{
sg4::Engine e(&argc, argv);
- e.load_platform("../../platforms/two_hosts.xml");
+ e.load_platform(argc > 1 ? argv[1] : "../../platforms/two_hosts.xml");
/* Create the requested amount of actors pairs. Each pair has a specific mutex and cell in `result`. */
std::vector<int> result(cfg_actor_count.get());
/** @brief Save the current state */
VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, RemoteApp& remote_app)
- : heap_bytes_used_(remote_app.get_remote_process_memory().get_remote_heap_bytes())
+ : heap_bytes_used_(remote_app.get_remote_process_memory()->get_remote_heap_bytes())
, actor_count_(actor_count)
, num_(state_number)
{
this->system_state_ = std::make_shared<simgrid::mc::Snapshot>(state_number, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
}
void VisitedStates::prune()
for (auto i = range_begin; i != range_end; ++i) {
auto& visited_state = *i;
if (visited_state->system_state_->equals_to(*new_state->system_state_.get(),
- remote_app.get_remote_process_memory())) {
+ *remote_app.get_remote_process_memory())) {
// The state has been visited:
std::unique_ptr<simgrid::mc::VisitedState> old_state = std::move(visited_state);
namespace simgrid::mc {
-RemoteApp::RemoteApp(const std::vector<char*>& args)
+RemoteApp::RemoteApp(const std::vector<char*>& args, bool need_memory_introspection)
{
- checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(args);
+ for (auto* arg : args)
+ app_args_.push_back(arg);
- initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
+ checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(app_args_, need_memory_introspection);
+
+ if (need_memory_introspection)
+ initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, *checker_side_->get_remote_memory());
}
RemoteApp::~RemoteApp()
{
initial_snapshot_ = nullptr;
- shutdown();
+ checker_side_ = nullptr;
}
-void RemoteApp::restore_initial_state() const
+void RemoteApp::restore_initial_state()
{
- this->initial_snapshot_->restore(checker_side_->get_remote_memory());
+ if (initial_snapshot_ == nullptr) { // No memory introspection
+ // We need to destroy the existing CheckerSide before creating the new one, or libevent gets crazy
+ checker_side_.reset(nullptr);
+ checker_side_.reset(new simgrid::mc::CheckerSide(app_args_, true));
+ } else
+ initial_snapshot_->restore(*checker_side_->get_remote_memory());
}
unsigned long RemoteApp::get_maxpid() const
checker_side_->wait_for_requests();
}
-void RemoteApp::shutdown()
-{
- XBT_DEBUG("Shutting down model-checker");
-
- if (checker_side_->running()) {
- XBT_DEBUG("Killing process");
- finalize_app(true);
- kill(checker_side_->get_pid(), SIGKILL);
- checker_side_->terminate();
- }
-}
-
Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_transition)
{
s_mc_message_simcall_execute_t m = {};
m.times_considered_ = times_considered;
checker_side_->get_channel().send(m);
- get_remote_process_memory().clear_cache();
+ if (auto* memory = get_remote_process_memory(); memory != nullptr)
+ memory->clear_cache();
if (checker_side_->running())
checker_side_->dispatch_events(); // The app may send messages while processing the transition
void RemoteApp::finalize_app(bool terminate_asap)
{
- s_mc_message_int_t m = {};
- m.type = MessageType::FINALIZE;
- m.value = terminate_asap;
- xbt_assert(checker_side_->get_channel().send(m) == 0, "Could not ask the app to finalize on need");
-
- s_mc_message_t answer;
- ssize_t s = checker_side_->get_channel().receive(answer);
- xbt_assert(s != -1, "Could not receive answer to FINALIZE");
- xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
- xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
- "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
- (int)answer.type, (int)MessageType::FINALIZE_REPLY);
+ checker_side_->finalize(terminate_asap);
}
} // namespace simgrid::mc
PageStore page_store_{500};
std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
+ std::vector<char*> app_args_;
+
// No copy:
RemoteApp(RemoteApp const&) = delete;
RemoteApp& operator=(RemoteApp const&) = delete;
*
* The code is expected to `exec` the model-checked application.
*/
- explicit RemoteApp(const std::vector<char*>& args);
+ explicit RemoteApp(const std::vector<char*>& args, bool need_memory_introspection);
~RemoteApp();
- void restore_initial_state() const;
+ void restore_initial_state();
void wait_for_requests();
/** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
/** Ask the application to run post-mortem analysis, and maybe to stop ASAP */
void finalize_app(bool terminate_asap = false);
- /** Forcefully kill the application (after running post-mortem analysis)*/
- void shutdown();
/** Retrieve the max PID of the running actors */
unsigned long get_maxpid() const;
Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
/* Get the memory of the remote process */
- RemoteProcessMemory& get_remote_process_memory() { return checker_side_->get_remote_memory(); }
+ RemoteProcessMemory* get_remote_process_memory() { return checker_side_->get_remote_memory(); }
PageStore& get_page_store() { return page_store_; }
};
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
}
State::State(RemoteApp& remote_app, const State* parent_state) : num_(++expended_states_), parent_state_(parent_state)
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
/* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
if (_sg_mc_sleep_set) {
if (not parent_state_->get_transition()->depends(&transition)) {
- sleep_set_.emplace(aid, transition);
+ sleep_set_.try_emplace(aid, transition);
if (guide_->actors_to_run_.count(aid) != 0) {
XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
- void add_sleep_set(Transition* t)
+ void add_sleep_set(const Transition* t)
{
sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
}
{
for (auto const& state : stack_) {
if (state->get_system_state()->equals_to(*current_state->get_system_state(),
- get_remote_app().get_remote_process_memory())) {
+ *get_remote_app().get_remote_process_memory())) {
XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
/* If asked to rollback on a state that has a snapshot, restore it */
State* last_state = backtrack.back().get();
if (const auto* system_state = last_state->get_system_state()) {
- system_state->restore(get_remote_app().get_remote_process_memory());
+ system_state->restore(*get_remote_app().get_remote_process_memory());
on_restore_system_state_signal(last_state, get_remote_app());
return;
}
XBT_VERB(">> Backtracked to %s", get_record_trace().to_string().c_str());
}
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args)
+// DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, _sg_mc_termination) //
+// UNCOMMENT TO ACTIVATE REFORKS
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor)
+ : Exploration(args, true) // This version does not use reforks as it breaks
{
if (with_dpor)
reduction_mode_ = ReductionMode::dpor;
Exploration* Exploration::instance_ = nullptr; // singleton instance
-Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make_unique<RemoteApp>(args))
+Exploration::Exploration(const std::vector<char*>& args, bool need_memory_introspection)
+ : remote_app_(std::make_unique<RemoteApp>(args, need_memory_introspection))
{
xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
instance_ = this;
}
}
-void Exploration::report_crash(int status)
+XBT_ATTRIB_NORETURN void Exploration::report_crash(int status)
{
XBT_INFO("**************************");
XBT_INFO("** CRASH IN THE PROGRAM **");
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
- XBT_INFO("Stack trace:");
- get_remote_app().get_remote_process_memory().dump_stack();
+ const auto* memory = get_remote_app().get_remote_process_memory();
+ if (memory) {
+ XBT_INFO("Stack trace:");
+ memory->dump_stack();
+ } else {
+ XBT_INFO("Stack trace not shown because there is no memory introspection.");
+ }
}
system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
-void Exploration::report_assertion_failure()
+XBT_ATTRIB_NORETURN void Exploration::report_assertion_failure()
{
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
system_exit(SIMGRID_MC_EXIT_SAFETY);
}
-void Exploration::system_exit(int status)
+void Exploration::system_exit(int status) const
{
- get_remote_app().shutdown();
::exit(status);
}
FILE* dot_output_ = nullptr;
public:
- explicit Exploration(const std::vector<char*>& args);
+ explicit Exploration(const std::vector<char*>& args, bool need_memory_introspection);
virtual ~Exploration();
static Exploration* get_instance() { return instance_; }
virtual void run() = 0;
/** Produce an error message indicating that the application crashed (status was produced by waitpid) */
- void report_crash(int status);
+ XBT_ATTRIB_NORETURN void report_crash(int status);
/** Produce an error message indicating that a property was violated */
- void report_assertion_failure();
+ XBT_ATTRIB_NORETURN void report_assertion_failure();
/** Kill the application and the model-checker (which exits with `status`)*/
- XBT_ATTRIB_NORETURN void system_exit(int status);
+ XBT_ATTRIB_NORETURN void system_exit(int status) const;
/* These methods are callbacks called by the model-checking engine
* to get and display information about the current state of the
RemoteApp& remote_app)
: num(pair_num), prop_state_(prop_state)
{
- auto& memory = remote_app.get_remote_process_memory();
+ auto* memory = remote_app.get_remote_process_memory();
this->app_state_ = std::move(app_state);
if (not this->app_state_->get_system_state())
- this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), memory));
- this->heap_bytes_used = memory.get_remote_heap_bytes();
+ this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), *memory));
+ this->heap_bytes_used = memory->get_remote_heap_bytes();
this->actor_count_ = app_state_->get_actor_count();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
(not pair_test->app_state_->get_system_state()->equals_to(*new_pair->app_state_->get_system_state(),
- get_remote_app().get_remote_process_memory())))
+ *get_remote_app().get_remote_process_memory())))
continue;
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
exploration_stack_.pop_back();
if (_sg_mc_checkpoint > 0) {
const Pair* pair = exploration_stack_.back().get();
if (const auto* system_state = pair->app_state_->get_system_state()) {
- system_state->restore(get_remote_app().get_remote_process_memory());
+ system_state->restore(*get_remote_app().get_remote_process_memory());
return;
}
}
if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
(not pair_test->app_state_->get_system_state()->equals_to(*visited_pair->app_state_->get_system_state(),
- get_remote_app().get_remote_process_memory())))
+ *get_remote_app().get_remote_process_memory())))
continue;
if (pair_test->other_num == -1)
visited_pair->other_num = pair_test->num;
}
}
-LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args) {}
+LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args, true) {}
LivenessChecker::~LivenessChecker()
{
xbt_automaton_free(property_automaton_);
#include "src/mc/explo/UdporChecker.hpp"
#include "src/mc/api/State.hpp"
+#include "src/mc/explo/udpor/Comb.hpp"
+#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+
#include <xbt/asserts.h>
#include <xbt/log.h>
namespace simgrid::mc::udpor {
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
{
// Initialize the map
}
// are no enabled transitions that can be executed from the
// state reached by `C` (denoted `state(C)`), i.e. by some
// execution of the transitions in C obeying the causality
- // relation. Here, then, we would be in a deadlock.
+ // relation. Here, then, we may be in a deadlock (the other
+ // possibility is that we've finished running everything, and
+ // we wouldn't be in deadlock then)
if (enC.empty()) {
get_remote_app().check_deadlock();
}
"the search, yet no events were actually chosen\n"
"*********************************\n\n");
- // Move the application into stateCe and actually make note of that state
+ // Move the application into stateCe and make note of that state
move_to_stateCe(*stateC, *e);
auto stateCe = record_current_state();
// D <-- D + {e}
D.insert(e);
- // TODO: Determine a value of K to use or don't use it at all
constexpr unsigned K = 10;
- if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
- J.subtract(C.get_events());
+ if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
// Before searching the "right half", we need to make
// sure the program actually reflects the fact
restore_program_state_to(*stateC);
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
+ auto J_minus_C = J.value().get_events().subtracting(C.get_events());
+ explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
}
// D <-- D - {e}
begin != maximal_subsets_iterator(); ++begin) {
const EventSet& maximal_subset = *begin;
- // TODO: Determine if `a` is enabled here
+ // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
+ // We leave the implementation as-is to ensure that any addition would be simple
+ // if it were ever added
const bool enabled_at_config_k = false;
if (enabled_at_config_k) {
}
}
}
-
return incremental_exC;
}
void UdporChecker::restore_program_state_to(const State& stateC)
{
- // TODO: Perform state regeneration in the same manner as is done
- // in the DFSChecker.cpp
+ get_remote_app().restore_initial_state();
+ // TODO: We need to have the stack of past states available at this
+ // point. Since the method is recursive, we'll need to keep track of
+ // this as we progress
}
std::unique_ptr<State> UdporChecker::record_current_state()
return nullptr;
}
-EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
-{
- // TODO: Compute k-partial alternatives using [2]
- return EventSet();
-}
-
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
{
- // TODO: Perform clean up here
+ const EventSet C_union_D = C.get_events().make_union(D);
+ const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
+ const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
+
+ // Move {e} \ Q_CDU from U to G
+ if (Q_CDU.contains(e)) {
+ this->unfolding.remove(e);
+ }
+
+ // foreach ê in #ⁱ_U(e)
+ for (const auto* e_hat : es_immediate_conflicts) {
+ // Move [ê] \ Q_CDU from U to G
+ const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
+ this->unfolding.remove(to_remove);
+ }
}
RecordTrace UdporChecker::get_record_trace()
* current implementation of `tiny_simgrid`:
*
* 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
- * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
+ * 2. "Quasi-Optimal Partial Order Reduction" by Nguyen et al.
* 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
*/
class XBT_PRIVATE UdporChecker : public Exploration {
inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
- /**
- * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
- * UDPOR properly searches the state space
- *
- * The set `U` is a global variable which is maintained by UDPOR
- * to keep track of "just enough" information about the unfolding
- * to compute *alternatives* (see the paper for more details).
- *
- * @invariant: When a new event is created by UDPOR, it is inserted into
- * this set. All new events that are created by UDPOR have causes that
- * also exist in U and are valid for the duration of the search.
- *
- * If an event is discarded instead of moved from set `U` to set `G`,
- * the event and its contents will be discarded.
- */
- EventSet U;
-
- /**
- * @brief The "irrelevant" portions of the unfolding that do not need to be kept
- * around to ensure that UDPOR functions correctly
- *
- * The set `G` is another global variable maintained by the UDPOR algorithm which
- * is used to keep track of all events which used to be important to UDPOR
- */
- EventSet G;
-
- /// @brief UDPOR's current "view" of the program it is exploring
Unfolding unfolding = Unfolding();
/**
* SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
* Intuitively, the idea is to take advantage of the fact that you can avoid a lot
* of repeated computation by exploiting the aforementioned properties (in [3]) in
- * what is effectively a dynamic programming optimization. See [3] for more details
+ * what is akin to a dynamic programming optimization. See [3] for more details
*
* @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
* computed
/**
* @brief Computes a portion of the extension set of a configuration given
- * some action `action`
+ * some action `action` by directly enumerating all maximal subsets of C
+ * (i.e. without specializations based on the action)
*/
EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
- /**
- *
- */
- EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
-
/**
*
*/
--- /dev/null
+/* 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_UDPOR_COMB_HPP
+#define SIMGRID_MC_UDPOR_COMB_HPP
+
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/xbt/utils/iter/variable_for_loop.hpp"
+
+#include <boost/iterator/function_input_iterator.hpp>
+#include <boost/iterator/indirect_iterator.hpp>
+#include <functional>
+#include <vector>
+
+namespace simgrid::mc::udpor {
+
+/**
+ * @brief An individual element of a `Comb`, i.e. a
+ * sequence of `const UnfoldingEvent*`s
+ */
+using Spike = std::vector<const UnfoldingEvent*>;
+
+/**
+ * @brief A two-dimensional data structure that is used
+ * to compute partial alternatives in UDPOR
+ *
+ * The comb data structure is described in the paper
+ * "Quasi-Optimal DPOR" by Nguyen et al. Formally,
+ * if `A` is a set:
+ *
+ * """
+ * An **A-Comb C of size `n` (`n` a natural number)**
+ * is an *ordered* collection of spikes <s_1, s_2, ..., s_n>,
+ * where each spike is a sequence of elements over A.
+ *
+ * Furthermore, a **combination over C** is any tuple
+ * <a_1, a_2, ..., a_n> where a_i is a member of s_i
+ * """
+ *
+ * The name probably comes from what the structure looks
+ * like if you draw it out. For example, if `A = {1, 2, 3, ..., 10}`,
+ * then a possible `A-comb` of size 8 might look like
+ *
+ * 1 2 3 4 5 6
+ * 2 4 5 9 8
+ * 10 9 2 1 1
+ * 8 9 10 5
+ * 1
+ * 3 4 5
+ * 1 4 4 5 1 6
+ * 8 8 9
+ *
+ * which, if you squint a bit, looks like a comb (albeit with some
+ * broken bristles [or spikes]). A combination is any selection of
+ * one element within each spike; e.g. (where _x_ denotes element `x`
+ * is selected)
+ *
+ * 1 2 _3_ 4 5 6
+ * 2 _4_ 5 9 8
+ * 10 9 2 _1_ 1
+ * 8 _9_ 10 5
+ * _1_
+ * 3 4 _5_
+ * 1 _4_ 4 5 1 6
+ * _8_ 8 9
+ *
+ * A `Comb` as described by this C++ class is a `U-comb`, where
+ * `U` is the set of events that UDPOR has explored. That is,
+ * the comb is over a set of events
+ */
+class Comb : public std::vector<Spike> {
+public:
+ explicit Comb(unsigned k) : std::vector<Spike>(k) {}
+ Comb(const Comb& other) = default;
+ Comb(Comb&& other) = default;
+ Comb& operator=(const Comb& other) = default;
+ Comb& operator=(Comb&& other) = default;
+
+ auto combinations_begin() const
+ {
+ std::vector<std::reference_wrapper<const Spike>> references;
+ std::transform(begin(), end(), std::back_inserter(references), [](const Spike& spike) { return std::cref(spike); });
+ return simgrid::xbt::variable_for_loop<const Spike>(std::move(references));
+ }
+ auto combinations_end() const { return simgrid::xbt::variable_for_loop<const Spike>(); }
+};
+
+} // namespace simgrid::mc::udpor
+#endif
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/Comb.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
#include "xbt/asserts.h"
{
}
+Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_history())
+{
+ // The local configuration should always be a valid configuration. We
+ // check the invariant regardless as a sanity check
+}
+
Configuration::Configuration(const EventSet& events) : events_(events)
{
if (!events_.is_valid_configuration()) {
}
}
+Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+
void Configuration::add_event(const UnfoldingEvent* e)
{
if (e == nullptr) {
}
}
+bool Configuration::is_compatible_with(const UnfoldingEvent* e) const
+{
+ return not e->conflicts_with(*this);
+}
+
+bool Configuration::is_compatible_with(const History& history) const
+{
+ return std::none_of(history.begin(), history.end(),
+ [&](const UnfoldingEvent* e) { return e->conflicts_with(*this); });
+}
+
std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
{
return this->events_.get_topological_ordering();
return minimally_reproducible_events;
}
+std::optional<Configuration> Configuration::compute_alternative_to(const EventSet& D, const Unfolding& U) const
+{
+ // A full alternative can be computed by checking against everything in D
+ return compute_k_partial_alternative_to(D, U, D.size());
+}
+
+std::optional<Configuration> Configuration::compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U,
+ size_t k) const
+{
+ // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
+ const auto D_hat = [&]() {
+ const size_t size = std::min(k, D.size());
+ std::vector<const UnfoldingEvent*> D_hat(size);
+ // TODO: Since any subset suffices for computing `k`-partial alternatives,
+ // potentially select intelligently here (e.g. perhaps pick events
+ // with transitions that we know are totally independent). This may be
+ // especially important if the enumeration is the slowest part of
+ // UDPOR
+ //
+ // For now, simply pick the first `k` events
+ std::copy_n(D.begin(), size, D_hat.begin());
+ return D_hat;
+ }();
+
+ // 2. Build a U-comb <s_1, ..., s_k> of size k, where spike `s_i` contains
+ // all events in conflict with `e_i`
+ //
+ // 3. EXCEPT those events e' for which [e'] + C is not a configuration or
+ // [e'] intersects D
+ //
+ // NOTE: This is an expensive operation as we must traverse the entire unfolding
+ // and compute `C.is_compatible_with(History)` for every event in the structure :/.
+ // A later performance improvement would be to incorporate the work of Nguyen et al.
+ // into SimGrid which associated additonal data structures with each unfolding event.
+ // Since that is a rather complicated addition, we defer it to a later time...
+ Comb comb(k);
+
+ for (const auto* e : U) {
+ for (unsigned i = 0; i < k; i++) {
+ const UnfoldingEvent* e_i = D_hat[i];
+ if (const auto e_local_config = History(e);
+ e_i->conflicts_with(e) and (not D.intersects(e_local_config)) and is_compatible_with(e_local_config)) {
+ comb[i].push_back(e);
+ }
+ }
+ }
+
+ // 4. Find any such combination <e_1', ..., e_k'> in comb satisfying
+ // ~(e_i' # e_j') for i != j
+ //
+ // NOTE: This is a VERY expensive operation: it enumerates all possible
+ // ways to select an element from each spike. Unfortunately there's no
+ // way around the enumeration, as computing a full alternative in general is
+ // NP-complete (although computing the k-partial alternative is polynomial in
+ // the number of events)
+ const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
+ std::vector<const UnfoldingEvent*> events;
+ for (const auto& event_in_spike : spikes) {
+ events.push_back(*event_in_spike);
+ }
+ return EventSet(std::move(events));
+ };
+ const auto alternative =
+ std::find_if(comb.combinations_begin(), comb.combinations_end(),
+ [&map_events](const auto& vector) { return map_events(vector).is_conflict_free(); });
+
+ // No such alternative exists
+ if (alternative == comb.combinations_end()) {
+ return std::nullopt;
+ }
+
+ // 5. J := [e_1] + [e_2] + ... + [e_k] is a k-partial alternative
+ return Configuration(History(map_events(*alternative)));
+}
+
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <optional>
+
namespace simgrid::mc::udpor {
class Configuration {
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
+ explicit Configuration(const UnfoldingEvent* event);
explicit Configuration(const EventSet& events);
+ explicit Configuration(const History& history);
explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
auto begin() const { return this->events_.begin(); }
*/
void add_event(const UnfoldingEvent* e);
+ /**
+ * @brief Whether or not the given event can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
+ bool is_compatible_with(const UnfoldingEvent* e) const;
+
+ /**
+ * @brief Whether or not the events in the given history can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
+ bool is_compatible_with(const History& history) const;
+
+ std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
+ std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
+
/**
* @brief Orders the events of the configuration such that
* "more recent" events (i.e. those that are farther down in
* of the events returned by this method is equal to the set of events
* in this configuration
*
- * @returns the smallest set of events whose events generates this configuration
- * (denoted `config(E)`)
+ * @returns the smallest set of events whose events generates
+ * this configuration (denoted `config(E)`)
*/
EventSet get_minimally_reproducible_events() const;
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
// Iteration with events directly should now also be finished
REQUIRE(first_events == last);
}
+}
+
+TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Reader/Writer Example")
+{
+ // The following tests concern the given event structure that is given as
+ // an example in figure 1 of the original UDPOR paper.
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // Theses tests walk through exactly the configurations and sets of `D` that
+ // UDPOR COULD encounter as it walks through the unfolding. Note that
+ // if there are multiple alternatives to any given configuration, UDPOR can
+ // continue searching any one of them. The sequence assumes UDPOR first picks `e1`,
+ // then `e4`, and then `e7`
+ Unfolding U;
+
+ auto e0 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<ConditionallyDependentAction>());
+ auto e0_handle = e0.get();
+
+ auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<DependentAction>());
+ auto e1_handle = e1.get();
+
+ auto e2 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e2_handle = e2.get();
+
+ auto e3 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e3_handle = e3.get();
+
+ auto e4 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e4_handle = e4.get();
+
+ auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}), std::make_shared<DependentAction>());
+ auto e5_handle = e5.get();
+
+ auto e6 = std::make_unique<UnfoldingEvent>(EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e6_handle = e6.get();
+
+ auto e7 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e7_handle = e7.get();
+
+ auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}), std::make_shared<DependentAction>());
+ auto e8_handle = e8.get();
+
+ auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<DependentAction>());
+ auto e9_handle = e9.get();
+
+ auto e10 = std::make_unique<UnfoldingEvent>(EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e10_handle = e10.get();
+
+ SECTION("Alternative computation call 1")
+ {
+ // During the first call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // /
+ // / /
+ // e2 e3
+ //
+ // C := {e0, e1, e2} and `Explore(C, D, A)` picked `e3`
+ // (since en(C') where C' := {e0, e1, e2, e3} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is empty at first)
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e1, e2}, {e3})
+ //
+ // where U is given above. There are no alternatives in
+ // this case since `e4` and `e7` conflict with `e1` (so
+ // they cannot be added to C to form a configuration)
+ const Configuration C{e0_handle, e1_handle, e2_handle};
+ const EventSet D_plus_e{e3_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 2")
+ {
+ // During the second call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // /
+ // / /
+ // e2 e3
+ //
+ // C := {e0, e1} and `Explore(C, D, A)` picked `e2`.
+ //
+ // Thus the computation is (since D is still empty)
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e1}, {e2})
+ //
+ // where U is given above. There are no alternatives in
+ // this case since `e4` and `e7` conflict with `e1` (so
+ // they cannot be added to C to form a configuration) and
+ // e3 is NOT in conflict with either e0 or e1
+ const Configuration C{e0_handle, e1_handle};
+ const EventSet D_plus_e{e2_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 3")
+ {
+ // During the thrid call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // /
+ // / /
+ // e2 e3
+ //
+ // C := {e0} and `Explore(C, D, A)` picked `e1`.
+ //
+ // Thus the computation is (since D is still empty)
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1})
+ //
+ // where U is given above. There are two alternatives in this case:
+ // {e0, e4} and {e0, e7}. Either one would be a valid choice for
+ // UDPOR, so we must check for the precense of either
+ const Configuration C{e0_handle};
+ const EventSet D_plus_e{e1_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE(alternative.has_value());
+
+ // The first alternative that is found is the one that is chosen. Since
+ // traversal over the elements of an unordered_set<> are not guaranteed,
+ // both {e0, e4} and {e0, e7} are valid alternatives
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
+ }
+
+ SECTION("Alternative computation call 4")
+ {
+ // During the fourth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / //
+ // / / e5 e8
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4, e5} and `Explore(C, D, A)` picked `e6`
+ // (since en(C') where C' := {e0, e4, e5, e6} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is {e1})
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4, e5}, {e1, e6})
+ //
+ // where U is given above. There are no alternatives in this
+ // case, since:
+ //
+ // 1.`e2/e3` are eliminated since their histories contain `e1`
+ // 2. `e7/e8` are eliminated because they conflict with `e5`
+ const Configuration C{e0_handle, e4_handle, e5_handle};
+ const EventSet D_plus_e{e1_handle, e6_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 5")
+ {
+ // During the fifth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / //
+ // / / e5 e8
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4} and `Explore(C, D, A)` picked `e5`
+ // (since en(C') where C' := {e0, e4, e5, e6} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is {e1})
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5})
+ //
+ // where U is given above. There are THREE alternatives in this case,
+ // viz. {e0, e7}, {e0, e4, e7} and {e0, e4, e7, e8}.
+ //
+ // To continue the search, UDPOR computes J / C which in this
+ // case gives {e7, e8}. Since `e8` is not in en(C), UDPOR will
+ // choose `e7` next and add `e5` to `D`
+ const Configuration C{e0_handle, e4_handle};
+ const EventSet D_plus_e{e1_handle, e5_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ REQUIRE(U.size() == 8);
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE(alternative.has_value());
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e7_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle})));
+ }
+
+ SECTION("Alternative computation call 6")
+ {
+ // During the sixth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4, e7} and `Explore(C, D, A)` picked `e8`
+ // (since en(C') where C' := {e0, e4, e7, e8} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is {e1, e5} [see the last step])
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4, e7}, {e1, e5, e8})
+ //
+ // where U is given above. There are no alternatives in this case
+ // since all `e9` conflicts with `e4` and all other events of `U`
+ // are eliminated since their history intersects `D`
+ const Configuration C{e0_handle, e4_handle, e7_handle};
+ const EventSet D_plus_e{e1_handle, e5_handle, e8_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 7")
+ {
+ // During the seventh call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4} and `Explore(C, D, A)` picked `e7`
+ //
+ // Thus the computation is (since D is {e1, e5} [see call 5])
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5, e7})
+ //
+ // where U is given above. There are no alternatives again in this case
+ // since all `e9` conflicts with `e4` and all other events of `U`
+ // are eliminated since their history intersects `D`
+ const Configuration C{e0_handle, e4_handle};
+ const EventSet D_plus_e{e1_handle, e5_handle, e7_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 8")
+ {
+ // During the eigth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0} and `Explore(C, D, A)` picked `e4`. At this
+ // point, UDPOR finished its recursive search of {e0, e4}
+ // after having finished {e0, e1} prior.
+ //
+ // Thus the computation is (since D = {e1})
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4})
+ //
+ // where U is given above. There is one alternative in this
+ // case, viz {e0, e7, e9} since
+ // 1. e9 conflicts with e4 in D
+ // 2. e7 conflicts with e1 in D
+ // 3. the set {e7, e9} is conflict-free since `e7 < e9`
+ // 4. all other events are eliminated since their histories
+ // intersect D
+ //
+ // UDPOR will continue its recursive search following `e7`
+ // and add `e4` to D
+ const Configuration C{e0_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE(alternative.has_value());
+ REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
+ }
+
+ SECTION("Alternative computation call 9")
+ {
+ // During the ninth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // C := {e0, e7, e9} and `Explore(C, D, A)` picked `e10`.
+ // (since en(C') where C' := {e0, e7, e9, e10} is empty
+ // [so UDPOR will simply return when C' is reached]).
+ //
+ // Thus the computation is (since D = {e1, e4} [see the previous step])
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e10})
+ //
+ // where U is given above. There are no alternatives in this case
+ const Configuration C{e0_handle, e7_handle, e9_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle, e10_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 10")
+ {
+ // During the tenth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // C := {e0, e7} and `Explore(C, D, A)` picked `e9`.
+ //
+ // Thus the computation is (since D = {e1, e4} [see call 8])
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e9})
+ //
+ // where U is given above. There are no alternatives in this case
+ const Configuration C{e0_handle, e7_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 11 (final call)")
+ {
+ // During the eleventh and final call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // C := {e0} and `Explore(C, D, A)` picked `e7`.
+ //
+ // Thus the computation is (since D = {e1, e4} [see call 8])
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e7})
+ //
+ // where U is given above. There are no alternatives in this case:
+ // everyone is eliminated!
+ const Configuration C{e0_handle, e7_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation next")
+ {
+ SECTION("Followed {e0, e7} first")
+ {
+ const EventSet D{e1_handle, e7_handle};
+ const Configuration C{e0_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e5));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D, U);
+ REQUIRE(alternative.has_value());
+
+ // In this case, only {e0, e4} is a valid alternative
+ REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e5_handle}));
+ }
+
+ SECTION("Followed {e0, e4} first")
+ {
+ const EventSet D{e1_handle, e4_handle};
+ const Configuration C{e0_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e5));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D, U);
+ REQUIRE(alternative.has_value());
+
+ // In this case, only {e0, e7} is a valid alternative
+ REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
+ }
+ }
}
\ No newline at end of file
return make_union(config.get_events());
}
+EventSet EventSet::get_local_config() const
+{
+ return History(*this).get_all_events();
+}
+
size_t EventSet::size() const
{
return this->events_.size();
return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
}
+bool EventSet::intersects(const History& history) const
+{
+ return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
+}
+
bool EventSet::is_maximal() const
{
// A set of events is maximal if no event from
EventSet make_union(const UnfoldingEvent*) const;
EventSet make_union(const EventSet&) const;
EventSet make_union(const Configuration&) const;
+ EventSet get_local_config() const;
size_t size() const;
bool empty() const;
bool contains(const UnfoldingEvent*) const;
bool contains(const History&) const;
+ bool intersects(const History&) const;
bool is_subset_of(const EventSet&) const;
bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
namespace simgrid::mc::udpor {
+void Unfolding::remove(const EventSet& events)
+{
+ for (const auto e : events) {
+ remove(e);
+ }
+}
+
void Unfolding::remove(const UnfoldingEvent* e)
{
if (e == nullptr) {
throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL");
}
this->global_events_.erase(e);
+ this->event_handles.remove(e);
}
void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
}
// Map the handle to its owner
+ this->event_handles.insert(handle);
this->global_events_[handle] = std::move(e);
}
{
// Notice the use of `==` equality here. `e` may not be contained in the
// unfolding; but some event which is "equivalent" to it could be.
- for (const auto& [event, _] : global_events_) {
+ for (const auto event : *this) {
if (*event == *e) {
return true;
}
return false;
}
+EventSet Unfolding::get_immediate_conflicts_of(const UnfoldingEvent* e) const
+{
+ EventSet immediate_conflicts;
+ for (const auto event : *this) {
+ if (event->immediately_conflicts_with(e)) {
+ immediate_conflicts.insert(e);
+ }
+ }
+ return immediate_conflicts;
+}
+
} // namespace simgrid::mc::udpor
#ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
#define SIMGRID_MC_UDPOR_UNFOLDING_HPP
+#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
*/
std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+ /**
+ * @brief: The collection of events in the unfolding
+ *
+ * @invariant: All of the events in this set are elements of `global_events_`
+ * and is kept updated at the same time as `global_events_`
+ */
+ EventSet event_handles;
+
+ /**
+ * @brief The "irrelevant" portions of the unfolding that do not need to be kept
+ * around to ensure that UDPOR functions correctly
+ *
+ * The set `G` is another global variable maintained by the UDPOR algorithm which
+ * is used to keep track of all events which used to be important to UDPOR.
+ *
+ * @note: The current implementation does not touch the set `G`. Its use is perhaps
+ * limited to debugging and/or model-checking acyclic state spaces
+ */
+ EventSet G;
+
public:
Unfolding() = default;
Unfolding& operator=(Unfolding&&) = default;
Unfolding(Unfolding&&) = default;
void remove(const UnfoldingEvent* e);
+ void remove(const EventSet& events);
void insert(std::unique_ptr<UnfoldingEvent> e);
bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
+ auto begin() const { return this->event_handles.begin(); }
+ auto end() const { return this->event_handles.end(); }
+ auto cbegin() const { return this->event_handles.cbegin(); }
+ auto cend() const { return this->event_handles.cend(); }
size_t size() const { return this->global_events_.size(); }
bool empty() const { return this->global_events_.empty(); }
+
+ /// @brief Computes "#ⁱ_U(e)" for the given event
+ EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
};
} // namespace simgrid::mc::udpor
bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
{
- // Must be run by the same actor
- if (associated_transition->aid_ != other.associated_transition->aid_)
- return false;
-
- // If run by the same actor, must be the same _step_ of that actor's
- // execution
-
- // TODO: Add in information to determine which step in the sequence this actor was executed
-
- // All unfolding event objects are created in reference to
- // an Unfolding object which owns them. Hence, the references
+ // Two events are equivalent iff:
+ // 1. they have the same action
+ // 2. they have the same history
+ //
+ // NOTE: All unfolding event objects are created in reference to
+ // an `Unfolding` object which owns them. Hence, the references
// they contain to other events in the unfolding can
// be used as intrinsic identities (i.e. we don't need to
// recursively check if each of our causes has a `==` in
// the other event's causes)
- return this->immediate_causes == other.immediate_causes;
+ return associated_transition->aid_ == other.associated_transition->aid_ &&
+ associated_transition->type_ == other.associated_transition->type_ &&
+ associated_transition->times_considered_ == other.associated_transition->times_considered_ &&
+ this->immediate_causes == other.immediate_causes;
}
EventSet UnfoldingEvent::get_history() const
bool in_history_of(const UnfoldingEvent* other) const;
bool related_to(const UnfoldingEvent* other) const;
+ /// @brief Whether or not this event is in conflict with
+ /// the given one (i.e. whether `this # other`)
bool conflicts_with(const UnfoldingEvent* other) const;
+
+ /// @brief Whether or not this event is in conflict with
+ /// any event in the given configuration
bool conflicts_with(const Configuration& config) const;
+
+ /// @brief Computes "this #ⁱ other"
bool immediately_conflicts_with(const UnfoldingEvent* other) const;
bool is_dependent_with(const Transition*) const;
bool is_dependent_with(const UnfoldingEvent* other) const;
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
+TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Semantic Equivalence Tests")
+{
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e4(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+ UnfoldingEvent e5(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e6(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e7(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+ SECTION("Equivalence is an equivalence relation")
+ {
+ SECTION("Equivalence is reflexive")
+ {
+ REQUIRE(e1 == e1);
+ REQUIRE(e2 == e2);
+ REQUIRE(e3 == e3);
+ REQUIRE(e4 == e4);
+ }
+
+ SECTION("Equivalence is symmetric")
+ {
+ REQUIRE(e2 == e3);
+ REQUIRE(e3 == e2);
+ REQUIRE(e3 == e4);
+ REQUIRE(e4 == e3);
+ REQUIRE(e2 == e4);
+ REQUIRE(e4 == e2);
+ }
+
+ SECTION("Equivalence is transitive")
+ {
+ REQUIRE(e2 == e3);
+ REQUIRE(e3 == e4);
+ REQUIRE(e2 == e4);
+ REQUIRE(e5 == e6);
+ REQUIRE(e6 == e7);
+ REQUIRE(e5 == e7);
+ }
+ }
+
+ SECTION("Equivalence fails with different actors")
+ {
+ UnfoldingEvent e1_diff_actor(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ UnfoldingEvent e2_diff_actor(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ UnfoldingEvent e5_diff_actor(EventSet({&e1, &e3, &e2}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ REQUIRE(e1 != e1_diff_actor);
+ REQUIRE(e1 != e2_diff_actor);
+ REQUIRE(e1 != e5_diff_actor);
+ }
+
+ SECTION("Equivalence fails with different transition types")
+ {
+ // NOTE: We're comparing the transition `type_` field directly. To avoid
+ // modifying the `Type` enum that exists in `Transition` just for the tests,
+ // we instead provide different values of `Transition::Type` to simulate
+ // the different types
+ UnfoldingEvent e1_diff_transition(EventSet(),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ UnfoldingEvent e2_diff_transition(EventSet({&e1}),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ UnfoldingEvent e5_diff_transition(EventSet({&e1, &e3, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ REQUIRE(e1 != e1_diff_transition);
+ REQUIRE(e1 != e2_diff_transition);
+ REQUIRE(e1 != e5_diff_transition);
+ }
+
+ SECTION("Equivalence fails with different `times_considered`")
+ {
+ // With a different number for `times_considered`, we know
+ UnfoldingEvent e1_diff_considered(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ UnfoldingEvent e2_diff_considered(EventSet({&e1}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ UnfoldingEvent e5_diff_considered(EventSet({&e1, &e3, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ REQUIRE(e1 != e1_diff_considered);
+ REQUIRE(e1 != e2_diff_considered);
+ REQUIRE(e1 != e5_diff_considered);
+ }
+
+ SECTION("Equivalence fails with different immediate histories of events")
+ {
+ UnfoldingEvent e1_diff_hist(EventSet({&e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e2_diff_hist(EventSet({&e3}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e5_diff_hist(EventSet({&e1, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ REQUIRE(e1 != e1_diff_hist);
+ REQUIRE(e1 != e2_diff_hist);
+ REQUIRE(e1 != e5_diff_hist);
+ }
+}
+
TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Dependency/Conflict Tests")
{
SECTION("Properties of the relations")
#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding")
unfolding.remove(e2_handle);
REQUIRE(unfolding.size() == 0);
REQUIRE(unfolding.empty());
-}
\ No newline at end of file
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events")
+{
+ Unfolding unfolding;
+ auto e1 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
+ auto e2 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
+
+ // e1 and e2 are equivalent
+ REQUIRE(*e1 == *e2);
+
+ const auto e1_handle = e1.get();
+ const auto e2_handle = e2.get();
+ unfolding.insert(std::move(e1));
+
+ REQUIRE(unfolding.contains_event_equivalent_to(e1_handle));
+ REQUIRE(unfolding.contains_event_equivalent_to(e2_handle));
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Checking all immediate conflicts restricted to an unfolding") {}
\ No newline at end of file
#ifndef SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
#define SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
+#include "src/mc/transition/Transition.hpp"
+
namespace simgrid::mc::udpor {
struct IndependentAction : public Transition {
+ IndependentAction() = default;
+ IndependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+
// Independent with everyone else
bool depends(const Transition* other) const override { return false; }
};
struct DependentAction : public Transition {
+ DependentAction() = default;
+ DependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+
// Dependent with everyone else (except IndependentAction)
bool depends(const Transition* other) const override
{
};
struct ConditionallyDependentAction : public Transition {
+ ConditionallyDependentAction() = default;
+ ConditionallyDependentAction(Type type, aid_t issuer, int times_considered)
+ : Transition(type, issuer, times_considered)
+ {
+ }
+
// Dependent only with DependentAction (i.e. not itself)
bool depends(const Transition* other) const override
{
xbt_assert(errno == 0 && raise(SIGSTOP) == 0, "Could not wait for the model-checker (errno = %d: %s)", errno,
strerror(errno));
- s_mc_message_initial_addresses_t message = {};
- message.type = MessageType::INITIAL_ADDRESSES;
- message.mmalloc_default_mdp = mmalloc_get_current_heap();
- xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
-
instance_->handle_messages();
return instance_.get();
}
if (terminate_asap)
::_Exit(0);
}
+void AppSide::handle_initial_addresses()
+{
+ this->need_memory_info_ = true;
+ s_mc_message_initial_addresses_reply_t answer = {};
+ answer.type = MessageType::INITIAL_ADDRESSES_REPLY;
+ answer.mmalloc_default_mdp = mmalloc_get_current_heap();
+ xbt_assert(channel_.send(answer) == 0, "Could not send response with initial addresses.");
+}
void AppSide::handle_actors_status() const
{
auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size, \
sizeof(_type_))
-void AppSide::handle_messages() const
+void AppSide::handle_messages()
{
while (true) { // Until we get a CONTINUE message
XBT_DEBUG("Waiting messages from model-checker");
handle_finalize((s_mc_message_int_t*)message_buffer.data());
break;
+ case MessageType::INITIAL_ADDRESSES:
+ assert_msg_size("INITIAL_ADDRESSES", s_mc_message_t);
+ handle_initial_addresses();
+ break;
+
case MessageType::ACTORS_STATUS:
assert_msg_size("ACTORS_STATUS", s_mc_message_t);
handle_actors_status();
}
}
-void AppSide::main_loop() const
+void AppSide::main_loop()
{
simgrid::mc::processes_time.resize(simgrid::kernel::actor::ActorImpl::get_maxpid());
MC_ignore_heap(simgrid::mc::processes_time.data(),
}
}
-void AppSide::report_assertion_failure() const
+void AppSide::report_assertion_failure()
{
xbt_assert(channel_.send(MessageType::ASSERTION_FAILED) == 0, "Could not send assertion to model-checker");
this->handle_messages();
void AppSide::ignore_memory(void* addr, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_ignore_memory_t message = {};
void AppSide::ignore_heap(void* address, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
void AppSide::unignore_heap(void* address, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_ignore_memory_t message = {};
void AppSide::declare_symbol(const char* name, int* value) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_) {
+ XBT_CRITICAL("Ignore AppSide::declare_symbol(%s)", name);
return;
+ }
s_mc_message_register_symbol_t message = {};
message.type = MessageType::REGISTER_SYMBOL;
*/
void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
private:
Channel channel_;
static std::unique_ptr<AppSide> instance_;
+ bool need_memory_info_ = false; /* by default we don't send memory info, unless we got a INITIAL_ADDRESSES */
public:
AppSide();
explicit AppSide(int fd) : channel_(fd) {}
- void handle_messages() const;
+ void handle_messages();
private:
void handle_deadlock_check(const s_mc_message_t* msg) const;
void handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const;
void handle_finalize(const s_mc_message_int_t* msg) const;
+ void handle_initial_addresses();
void handle_actors_status() const;
void handle_actors_maxpid() const;
public:
Channel const& get_channel() const { return channel_; }
Channel& get_channel() { return channel_; }
- XBT_ATTRIB_NORETURN void main_loop() const;
- void report_assertion_failure() const;
+ XBT_ATTRIB_NORETURN void main_loop();
+ void report_assertion_failure();
void ignore_memory(void* addr, std::size_t size) const;
void ignore_heap(void* addr, std::size_t size) const;
void unignore_heap(void* addr, std::size_t size) const;
void CheckerSide::setup_events()
{
+ if (base_ != nullptr)
+ event_base_free(base_.get());
auto* base = event_base_new();
base_.reset(base);
- auto* socket_event = event_new(
+ socket_event_ = event_new(
base, get_channel().get_socket(), EV_READ | EV_PERSIST,
- [](evutil_socket_t sig, short events, void* arg) {
+ [](evutil_socket_t, short events, void* arg) {
auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
if (events == EV_READ) {
std::array<char, MC_MESSAGE_LENGTH> buffer;
}
},
this);
- event_add(socket_event, nullptr);
- socket_event_.reset(socket_event);
+ event_add(socket_event_, nullptr);
- auto* signal_event = event_new(
+ signal_event_ = event_new(
base, SIGCHLD, EV_SIGNAL | EV_PERSIST,
[](evutil_socket_t sig, short events, void* arg) {
auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
}
},
this);
- event_add(signal_event, nullptr);
- signal_event_.reset(signal_event);
+ event_add(signal_event_, nullptr);
}
-CheckerSide::CheckerSide(const std::vector<char*>& args) : running_(true)
+CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_introspection) : running_(true)
{
// Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor)
// and the application process (child)
setup_events();
wait_application_process(pid_);
+ // Request the initial memory on need
+ if (need_memory_introspection) {
+ channel_.send(MessageType::INITIAL_ADDRESSES);
+ s_mc_message_initial_addresses_reply_t answer;
+ ssize_t answer_size = channel_.receive(answer);
+ xbt_assert(answer_size != -1, "Could not receive message");
+ xbt_assert(answer.type == MessageType::INITIAL_ADDRESSES_REPLY,
+ "The received message is not the INITIAL_ADDRESS_REPLY I was expecting but of type %s",
+ to_c_str(answer.type));
+ xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
+
+ /* We now have enough info to create the memory address space */
+ remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, answer.mmalloc_default_mdp);
+ }
+
wait_for_requests();
}
+CheckerSide::~CheckerSide()
+{
+ event_del(socket_event_);
+ event_free(socket_event_);
+ event_del(signal_event_);
+ event_free(signal_event_);
+
+ if (running()) {
+ XBT_DEBUG("Killing process");
+ finalize(true);
+ kill(get_pid(), SIGKILL);
+ terminate();
+ handle_waitpid();
+ }
+}
+
+void CheckerSide::finalize(bool terminate_asap)
+{
+ s_mc_message_int_t m = {};
+ m.type = MessageType::FINALIZE;
+ m.value = terminate_asap;
+ xbt_assert(get_channel().send(m) == 0, "Could not ask the app to finalize on need");
+
+ s_mc_message_t answer;
+ ssize_t s = get_channel().receive(answer);
+ xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+ xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
+ xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
+ "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
+ (int)answer.type, (int)MessageType::FINALIZE_REPLY);
+}
+
void CheckerSide::dispatch_events() const
{
event_base_dispatch(base_.get());
memcpy(&base_message, buffer, sizeof(base_message));
switch (base_message.type) {
- case MessageType::INITIAL_ADDRESSES: {
- s_mc_message_initial_addresses_t message;
- xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size,
- (int)sizeof(message));
- memcpy(&message, buffer, sizeof(message));
- /* Create the memory address space, now that we have the mandatory information */
- remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, message.mmalloc_default_mdp);
- break;
- }
-
case MessageType::IGNORE_HEAP: {
- s_mc_message_ignore_heap_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
-
- IgnoredHeapRegion region;
- region.block = message.block;
- region.fragment = message.fragment;
- region.address = message.address;
- region.size = message.size;
- get_remote_memory().ignore_heap(region);
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_heap_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ get_remote_memory()->ignore_heap(region);
+ } else {
+ XBT_INFO("Ignoring a IGNORE_HEAP message because we don't need to introspect memory.");
+ }
break;
}
case MessageType::UNIGNORE_HEAP: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->unignore_heap((void*)message.addr, message.size);
+ } else {
+ XBT_INFO("Ignoring an UNIGNORE_HEAP message because we don't need to introspect memory.");
+ }
break;
}
case MessageType::IGNORE_MEMORY: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_memory().ignore_region(message.addr, message.size);
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->ignore_region(message.addr, message.size);
+ } else {
+ XBT_INFO("Ignoring an IGNORE_MEMORY message because we don't need to introspect memory.");
+ }
break;
}
case MessageType::STACK_REGION: {
- s_mc_message_stack_region_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_memory().stack_areas().push_back(message.stack_region);
- } break;
+ if (remote_memory_ != nullptr) {
+ s_mc_message_stack_region_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->stack_areas().push_back(message.stack_region);
+ } else {
+ XBT_INFO("Ignoring an STACK_REGION message because we don't need to introspect memory.");
+ }
+ break;
+ }
case MessageType::REGISTER_SYMBOL: {
s_mc_message_register_symbol_t message;
xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
XBT_DEBUG("Received symbol: %s", message.name.data());
- LivenessChecker::automaton_register_symbol(get_remote_memory(), message.name.data(), remote((int*)message.data));
+ LivenessChecker::automaton_register_symbol(*get_remote_memory(), message.name.data(), remote((int*)message.data));
break;
}
xbt_assert(not this->running(), "Inconsistent state");
break;
} else {
- XBT_ERROR("Could not wait for pid");
- throw simgrid::xbt::errno_error();
+ xbt_die("Could not wait for pid: %s", strerror(errno));
}
}
/* CheckerSide: All what the checker needs to interact with a given application process */
class CheckerSide {
+ event* socket_event_;
+ event* signal_event_;
std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
- std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, &event_free};
- std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, &event_free};
std::unique_ptr<RemoteProcessMemory> remote_memory_;
- Channel channel_;
+ Channel channel_;
bool running_ = false;
pid_t pid_;
void handle_waitpid();
public:
- explicit CheckerSide(const std::vector<char*>& args);
+ explicit CheckerSide(const std::vector<char*>& args, bool need_memory_introspection);
+ ~CheckerSide();
// No copy:
CheckerSide(CheckerSide const&) = delete;
void break_loop() const;
void wait_for_requests();
+ /** Ask the application to run post-mortem analysis, and maybe to stop ASAP */
+ void finalize(bool terminate_asap = false);
+
/* Interacting with the application process */
pid_t get_pid() const { return pid_; }
bool running() const { return running_; }
void terminate() { running_ = false; }
- RemoteProcessMemory& get_remote_memory() { return *remote_memory_.get(); }
+ RemoteProcessMemory* get_remote_memory() { return remote_memory_.get(); }
};
} // namespace simgrid::mc
// ***** Messages
namespace simgrid::mc {
-XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
- STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
- SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID,
- ACTORS_MAXPID_REPLY, FINALIZE, FINALIZE_REPLY);
+XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, INITIAL_ADDRESSES_REPLY, CONTINUE, IGNORE_HEAP,
+ UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK,
+ DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE, SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED,
+ ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID, ACTORS_MAXPID_REPLY, FINALIZE,
+ FINALIZE_REPLY);
} // namespace simgrid::mc
constexpr unsigned MC_MESSAGE_LENGTH = 512;
};
/* Client->Server */
-struct s_mc_message_initial_addresses_t {
- simgrid::mc::MessageType type;
- xbt_mheap_t mmalloc_default_mdp;
-};
-
struct s_mc_message_ignore_heap_t {
simgrid::mc::MessageType type;
int block;
};
/* Server -> client */
+struct s_mc_message_initial_addresses_reply_t {
+ simgrid::mc::MessageType type;
+ xbt_mheap_t mmalloc_default_mdp;
+};
+
struct s_mc_message_simcall_execute_t {
simgrid::mc::MessageType type;
aid_t aid_;
namespace simgrid::mc {
-Region::Region(PageStore& store, RemoteProcessMemory& memory, RegionType region_type, void* start_addr, size_t size)
+Region::Region(PageStore& store, const RemoteProcessMemory& memory, RegionType region_type, void* start_addr,
+ size_t size)
: region_type_(region_type), start_addr_(start_addr), size_(size)
{
xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize - 1)) == 0, "Start address not at the beginning of a page");
*
* @param region Target region
*/
-void Region::restore(RemoteProcessMemory& memory) const
+void Region::restore(const RemoteProcessMemory& memory) const
{
xbt_assert(((start().address()) & (xbt_pagesize - 1)) == 0, "Not at the beginning of a page");
xbt_assert(simgrid::mc::mmu::chunk_count(size()) == get_chunks().page_count());
ChunkedData chunks_;
public:
- Region(PageStore& store, RemoteProcessMemory& memory, RegionType type, void* start_addr, size_t size);
+ Region(PageStore& store, const RemoteProcessMemory& memory, RegionType type, void* start_addr, size_t size);
Region(Region const&) = delete;
Region& operator=(Region const&) = delete;
Region(Region&& that) = delete;
bool contain(RemotePtr<void> p) const { return p >= start() && p < end(); }
/** @brief Restore a region from a snapshot */
- void restore(RemoteProcessMemory& memory) const;
+ void restore(const RemoteProcessMemory& memory) const;
/** @brief Read memory that was snapshotted in this region
*
}
Snapshot::Snapshot(long num_state, PageStore& store, RemoteProcessMemory& memory)
- : AddressSpace(memory), page_store_(store), num_state_(num_state)
+ : AddressSpace(&memory), page_store_(store), num_state_(num_state)
{
XBT_DEBUG("Taking snapshot %ld", num_state);
}
}
-int some_global_variable = 42;
-void* some_global_pointer = &some_global_variable;
+const int some_global_variable = 42;
+const void* some_global_pointer = &some_global_variable;
void snap_test_helper::read_pointer()
{
prologue_return ret = prologue(1);
{
short s;
xbt_assert(stream >> s >> objaddr_ >> objname_ >> file_ >> line_);
- type_ = static_cast<simgrid::mc::ObjectAccessType>(s);
+ access_type_ = static_cast<simgrid::mc::ObjectAccessType>(s);
}
std::string ObjectAccessTransition::to_string(bool verbose) const
{
std::string res;
- if (type_ == ObjectAccessType::ENTER)
+ if (access_type_ == ObjectAccessType::ENTER)
res = std::string("BeginObjectAccess(");
- else if (type_ == ObjectAccessType::EXIT)
+ else if (access_type_ == ObjectAccessType::EXIT)
res = std::string("EndObjectAccess(");
else
res = std::string("ObjectAccess(");
XBT_DECLARE_ENUM_CLASS(ObjectAccessType, ENTER, EXIT, BOTH);
class ObjectAccessTransition : public Transition {
- ObjectAccessType type_;
+ ObjectAccessType access_type_;
void* objaddr_;
std::string objname_;
std::string file_;
src/mc/explo/LivenessChecker.hpp
src/mc/explo/UdporChecker.cpp
src/mc/explo/UdporChecker.hpp
-
+
+ src/mc/explo/udpor/Comb.hpp
src/mc/explo/udpor/Configuration.hpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/EventSet.cpp
if [ "$runtests" = "ON" ]; then
# exclude tests known to fail with _GLIBCXX_DEBUG
- ctest -j$NUMPROC -E '^[ps]thread-|mc-bugged1-liveness'
+ ctest -j$NUMPROC -E '^[ps]thread-|mc-bugged1-liveness' --output-on-failure
fi
cd ..
