X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/bdef81fa4e3566ce31b435deb98fea7b8fe70e6e..603a2971cfa9ec8a4fd4493b74c5680956828423:/src/mc/checker/LivenessChecker.cpp diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index fc2ecb1eff..4c5a2ca033 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -1,5 +1,4 @@ -/* Copyright (c) 2011-2015. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2011-2019. 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. */ @@ -16,59 +15,47 @@ #include #include -#include #include #include -#include "src/mc/mc_request.h" -#include "src/mc/checker/LivenessChecker.hpp" -#include "src/mc/mc_private.h" -#include "src/mc/mc_record.h" -#include "src/mc/mc_smx.h" -#include "src/mc/Client.hpp" -#include "src/mc/mc_private.h" -#include "src/mc/mc_replay.h" -#include "src/mc/mc_safety.h" -#include "src/mc/mc_exit.h" -#include "src/mc/Transition.hpp" #include "src/mc/Session.hpp" +#include "src/mc/Transition.hpp" +#include "src/mc/checker/LivenessChecker.hpp" +#include "src/mc/mc_exit.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/mc_record.hpp" +#include "src/mc/mc_replay.hpp" +#include "src/mc/mc_request.hpp" +#include "src/mc/mc_smx.hpp" +#include "src/mc/remote/Client.hpp" -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, - "Logging specific to algorithms for liveness properties verification"); +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); /********* Static functions *********/ namespace simgrid { namespace mc { -VisitedPair::VisitedPair( - int pair_num, xbt_automaton_state_t automaton_state, - std::shared_ptr> atomic_propositions, - std::shared_ptr graph_state) +VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, + std::shared_ptr> atomic_propositions, + std::shared_ptr graph_state) + : num(pair_num), automaton_state(automaton_state) { - simgrid::mc::Process* process = &(mc_model_checker->process()); + simgrid::mc::RemoteClient* process = &(mc_model_checker->process()); this->graph_state = std::move(graph_state); if(this->graph_state->system_state == nullptr) this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); - this->heap_bytes_used = mmalloc_get_bytes_used_remote( - process->get_heap()->heaplimit, - process->get_malloc_info()); + this->heap_bytes_used = mmalloc_get_bytes_used_remote(process->get_heap()->heaplimit, process->get_malloc_info()); this->actors_count = mc_model_checker->process().actors().size(); - this->automaton_state = automaton_state; - this->num = pair_num; this->other_num = -1; this->atomic_propositions = std::move(atomic_propositions); } -VisitedPair::~VisitedPair() -{ -} - -static bool evaluate_label( - xbt_automaton_exp_label_t l, std::vector const& values) +static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector const& values) { switch (l->type) { case xbt_automaton_exp_label::AUT_OR: @@ -78,7 +65,7 @@ static bool evaluate_label( return evaluate_label(l->u.or_and.left_exp, values) && evaluate_label(l->u.or_and.right_exp, values); case xbt_automaton_exp_label::AUT_NOT: - return !evaluate_label(l->u.exp_not, values); + return not evaluate_label(l->u.exp_not, values); case xbt_automaton_exp_label::AUT_PREDICAT:{ unsigned int cursor = 0; xbt_automaton_propositional_symbol_t p = nullptr; @@ -87,6 +74,7 @@ static bool evaluate_label( return values[cursor] != 0; } xbt_die("Missing predicate"); + break; } case xbt_automaton_exp_label::AUT_ONE: return true; @@ -98,8 +86,6 @@ static bool evaluate_label( Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} -Pair::~Pair() {} - std::shared_ptr> LivenessChecker::getPropositionValues() { std::vector values; @@ -135,13 +121,11 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || this->compare(pair_test.get(), new_pair.get()) != 0) continue; - XBT_INFO("Pair %d already reached (equal to pair %d) !", - new_pair->num, pair_test->num); + XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); explorationStack_.pop_back(); if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - this->previousPair_, pair_test->num, - this->previousRequest_.c_str()); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, pair_test->num, + this->previousRequest_.c_str()); return nullptr; } @@ -158,22 +142,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num) } } -void LivenessChecker::prepare(void) -{ - this->previousPair_ = 0; - - std::shared_ptr> propos = this->getPropositionValues(); - - // For each initial state of the property automaton, push a - // (application_state, automaton_state) pair to the exploration stack: - unsigned int cursor = 0; - xbt_automaton_state_t automaton_state; - xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state) - if (automaton_state->type == -1) - explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); -} - - void LivenessChecker::replay() { XBT_DEBUG("**** Begin Replay ****"); @@ -234,17 +202,16 @@ void LivenessChecker::replay() } /** - * \brief Checks whether a given pair has already been visited by the algorithm. + * @brief Checks whether a given pair has already been visited by the algorithm. */ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair) { - if (_sg_mc_visited == 0) + if (_sg_mc_max_visited_states == 0) return -1; if (visited_pair == nullptr) - visited_pair = std::make_shared( - pair->num, pair->automaton_state, pair->atomic_propositions, - pair->graph_state); + visited_pair = + std::make_shared(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(), simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap()); @@ -276,7 +243,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair void LivenessChecker::purgeVisitedPairs() { - if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) { + if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) { // Remove the oldest entry with a linear search: visitedPairs_.erase(boost::min_element(visitedPairs_, [](std::shared_ptr const a, std::shared_ptr const& b) { @@ -284,11 +251,7 @@ void LivenessChecker::purgeVisitedPairs() } } -LivenessChecker::LivenessChecker(Session& session) : Checker(session) -{ -} - -LivenessChecker::~LivenessChecker() +LivenessChecker::LivenessChecker(Session& s) : Checker(s) { } @@ -302,7 +265,6 @@ RecordTrace LivenessChecker::getRecordTrace() // override void LivenessChecker::logState() // override { - Checker::logState(); XBT_INFO("Expanded pairs = %lu", expandedPairsCount_); XBT_INFO("Visited pairs = %lu", visitedPairsCount_); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); @@ -313,12 +275,12 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth) XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); + XBT_INFO("Counter-example that violates formula:"); + for (auto const& s : this->getTextualTrace()) + XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); - for (auto& s : this->getTextualTrace()) - XBT_INFO("%s", s.c_str()); simgrid::mc::session->logState(); - XBT_INFO("Counter-example depth : %zd", depth); + XBT_INFO("Counter-example depth: %zu", depth); } std::vector LivenessChecker::getTextualTrace() // override @@ -334,19 +296,85 @@ std::vector LivenessChecker::getTextualTrace() // override return trace; } -int LivenessChecker::main(void) +std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, + std::shared_ptr> propositions) +{ + expandedPairsCount_++; + std::shared_ptr next_pair = std::make_shared(expandedPairsCount_); + next_pair->automaton_state = state; + next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expandedStatesCount_)); + next_pair->atomic_propositions = std::move(propositions); + if (current_pair) + next_pair->depth = current_pair->depth + 1; + else + next_pair->depth = 1; + /* Get enabled actors and insert them in the interleave set of the next graph_state */ + for (auto& actor : mc_model_checker->process().actors()) + if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) + next_pair->graph_state->addInterleavingSet(actor.copy.getBuffer()); + next_pair->requests = next_pair->graph_state->interleaveSize(); + /* FIXME : get search_cycle value for each accepting state */ + if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle)) + next_pair->search_cycle = true; + else + next_pair->search_cycle = false; + return next_pair; +} + +void LivenessChecker::backtrack() { - while (!explorationStack_.empty()){ + /* Traverse the stack backwards until a pair with a non empty interleave + set is found, deleting all the pairs that have it empty in the way. */ + while (not explorationStack_.empty()) { + std::shared_ptr current_pair = explorationStack_.back(); + explorationStack_.pop_back(); + if (current_pair->requests > 0) { + /* We found a backtracking point */ + XBT_DEBUG("Backtracking to depth %d", current_pair->depth); + explorationStack_.push_back(std::move(current_pair)); + this->replay(); + XBT_DEBUG("Backtracking done"); + break; + } else { + XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); + if (current_pair->automaton_state->type == 1) + this->removeAcceptancePair(current_pair->num); + } + } +} + +void LivenessChecker::run() +{ + XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str()); + MC_automaton_load(_sg_mc_property_file.get().c_str()); + + XBT_DEBUG("Starting the liveness algorithm"); + simgrid::mc::session->initialize(); + + /* Initialize */ + this->previousPair_ = 0; + + std::shared_ptr> propos = this->getPropositionValues(); + + // For each initial state of the property automaton, push a + // (application_state, automaton_state) pair to the exploration stack: + unsigned int cursor = 0; + xbt_automaton_state_t automaton_state; + xbt_dynar_foreach (simgrid::mc::property_automaton->states, cursor, automaton_state) + if (automaton_state->type == -1) + explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); + + /* Actually run the double DFS search for counter-examples */ + while (not explorationStack_.empty()) { std::shared_ptr current_pair = explorationStack_.back(); /* Update current state in buchi automaton */ simgrid::mc::property_automaton->current_state = current_pair->automaton_state; - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %zd, pair_num = %d, requests = %d)", - current_pair->depth, current_pair->search_cycle, - current_pair->graph_state->interleaveSize(), - current_pair->num, - current_pair->requests); + XBT_DEBUG( + "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)", + current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleaveSize(), current_pair->num, + current_pair->requests); if (current_pair->requests == 0) { this->backtrack(); @@ -354,27 +382,28 @@ int LivenessChecker::main(void) } std::shared_ptr reached_pair; - if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started - && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) { - this->showAcceptanceCycle(current_pair->depth); - return SIMGRID_MC_EXIT_LIVENESS; + if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) { + reached_pair = this->insertAcceptancePair(current_pair.get()); + if (reached_pair == nullptr) { + this->showAcceptanceCycle(current_pair->depth); + throw simgrid::mc::LivenessError(); + } } /* Pair already visited ? stop the exploration on the current path */ - int visited_num = -1; - if ((!current_pair->exploration_started) - && (visited_num = this->insertVisitedPair( - reached_pair, current_pair.get())) != -1) { - if (dot_output != nullptr){ - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - this->previousPair_, visited_num, - this->previousRequest_.c_str()); - fflush(dot_output); + if (not current_pair->exploration_started) { + int visited_num = this->insertVisitedPair(reached_pair, current_pair.get()); + if (visited_num != -1) { + if (dot_output != nullptr) { + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, visited_num, + this->previousRequest_.c_str()); + fflush(dot_output); + } + XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); + current_pair->requests = 0; + this->backtrack(); + continue; } - XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); - current_pair->requests = 0; - this->backtrack(); - continue; } smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get()); @@ -400,7 +429,7 @@ int LivenessChecker::main(void) /* Update stats */ mc_model_checker->executed_transitions++; - if (!current_pair->exploration_started) + if (not current_pair->exploration_started) visitedPairsCount_++; /* Answer the request */ @@ -417,85 +446,23 @@ int LivenessChecker::main(void) // For each enabled transition in the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: - int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; - while (cursor >= 0) { - xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t); + for (int i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) { + xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as( + current_pair->automaton_state->out, i, xbt_automaton_transition_t); if (evaluate_label(transition_succ->label, *prop_values)) explorationStack_.push_back(this->newPair( current_pair.get(), transition_succ->dst, prop_values)); - cursor--; } } XBT_INFO("No property violation found."); simgrid::mc::session->logState(); - return SIMGRID_MC_EXIT_SUCCESS; -} - -std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr> propositions) -{ - std::shared_ptr next_pair = std::make_shared(++expandedPairsCount_); - next_pair->automaton_state = state; - next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expandedStatesCount_)); - next_pair->atomic_propositions = std::move(propositions); - if (current_pair) - next_pair->depth = current_pair->depth + 1; - else - next_pair->depth = 1; - /* Get enabled actors and insert them in the interleave set of the next graph_state */ - for (auto& actor : mc_model_checker->process().actors()) - if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) - next_pair->graph_state->interleave(actor.copy.getBuffer()); - next_pair->requests = next_pair->graph_state->interleaveSize(); - /* FIXME : get search_cycle value for each accepting state */ - if (next_pair->automaton_state->type == 1 || - (current_pair && current_pair->search_cycle)) - next_pair->search_cycle = true; - else - next_pair->search_cycle = false; - return next_pair; -} - -void LivenessChecker::backtrack() -{ - /* Traverse the stack backwards until a pair with a non empty interleave - set is found, deleting all the pairs that have it empty in the way. */ - while (!explorationStack_.empty()) { - std::shared_ptr current_pair = explorationStack_.back(); - explorationStack_.pop_back(); - if (current_pair->requests > 0) { - /* We found a backtracking point */ - XBT_DEBUG("Backtracking to depth %d", current_pair->depth); - explorationStack_.push_back(std::move(current_pair)); - this->replay(); - XBT_DEBUG("Backtracking done"); - break; - } else { - XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); - if (current_pair->automaton_state->type == 1) - this->removeAcceptancePair(current_pair->num); - } - } -} - -int LivenessChecker::run() -{ - XBT_INFO("Check the liveness property %s", _sg_mc_property_file); - MC_automaton_load(_sg_mc_property_file); - - XBT_DEBUG("Starting the liveness algorithm"); - simgrid::mc::session->initialize(); - this->prepare(); - - int res = this->main(); - - return res; } -Checker* createLivenessChecker(Session& session) +Checker* createLivenessChecker(Session& s) { - return new LivenessChecker(session); + return new LivenessChecker(s); } }