From: mlaurent Date: Thu, 23 Mar 2023 08:58:49 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.34~240^2~10 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/50753d5f8442a47c17c4035724201a18a7ff6146?hp=a6d5fdeb22df5f5b1ca02a3dad8ba6094202a4f3 Merge branch 'master' of https://framagit.org/simgrid/simgrid --- diff --git a/MANIFEST.in b/MANIFEST.in index 3bd5a10520..1eea8b7924 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2168,6 +2168,7 @@ include src/mc/explo/LivenessChecker.hpp 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 diff --git a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp index bab673122f..241322650e 100644 --- a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp +++ b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp @@ -47,7 +47,7 @@ static void workerScopedLock(sg4::MutexPtr mutex, int& result) 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 result(cfg_actor_count.get()); diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index a52b8fcddf..8e19472627 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -19,12 +19,12 @@ namespace simgrid::mc { /** @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(state_number, remote_app.get_page_store(), - remote_app.get_remote_process_memory()); + *remote_app.get_remote_process_memory()); } void VisitedStates::prune() @@ -59,7 +59,7 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g 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 old_state = std::move(visited_state); diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 2ddd5c0876..45e595eed6 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -29,22 +29,31 @@ XBT_LOG_EXTERNAL_CATEGORY(mc_global); namespace simgrid::mc { -RemoteApp::RemoteApp(const std::vector& args) +RemoteApp::RemoteApp(const std::vector& args, bool need_memory_introspection) { - checker_side_ = std::make_unique(args); + for (auto* arg : args) + app_args_.push_back(arg); - initial_snapshot_ = std::make_shared(0, page_store_, checker_side_->get_remote_memory()); + checker_side_ = std::make_unique(app_args_, need_memory_introspection); + + if (need_memory_introspection) + initial_snapshot_ = std::make_shared(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 @@ -168,18 +177,6 @@ void RemoteApp::wait_for_requests() 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 = {}; @@ -188,7 +185,8 @@ Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_ 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 @@ -209,18 +207,7 @@ Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_ 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 diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp index d6e5eee825..0c9c00dc3c 100644 --- a/src/mc/api/RemoteApp.hpp +++ b/src/mc/api/RemoteApp.hpp @@ -30,6 +30,8 @@ private: PageStore page_store_{500}; std::shared_ptr initial_snapshot_; + std::vector app_args_; + // No copy: RemoteApp(RemoteApp const&) = delete; RemoteApp& operator=(RemoteApp const&) = delete; @@ -42,11 +44,11 @@ public: * * The code is expected to `exec` the model-checked application. */ - explicit RemoteApp(const std::vector& args); + explicit RemoteApp(const std::vector& 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. */ @@ -54,8 +56,6 @@ public: /** 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; @@ -67,7 +67,7 @@ public: 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_; } }; diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index d702ff39d9..b35f37e3fc 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -30,7 +30,7 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) system_state_ = std::make_shared(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) @@ -47,7 +47,7 @@ State::State(RemoteApp& remote_app, const State* parent_state) : num_(++expended /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) system_state_ = std::make_shared(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) { @@ -58,7 +58,7 @@ State::State(RemoteApp& remote_app, const State* parent_state) : num_(++expended 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); diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index f0994e8aa5..a0c68f4d21 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -87,7 +87,7 @@ public: void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } std::map 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_)); } diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 792383ecee..187b9bb152 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -43,7 +43,7 @@ void DFSExplorer::check_non_termination(const State* current_state) { 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 ***"); @@ -291,7 +291,7 @@ void DFSExplorer::backtrack() /* 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; } @@ -312,7 +312,10 @@ void DFSExplorer::backtrack() XBT_VERB(">> Backtracked to %s", get_record_trace().to_string().c_str()); } -DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Exploration(args) +// DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Exploration(args, _sg_mc_termination) // +// UNCOMMENT TO ACTIVATE REFORKS +DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) + : Exploration(args, true) // This version does not use reforks as it breaks { if (with_dpor) reduction_mode_ = ReductionMode::dpor; diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 1dbe4c41e3..1f0e24f98f 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -20,7 +20,8 @@ static simgrid::config::Flag cfg_dot_output_file{ Exploration* Exploration::instance_ = nullptr; // singleton instance -Exploration::Exploration(const std::vector& args) : remote_app_(std::make_unique(args)) +Exploration::Exploration(const std::vector& args, bool need_memory_introspection) + : remote_app_(std::make_unique(args, need_memory_introspection)) { xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance"); instance_ = this; @@ -65,7 +66,7 @@ void Exploration::log_state() } } -void Exploration::report_crash(int status) +XBT_ATTRIB_NORETURN void Exploration::report_crash(int status) { XBT_INFO("**************************"); XBT_INFO("** CRASH IN THE PROGRAM **"); @@ -87,13 +88,18 @@ void Exploration::report_crash(int status) 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 ***"); @@ -108,9 +114,8 @@ void Exploration::report_assertion_failure() 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); } diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index c027256ade..aa6d420245 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -34,7 +34,7 @@ class Exploration : public xbt::Extendable { FILE* dot_output_ = nullptr; public: - explicit Exploration(const std::vector& args); + explicit Exploration(const std::vector& args, bool need_memory_introspection); virtual ~Exploration(); static Exploration* get_instance() { return instance_; } @@ -46,12 +46,12 @@ public: 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 diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 72909308dc..3638fd67a3 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -23,11 +23,11 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state, 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(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(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); @@ -75,7 +75,7 @@ std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc 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(); @@ -104,7 +104,7 @@ void LivenessChecker::replay() 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; } } @@ -153,7 +153,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa 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; @@ -180,7 +180,7 @@ void LivenessChecker::purge_visited_pairs() } } -LivenessChecker::LivenessChecker(const std::vector& args) : Exploration(args) {} +LivenessChecker::LivenessChecker(const std::vector& args) : Exploration(args, true) {} LivenessChecker::~LivenessChecker() { xbt_automaton_free(property_automaton_); diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 1506a16cdd..550e5b7c7f 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -5,7 +5,10 @@ #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 #include @@ -13,7 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification namespace simgrid::mc::udpor { -UdporChecker::UdporChecker(const std::vector& args) : Exploration(args) +UdporChecker::UdporChecker(const std::vector& args) : Exploration(args, true) { // Initialize the map } @@ -59,7 +62,9 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std:: // 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(); } @@ -75,7 +80,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std:: "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(); @@ -92,10 +97,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std:: // 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 @@ -104,7 +107,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std:: 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} @@ -157,7 +161,9 @@ EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const 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) { @@ -169,7 +175,6 @@ EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const } } } - return incremental_exC; } @@ -199,8 +204,10 @@ void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e) 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 UdporChecker::record_current_state() @@ -227,15 +234,23 @@ const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& 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() diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 2bcdeb4065..6214039ce6 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -28,7 +28,7 @@ namespace simgrid::mc::udpor { * 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 { @@ -42,33 +42,6 @@ public: inline std::unique_ptr get_current_state() { return std::make_unique(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(); /** @@ -131,7 +104,7 @@ private: * 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 @@ -144,17 +117,13 @@ private: /** * @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 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; - /** * */ diff --git a/src/mc/explo/udpor/Comb.hpp b/src/mc/explo/udpor/Comb.hpp new file mode 100644 index 0000000000..ab0ec7a08e --- /dev/null +++ b/src/mc/explo/udpor/Comb.hpp @@ -0,0 +1,92 @@ +/* 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 +#include +#include +#include + +namespace simgrid::mc::udpor { + +/** + * @brief An individual element of a `Comb`, i.e. a + * sequence of `const UnfoldingEvent*`s + */ +using Spike = std::vector; + +/** + * @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 , + * where each spike is a sequence of elements over A. + * + * Furthermore, a **combination over C** is any tuple + * 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 { +public: + explicit Comb(unsigned k) : std::vector(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> references; + std::transform(begin(), end(), std::back_inserter(references), [](const Spike& spike) { return std::cref(spike); }); + return simgrid::xbt::variable_for_loop(std::move(references)); + } + auto combinations_end() const { return simgrid::xbt::variable_for_loop(); } +}; + +} // namespace simgrid::mc::udpor +#endif diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index 8e2cb8521e..98d004b22d 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -4,7 +4,9 @@ * 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" @@ -19,6 +21,12 @@ Configuration::Configuration(std::initializer_list events { } +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()) { @@ -26,6 +34,8 @@ Configuration::Configuration(const EventSet& events) : events_(events) } } +Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {} + void Configuration::add_event(const UnfoldingEvent* e) { if (e == nullptr) { @@ -53,6 +63,17 @@ void Configuration::add_event(const UnfoldingEvent* e) } } +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 Configuration::get_topologically_sorted_events() const { return this->events_.get_topological_ordering(); @@ -94,4 +115,79 @@ EventSet Configuration::get_minimally_reproducible_events() const return minimally_reproducible_events; } +std::optional 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::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 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 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 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& spikes) { + std::vector 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 diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index a27b9a6a8a..619871eac2 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -9,6 +9,8 @@ #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" +#include + namespace simgrid::mc::udpor { class Configuration { @@ -18,7 +20,9 @@ public: 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 events); auto begin() const { return this->events_.begin(); } @@ -59,6 +63,23 @@ public: */ 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 compute_alternative_to(const EventSet& D, const Unfolding& U) const; + std::optional 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 @@ -108,8 +129,8 @@ public: * 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; diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp index 48eeb4e1fd..8deb62e814 100644 --- a/src/mc/explo/udpor/Configuration_test.cpp +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -7,6 +7,7 @@ #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" @@ -598,4 +599,568 @@ TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Stress Test for Maximal // 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(EventSet(), std::make_shared()); + auto e0_handle = e0.get(); + + auto e1 = std::make_unique(EventSet({e0_handle}), std::make_shared()); + auto e1_handle = e1.get(); + + auto e2 = std::make_unique(EventSet({e1_handle}), std::make_shared()); + auto e2_handle = e2.get(); + + auto e3 = std::make_unique(EventSet({e1_handle}), std::make_shared()); + auto e3_handle = e3.get(); + + auto e4 = std::make_unique(EventSet({e0_handle}), std::make_shared()); + auto e4_handle = e4.get(); + + auto e5 = std::make_unique(EventSet({e4_handle}), std::make_shared()); + auto e5_handle = e5.get(); + + auto e6 = std::make_unique(EventSet({e5_handle}), std::make_shared()); + auto e6_handle = e6.get(); + + auto e7 = std::make_unique(EventSet({e0_handle}), std::make_shared()); + auto e7_handle = e7.get(); + + auto e8 = std::make_unique(EventSet({e4_handle, e7_handle}), std::make_shared()); + auto e8_handle = e8.get(); + + auto e9 = std::make_unique(EventSet({e7_handle}), std::make_shared()); + auto e9_handle = e9.get(); + + auto e10 = std::make_unique(EventSet({e9_handle}), std::make_shared()); + 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 diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp index f0dd8d1c4d..09cb66b061 100644 --- a/src/mc/explo/udpor/EventSet.cpp +++ b/src/mc/explo/udpor/EventSet.cpp @@ -90,6 +90,11 @@ EventSet EventSet::make_union(const Configuration& config) const 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(); @@ -132,6 +137,11 @@ bool EventSet::contains(const History& history) const 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 diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index c6e755be79..54c00c8f47 100644 --- a/src/mc/explo/udpor/EventSet.hpp +++ b/src/mc/explo/udpor/EventSet.hpp @@ -48,11 +48,13 @@ public: 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_; } diff --git a/src/mc/explo/udpor/Unfolding.cpp b/src/mc/explo/udpor/Unfolding.cpp index 84ad822cfe..1b63328bbb 100644 --- a/src/mc/explo/udpor/Unfolding.cpp +++ b/src/mc/explo/udpor/Unfolding.cpp @@ -9,12 +9,20 @@ 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 e) @@ -29,6 +37,7 @@ void Unfolding::insert(std::unique_ptr e) } // Map the handle to its owner + this->event_handles.insert(handle); this->global_events_[handle] = std::move(e); } @@ -36,7 +45,7 @@ bool Unfolding::contains_event_equivalent_to(const UnfoldingEvent* e) const { // 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; } @@ -44,4 +53,15 @@ bool Unfolding::contains_event_equivalent_to(const UnfoldingEvent* e) const 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 diff --git a/src/mc/explo/udpor/Unfolding.hpp b/src/mc/explo/udpor/Unfolding.hpp index 01c76637d4..0107692670 100644 --- a/src/mc/explo/udpor/Unfolding.hpp +++ b/src/mc/explo/udpor/Unfolding.hpp @@ -6,6 +6,7 @@ #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" @@ -26,17 +27,45 @@ private: */ std::unordered_map> 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 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 diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index b62ef1a02a..c51023b474 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -20,22 +20,20 @@ UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptraid_ != 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 diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index c2ab4946fc..aeb4902e98 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -30,8 +30,15 @@ public: 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; diff --git a/src/mc/explo/udpor/UnfoldingEvent_test.cpp b/src/mc/explo/udpor/UnfoldingEvent_test.cpp index a0a18e92c3..a676c69fdb 100644 --- a/src/mc/explo/udpor/UnfoldingEvent_test.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent_test.cpp @@ -7,8 +7,104 @@ #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(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e3(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e4(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + + UnfoldingEvent e5(EventSet({&e1, &e3, &e2}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e6(EventSet({&e1, &e3, &e2}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e7(EventSet({&e1, &e3, &e2}), std::make_shared(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(Transition::Type::UNKNOWN, 1, 0)); + UnfoldingEvent e2_diff_actor(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 1, 0)); + UnfoldingEvent e5_diff_actor(EventSet({&e1, &e3, &e2}), + std::make_shared(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(Transition::Type::ACTOR_JOIN, 0, 0)); + UnfoldingEvent e2_diff_transition(EventSet({&e1}), + std::make_shared(Transition::Type::ACTOR_JOIN, 0, 0)); + UnfoldingEvent e5_diff_transition(EventSet({&e1, &e3, &e2}), + std::make_shared(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(Transition::Type::UNKNOWN, 0, 1)); + UnfoldingEvent e2_diff_considered(EventSet({&e1}), + std::make_shared(Transition::Type::UNKNOWN, 0, 1)); + UnfoldingEvent e5_diff_considered(EventSet({&e1, &e3, &e2}), + std::make_shared(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(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e2_diff_hist(EventSet({&e3}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e5_diff_hist(EventSet({&e1, &e2}), + std::make_shared(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") diff --git a/src/mc/explo/udpor/Unfolding_test.cpp b/src/mc/explo/udpor/Unfolding_test.cpp index 72f8602229..d75fb28763 100644 --- a/src/mc/explo/udpor/Unfolding_test.cpp +++ b/src/mc/explo/udpor/Unfolding_test.cpp @@ -7,6 +7,7 @@ #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") @@ -39,4 +40,25 @@ TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an 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( + EventSet(), std::make_shared(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2)); + auto e2 = std::make_unique( + EventSet(), std::make_shared(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 diff --git a/src/mc/explo/udpor/udpor_tests_private.hpp b/src/mc/explo/udpor/udpor_tests_private.hpp index 6e1a23345b..276edfca79 100644 --- a/src/mc/explo/udpor/udpor_tests_private.hpp +++ b/src/mc/explo/udpor/udpor_tests_private.hpp @@ -12,14 +12,22 @@ #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 { @@ -28,6 +36,12 @@ struct DependentAction : public Transition { }; 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 { diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index b62e0605ff..7e6e4145f2 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -75,11 +75,6 @@ AppSide* AppSide::initialize() 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(); } @@ -152,6 +147,14 @@ void AppSide::handle_finalize(const s_mc_message_int_t* msg) const 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(); @@ -235,7 +238,7 @@ void AppSide::handle_actors_maxpid() const 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"); @@ -268,6 +271,11 @@ void AppSide::handle_messages() const 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(); @@ -285,7 +293,7 @@ void AppSide::handle_messages() const } } -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(), @@ -301,7 +309,7 @@ void AppSide::main_loop() const } } -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(); @@ -309,7 +317,7 @@ void AppSide::report_assertion_failure() const 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 = {}; @@ -321,7 +329,7 @@ void AppSide::ignore_memory(void* addr, std::size_t size) const 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(); @@ -344,7 +352,7 @@ void AppSide::ignore_heap(void* address, std::size_t size) const 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 = {}; @@ -356,8 +364,10 @@ void AppSide::unignore_heap(void* address, std::size_t size) const 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; @@ -376,7 +386,7 @@ void AppSide::declare_symbol(const char* name, int* value) const */ 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(); diff --git a/src/mc/remote/AppSide.hpp b/src/mc/remote/AppSide.hpp index 7389f54141..8d8a3cfbcc 100644 --- a/src/mc/remote/AppSide.hpp +++ b/src/mc/remote/AppSide.hpp @@ -22,24 +22,26 @@ class XBT_PUBLIC AppSide { private: Channel channel_; static std::unique_ptr 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; diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp index bd7b16b367..5958cd33ee 100644 --- a/src/mc/remote/CheckerSide.cpp +++ b/src/mc/remote/CheckerSide.cpp @@ -126,12 +126,14 @@ static void wait_application_process(pid_t pid) 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(arg); if (events == EV_READ) { std::array buffer; @@ -149,10 +151,9 @@ void CheckerSide::setup_events() } }, 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(arg); @@ -166,11 +167,10 @@ void CheckerSide::setup_events() } }, this); - event_add(signal_event, nullptr); - signal_event_.reset(signal_event); + event_add(signal_event_, nullptr); } -CheckerSide::CheckerSide(const std::vector& args) : running_(true) +CheckerSide::CheckerSide(const std::vector& 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) @@ -193,9 +193,56 @@ CheckerSide::CheckerSide(const std::vector& args) : running_(true) 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(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()); @@ -213,52 +260,59 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) 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(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; @@ -267,7 +321,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) 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; } @@ -312,8 +366,7 @@ void CheckerSide::handle_waitpid() 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)); } } diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp index 2461d335c3..17fb33c3c4 100644 --- a/src/mc/remote/CheckerSide.hpp +++ b/src/mc/remote/CheckerSide.hpp @@ -18,12 +18,12 @@ namespace simgrid::mc { /* CheckerSide: All what the checker needs to interact with a given application process */ class CheckerSide { + event* socket_event_; + event* signal_event_; std::unique_ptr base_{nullptr, &event_base_free}; - std::unique_ptr socket_event_{nullptr, &event_free}; - std::unique_ptr signal_event_{nullptr, &event_free}; std::unique_ptr remote_memory_; - Channel channel_; + Channel channel_; bool running_ = false; pid_t pid_; @@ -32,7 +32,8 @@ class CheckerSide { void handle_waitpid(); public: - explicit CheckerSide(const std::vector& args); + explicit CheckerSide(const std::vector& args, bool need_memory_introspection); + ~CheckerSide(); // No copy: CheckerSide(CheckerSide const&) = delete; @@ -48,11 +49,14 @@ public: 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 diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index 4eef95b789..108128449a 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -23,10 +23,11 @@ // ***** 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; @@ -53,11 +54,6 @@ struct s_mc_message_int_t { }; /* 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; @@ -85,6 +81,11 @@ struct s_mc_message_register_symbol_t { }; /* 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_; diff --git a/src/mc/sosp/Region.cpp b/src/mc/sosp/Region.cpp index acbc080110..2dca797e71 100644 --- a/src/mc/sosp/Region.cpp +++ b/src/mc/sosp/Region.cpp @@ -16,7 +16,8 @@ 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"); @@ -28,7 +29,7 @@ Region::Region(PageStore& store, RemoteProcessMemory& memory, RegionType region_ * * @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()); diff --git a/src/mc/sosp/Region.hpp b/src/mc/sosp/Region.hpp index cf7b748577..7ab26e2de9 100644 --- a/src/mc/sosp/Region.hpp +++ b/src/mc/sosp/Region.hpp @@ -35,7 +35,7 @@ private: 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; @@ -58,7 +58,7 @@ public: bool contain(RemotePtr 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 * diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp index fee842d32c..72e2355c48 100644 --- a/src/mc/sosp/Snapshot.cpp +++ b/src/mc/sosp/Snapshot.cpp @@ -200,7 +200,7 @@ void Snapshot::ignore_restore() const } 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); diff --git a/src/mc/sosp/Snapshot_test.cpp b/src/mc/sosp/Snapshot_test.cpp index 237065b7e0..d2f7d0e24c 100644 --- a/src/mc/sosp/Snapshot_test.cpp +++ b/src/mc/sosp/Snapshot_test.cpp @@ -151,8 +151,8 @@ void snap_test_helper::compare_region_parts() } } -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); diff --git a/src/mc/transition/TransitionObjectAccess.cpp b/src/mc/transition/TransitionObjectAccess.cpp index d16472e98a..63a7d92fc3 100644 --- a/src/mc/transition/TransitionObjectAccess.cpp +++ b/src/mc/transition/TransitionObjectAccess.cpp @@ -15,14 +15,14 @@ ObjectAccessTransition::ObjectAccessTransition(aid_t issuer, int times_considere { short s; xbt_assert(stream >> s >> objaddr_ >> objname_ >> file_ >> line_); - type_ = static_cast(s); + access_type_ = static_cast(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("); diff --git a/src/mc/transition/TransitionObjectAccess.hpp b/src/mc/transition/TransitionObjectAccess.hpp index 12314462e5..4ca7ff8250 100644 --- a/src/mc/transition/TransitionObjectAccess.hpp +++ b/src/mc/transition/TransitionObjectAccess.hpp @@ -12,7 +12,7 @@ namespace simgrid::mc { 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_; diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 528ed022ba..1703fe08f2 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -529,7 +529,8 @@ set(MC_SRC 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 diff --git a/tools/jenkins/Flags.sh b/tools/jenkins/Flags.sh index 25fadeb18e..e8f9198f16 100755 --- a/tools/jenkins/Flags.sh +++ b/tools/jenkins/Flags.sh @@ -89,7 +89,7 @@ make -j$NUMPROC tests 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 ..