X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2ec9b2255f0b467409a521da2efcc79f43812b2e..9692d43fa911bdc2d6d0263a3cb3e22d5e3167fe:/src/mc/LivenessChecker.cpp diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 80cffd37e5..19e634779c 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -6,10 +6,11 @@ #include -#include #include #include +#include + #include #include @@ -29,6 +30,8 @@ #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" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); @@ -92,7 +95,7 @@ static bool evaluate_label( } } -Pair::Pair() : num(++mc_stats->expanded_pairs) +Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} Pair::~Pair() {} @@ -122,7 +125,7 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); - auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(), + auto res = boost::range::equal_range(acceptancePairs_, new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap()); if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) { @@ -137,8 +140,8 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: explorationStack_.pop_back(); if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - initial_global_state->prev_pair, pair_test->num, - initial_global_state->prev_req.c_str()); + this->previousPair_, pair_test->num, + this->previousRequest_.c_str()); return nullptr; } @@ -157,9 +160,7 @@ void LivenessChecker::removeAcceptancePair(int pair_num) void LivenessChecker::prepare(void) { - mc_model_checker->wait_for_requests(); - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); - initial_global_state->prev_pair = 0; + this->previousPair_ = 0; std::shared_ptr> propos = this->getPropositionValues(); @@ -187,7 +188,7 @@ void LivenessChecker::replay() } /* Restore the initial state */ - simgrid::mc::restore_snapshot(initial_global_state->snapshot); + simgrid::mc::session->restoreInitialState(); /* Traverse the stack from the initial state and re-execute the transitions */ int depth = 1; @@ -199,7 +200,7 @@ void LivenessChecker::replay() if (pair->exploration_started) { - int value = state->req_num; + int req_num = state->transition.argument; smx_simcall_t saved_req = &state->executed_req; smx_simcall_t req = nullptr; @@ -207,24 +208,23 @@ void LivenessChecker::replay() if (saved_req != nullptr) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ - const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req); req = &issuer->simcall; /* Debug information */ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::simix).c_str(), + req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get()); } - simgrid::mc::handle_simcall(req, value); - mc_model_checker->wait_for_requests(); + this->getSession().execute(state->transition); } /* Update statistics */ - mc_stats->visited_pairs++; - mc_stats->executed_transitions++; + visitedPairsCount_++; + mc_model_checker->executed_transitions++; depth++; @@ -246,7 +246,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); - auto range = std::equal_range(visitedPairs_.begin(), visitedPairs_.end(), + auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap()); for (auto i = range.first; i != range.second; ++i) { @@ -278,8 +278,7 @@ void LivenessChecker::purgeVisitedPairs() { if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) { // Remove the oldest entry with a linear search: - visitedPairs_.erase(std::min_element( - visitedPairs_.begin(), visitedPairs_.end(), + visitedPairs_.erase(boost::min_element(visitedPairs_, [](std::shared_ptr const a, std::shared_ptr const& b) { return a->num < b->num; } )); } @@ -297,10 +296,18 @@ RecordTrace LivenessChecker::getRecordTrace() // override { RecordTrace res; for (std::shared_ptr const& pair : explorationStack_) - res.push_back(pair->graph_state->getRecordElement()); + res.push_back(pair->graph_state->getTransition()); return res; } +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); +} + void LivenessChecker::showAcceptanceCycle(std::size_t depth) { XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -310,7 +317,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth) simgrid::mc::dumpRecordPath(); for (auto& s : this->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); XBT_INFO("Counter-example depth : %zd", depth); } @@ -318,11 +325,11 @@ std::vector LivenessChecker::getTextualTrace() // override { std::vector trace; for (std::shared_ptr const& pair : explorationStack_) { - int value = pair->graph_state->req_num; + int req_num = pair->graph_state->transition.argument; smx_simcall_t req = &pair->graph_state->executed_req; if (req && req->call != SIMCALL_NONE) trace.push_back(simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::executed)); + req, req_num, simgrid::mc::RequestType::executed)); } return trace; } @@ -360,8 +367,8 @@ int LivenessChecker::main(void) reached_pair, current_pair.get())) != -1) { if (dot_output != nullptr){ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - initial_global_state->prev_pair, visited_num, - initial_global_state->prev_req.c_str()); + 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); @@ -370,18 +377,18 @@ int LivenessChecker::main(void) continue; } - int value; - smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value); + smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get()); + int req_num = current_pair->graph_state->transition.argument; if (dot_output != nullptr) { - if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) { + if (this->previousPair_ != 0 && this->previousPair_ != current_pair->num) { fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - initial_global_state->prev_pair, current_pair->num, - initial_global_state->prev_req.c_str()); - initial_global_state->prev_req.clear(); + this->previousPair_, current_pair->num, + this->previousRequest_.c_str()); + this->previousRequest_.clear(); } - initial_global_state->prev_pair = current_pair->num; - initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value); + this->previousPair_ = current_pair->num; + this->previousRequest_ = simgrid::mc::request_get_dot_output(req, req_num); if (current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); fflush(dot_output); @@ -389,15 +396,15 @@ int LivenessChecker::main(void) XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::simix).c_str()); + req, req_num, simgrid::mc::RequestType::simix).c_str()); - /* Update mc_stats */ - mc_stats->executed_transitions++; + /* Update stats */ + mc_model_checker->executed_transitions++; if (!current_pair->exploration_started) - mc_stats->visited_pairs++; + visitedPairsCount_++; /* Answer the request */ - simgrid::mc::handle_simcall(req, value); + mc_model_checker->handle_simcall(current_pair->graph_state->transition); /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); @@ -422,15 +429,15 @@ int LivenessChecker::main(void) } XBT_INFO("No property violation found."); - MC_print_statistics(mc_stats); + 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(); + std::shared_ptr next_pair = std::make_shared(++expandedPairsCount_); next_pair->automaton_state = state; - next_pair->graph_state = std::shared_ptr(MC_state_new()); + next_pair->graph_state = std::shared_ptr(MC_state_new(++expandedStatesCount_)); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; @@ -438,8 +445,8 @@ std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton next_pair->depth = 1; /* Get enabled processes and insert them in the interleave set of the next graph_state */ for (auto& p : mc_model_checker->process().simix_processes()) - if (simgrid::mc::process_is_enabled(&p.copy)) - next_pair->graph_state->interleave(&p.copy); + if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) + next_pair->graph_state->interleave(p.copy.getBuffer()); next_pair->requests = next_pair->graph_state->interleaveSize(); /* FIXME : get search_cycle value for each acceptant state */ if (next_pair->automaton_state->type == 1 || @@ -447,7 +454,7 @@ std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton next_pair->search_cycle = true; else next_pair->search_cycle = false; - return std::move(next_pair); + return next_pair; } void LivenessChecker::backtrack() @@ -476,16 +483,12 @@ int LivenessChecker::run() { XBT_INFO("Check the liveness property %s", _sg_mc_property_file); MC_automaton_load(_sg_mc_property_file); - mc_model_checker->wait_for_requests(); XBT_DEBUG("Starting the liveness algorithm"); - - /* Create the initial state */ - simgrid::mc::initial_global_state = std::unique_ptr(new s_mc_global_t()); - + simgrid::mc::session->initialize(); this->prepare(); + int res = this->main(); - simgrid::mc::initial_global_state = nullptr; return res; }