X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/96d605fde63f72480bf570f7bc7609e2954cb2d7..239cd16f4e95031d3a106e487c1485726069f1d7:/src/mc/explo/LivenessChecker.cpp diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 3acd33a319..370a146d0b 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2011-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2011-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. */ @@ -19,19 +19,21 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms namespace simgrid::mc { VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state, - std::shared_ptr> atomic_propositions, std::shared_ptr app_state) + std::shared_ptr> atomic_propositions, std::shared_ptr app_state, + RemoteApp& remote_app) : num(pair_num), prop_state_(prop_state) { + auto& memory = mc_model_checker->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)); - this->heap_bytes_used = Api::get().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); } -static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector const& values) +bool LivenessChecker::evaluate_label(const xbt_automaton_exp_label* l, std::vector const& values) { switch (l->type) { case xbt_automaton_exp_label::AUT_OR: @@ -41,7 +43,7 @@ static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector co case xbt_automaton_exp_label::AUT_NOT: return not evaluate_label(l->u.exp_not, values); case xbt_automaton_exp_label::AUT_PREDICAT: - return values.at(Api::get().compare_automaton_exp_label(l)) != 0; + return values.at(compare_automaton_exp_label(l)) != 0; case xbt_automaton_exp_label::AUT_ONE: return true; default: @@ -53,30 +55,30 @@ Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} std::shared_ptr> LivenessChecker::get_proposition_values() const { - auto values = Api::get().automaton_propositional_symbol_evaluate(); + auto values = automaton_propositional_symbol_evaluate(); return std::make_shared>(std::move(values)); } std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair) { - auto new_pair = - std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_); + auto new_pair = std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, + pair->app_state_, get_remote_app()); - auto [res_begin, res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), Api::get().compare_pair()); + auto [res_begin, + res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), [](auto const& a, auto const& b) { + return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used); + }); if (pair->search_cycle) for (auto i = res_begin; i != res_end; ++i) { std::shared_ptr const& pair_test = *i; if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || - not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(), - new_pair->app_state_->get_system_state())) + (*pair_test->app_state_->get_system_state() != *new_pair->app_state_->get_system_state())) continue; XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); exploration_stack_.pop_back(); - if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, - this->previous_request_.c_str()); + dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, this->previous_request_.c_str()); return nullptr; } @@ -101,7 +103,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()) { - Api::get().restore_state(system_state); + system_state->restore(get_remote_app().get_remote_process_memory()); return; } } @@ -137,28 +139,26 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa return -1; if (visited_pair == nullptr) - visited_pair = - std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_); + visited_pair = std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, + pair->app_state_, get_remote_app()); - auto [range_begin, range_end] = - boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair()); + auto [range_begin, + range_end] = boost::range::equal_range(visited_pairs_, visited_pair.get(), [](auto const& a, auto const& b) { + return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used); + }); for (auto i = range_begin; i != range_end; ++i) { const VisitedPair* pair_test = i->get(); if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) || - not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(), - visited_pair->app_state_->get_system_state())) + (*pair_test->app_state_->get_system_state() != *visited_pair->app_state_->get_system_state())) continue; if (pair_test->other_num == -1) visited_pair->other_num = pair_test->num; else visited_pair->other_num = pair_test->other_num; - if (dot_output == nullptr) - XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", visited_pair->num, pair_test->num); - else - XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", visited_pair->num, - pair_test->num, visited_pair->other_num); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", visited_pair->num, pair_test->num, + visited_pair->other_num); (*i) = std::move(visited_pair); return (*i)->other_num; } @@ -178,7 +178,79 @@ void LivenessChecker::purge_visited_pairs() } } -LivenessChecker::LivenessChecker(RemoteApp* remote_app) : Exploration(remote_app) {} +LivenessChecker::LivenessChecker(const std::vector& args) : Exploration(args) {} +LivenessChecker::~LivenessChecker() +{ + xbt_automaton_free(property_automaton_); +} + +xbt_automaton_t LivenessChecker::property_automaton_ = nullptr; + +void LivenessChecker::automaton_load(const char* file) const +{ + if (property_automaton_ == nullptr) + property_automaton_ = xbt_automaton_new(); + + xbt_automaton_load(property_automaton_, file); +} + +std::vector LivenessChecker::automaton_propositional_symbol_evaluate() const +{ + unsigned int cursor = 0; + std::vector values; + xbt_automaton_propositional_symbol_t ps = nullptr; + xbt_dynar_foreach (property_automaton_->propositional_symbols, cursor, ps) + values.push_back(xbt_automaton_propositional_symbol_evaluate(ps)); + return values; +} + +std::vector LivenessChecker::get_automaton_state() const +{ + std::vector automaton_stack; + unsigned int cursor = 0; + xbt_automaton_state_t automaton_state; + xbt_dynar_foreach (property_automaton_->states, cursor, automaton_state) + if (automaton_state->type == -1) + automaton_stack.push_back(automaton_state); + return automaton_stack; +} + +int LivenessChecker::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const +{ + unsigned int cursor = 0; + xbt_automaton_propositional_symbol_t p = nullptr; + xbt_dynar_foreach (property_automaton_->propositional_symbols, cursor, p) { + if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0) + return cursor; + } + return -1; +} + +void LivenessChecker::set_property_automaton(xbt_automaton_state_t const& automaton_state) const +{ + property_automaton_->current_state = automaton_state; +} + +xbt_automaton_exp_label_t LivenessChecker::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const +{ + const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t); + return transition->label; +} + +xbt_automaton_state_t LivenessChecker::get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const +{ + const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t); + return transition->dst; +} +void LivenessChecker::automaton_register_symbol(RemoteProcessMemory const& remote_process, const char* name, + RemotePtr address) +{ + if (property_automaton_ == nullptr) + property_automaton_ = xbt_automaton_new(); + + xbt::add_proposition(property_automaton_, name, + [&remote_process, address]() { return remote_process.read(address); }); +} RecordTrace LivenessChecker::get_record_trace() // override { @@ -193,6 +265,7 @@ void LivenessChecker::log_state() // override XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_); XBT_INFO("Visited pairs = %lu", visited_pairs_count_); XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions()); + Exploration::log_state(); } void LivenessChecker::show_acceptance_cycle(std::size_t depth) @@ -203,7 +276,9 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth) XBT_INFO("Counter-example that violates formula:"); for (auto const& s : this->get_textual_trace()) XBT_INFO(" %s", s.c_str()); - XBT_INFO("Path = %s", get_record_trace().to_string().c_str()); + XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " + "--cfg=model-check/replay:'%s'", + get_record_trace().to_string().c_str()); log_state(); XBT_INFO("Counter-example depth: %zu", depth); } @@ -268,10 +343,9 @@ void LivenessChecker::backtrack() void LivenessChecker::run() { XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str()); - Api::get().automaton_load(_sg_mc_property_file.get().c_str()); + automaton_load(_sg_mc_property_file.get().c_str()); XBT_DEBUG("Starting the liveness algorithm"); - get_remote_app().take_initial_snapshot(); /* Initialize */ this->previous_pair_ = 0; @@ -280,7 +354,7 @@ void LivenessChecker::run() // For each initial state of the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: - auto automaton_stack = Api::get().get_automaton_state(); + auto automaton_stack = get_automaton_state(); for (auto* automaton_state : automaton_stack) { if (automaton_state->type == -1) exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos)); @@ -291,7 +365,7 @@ void LivenessChecker::run() std::shared_ptr current_pair = exploration_stack_.back(); /* Update current state in buchi automaton */ - Api::get().set_property_automaton(current_pair->prop_state_); + set_property_automaton(current_pair->prop_state_); XBT_DEBUG( "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)", @@ -316,11 +390,8 @@ void LivenessChecker::run() if (not current_pair->exploration_started) { int visited_num = this->insert_visited_pair(reached_pair, current_pair.get()); if (visited_num != -1) { - if (dot_output != nullptr) { - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num, - this->previous_request_.c_str()); - fflush(dot_output); - } + dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num, this->previous_request_.c_str()); + XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); current_pair->requests = 0; this->backtrack(); @@ -328,21 +399,18 @@ void LivenessChecker::run() } } - current_pair->app_state_->execute_next(current_pair->app_state_->next_transition()); + current_pair->app_state_->execute_next(current_pair->app_state_->next_transition(), get_remote_app()); XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str()); - if (dot_output != nullptr) { - if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num, - this->previous_request_.c_str()); - this->previous_request_.clear(); - } - this->previous_pair_ = current_pair->num; - this->previous_request_ = current_pair->app_state_->get_transition()->dot_string(); - if (current_pair->search_cycle) - fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); - fflush(dot_output); + /* Update the dot output */ + if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { + dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num, this->previous_request_.c_str()); + this->previous_request_.clear(); } + this->previous_pair_ = current_pair->num; + this->previous_request_ = current_pair->app_state_->get_transition()->dot_string(); + if (current_pair->search_cycle) + dot_output("%d [shape=doublecircle];\n", current_pair->num); if (not current_pair->exploration_started) visited_pairs_count_++; @@ -356,8 +424,8 @@ void LivenessChecker::run() // For each enabled transition in the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: for (int i = xbt_dynar_length(current_pair->prop_state_->out) - 1; i >= 0; i--) { - const auto* transition_succ_label = Api::get().get_automaton_transition_label(current_pair->prop_state_->out, i); - auto* transition_succ_dst = Api::get().get_automaton_transition_dst(current_pair->prop_state_->out, i); + const auto* transition_succ_label = get_automaton_transition_label(current_pair->prop_state_->out, i); + auto* transition_succ_dst = get_automaton_transition_dst(current_pair->prop_state_->out, i); if (evaluate_label(transition_succ_label, *prop_values)) exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ_dst, prop_values)); } @@ -367,9 +435,9 @@ void LivenessChecker::run() log_state(); } -Exploration* create_liveness_checker(RemoteApp* remote_app) +Exploration* create_liveness_checker(const std::vector& args) { - return new LivenessChecker(remote_app); + return new LivenessChecker(args); } } // namespace simgrid::mc