From: Gabriel Corona Date: Thu, 24 Mar 2016 08:30:24 +0000 (+0100) Subject: [mc] Move main liveness code in a LivenessChecker class X-Git-Tag: v3_13~311^2~1 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a497c1d62e1064de5a4d765dc43cb9e71243ba95?hp=1a5ae581508abf014bc4dcbc65f2d5e5af9da573 [mc] Move main liveness code in a LivenessChecker class --- diff --git a/src/mc/mc_liveness.cpp b/src/mc/LivenessChecker.cpp similarity index 89% rename from src/mc/mc_liveness.cpp rename to src/mc/LivenessChecker.cpp index cc9897d0cb..71e44eb079 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/LivenessChecker.cpp @@ -20,7 +20,7 @@ #include #include "src/mc/mc_request.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_private.h" #include "src/mc/mc_record.h" #include "src/mc/mc_smx.h" @@ -42,6 +42,41 @@ xbt_dynar_t acceptance_pairs; namespace simgrid { namespace mc { +static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, + xbt_dynar_t atomic_propositions_values) +{ + + switch (l->type) { + case 0:{ + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); + return (left_res || right_res); + } + case 1:{ + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); + return (left_res && right_res); + } + case 2:{ + int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values); + return (!res); + } + case 3:{ + unsigned int cursor = 0; + xbt_automaton_propositional_symbol_t p = nullptr; + xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) { + if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0) + return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int); + } + return -1; + } + case 4: + return 2; + default: + return -1; + } +} + static xbt_dynar_t visited_pairs; Pair::Pair() : num(++mc_stats->expanded_pairs), @@ -53,7 +88,7 @@ Pair::~Pair() { MC_state_delete(this->graph_state, 1); } -static void show_stack_liveness(xbt_fifo_t stack) +void LivenessChecker::showStack(xbt_fifo_t stack) { int value; simgrid::mc::Pair* pair; @@ -73,14 +108,14 @@ static void show_stack_liveness(xbt_fifo_t stack) } } -static void dump_stack_liveness(xbt_fifo_t stack) +void LivenessChecker::dumpStack(xbt_fifo_t stack) { simgrid::mc::Pair* pair; while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr) delete pair; } -static simgrid::xbt::unique_ptr get_atomic_propositions_values() +simgrid::xbt::unique_ptr LivenessChecker::getPropositionValues() { unsigned int cursor = 0; xbt_automaton_propositional_symbol_t ps = nullptr; @@ -92,16 +127,16 @@ static simgrid::xbt::unique_ptr get_atomic_propositions_values() return std::move(values); } -static int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2) +int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2) { simgrid::mc::Snapshot* s1 = state1->graph_state->system_state; simgrid::mc::Snapshot* s2 = state2->graph_state->system_state; int num1 = state1->num; int num2 = state2->num; - return snapshot_compare(num1, s1, num2, s2); + return simgrid::mc::snapshot_compare(num1, s1, num2, s2); } -static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair) +simgrid::mc::VisitedPair* LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair) { auto acceptance_pairs = simgrid::xbt::range(::acceptance_pairs); auto new_pair = @@ -120,7 +155,7 @@ static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* p if (xbt_automaton_propositional_symbols_compare_value( pair_test->atomic_propositions.get(), new_pair->atomic_propositions.get()) == 0) { - if (snapshot_compare(pair_test, new_pair.get()) == 0) { + if (this->compare(pair_test, new_pair.get()) == 0) { XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); xbt_fifo_shift(mc_stack); if (dot_output != nullptr) @@ -137,7 +172,7 @@ static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* p return new_raw_pair; } -static void remove_acceptance_pair(int pair_num) +void LivenessChecker::removeAcceptancePair(int pair_num) { unsigned int cursor = 0; simgrid::mc::VisitedPair* pair_test = nullptr; @@ -160,43 +195,7 @@ static void remove_acceptance_pair(int pair_num) } } - -static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, - xbt_dynar_t atomic_propositions_values) -{ - - switch (l->type) { - case 0:{ - int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); - int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); - return (left_res || right_res); - } - case 1:{ - int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); - int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); - return (left_res && right_res); - } - case 2:{ - int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values); - return (!res); - } - case 3:{ - unsigned int cursor = 0; - xbt_automaton_propositional_symbol_t p = nullptr; - xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) { - if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0) - return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int); - } - return -1; - } - case 4: - return 2; - default: - return -1; - } -} - -static void MC_pre_modelcheck_liveness(void) +void LivenessChecker::prepare(void) { simgrid::mc::Pair* initial_pair = nullptr; mc_model_checker->wait_for_requests(); @@ -209,14 +208,14 @@ static void MC_pre_modelcheck_liveness(void) 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) { /* Initial automaton state */ initial_pair = new Pair(); initial_pair->automaton_state = automaton_state; initial_pair->graph_state = MC_state_new(); - initial_pair->atomic_propositions = get_atomic_propositions_values(); + initial_pair->atomic_propositions = this->getPropositionValues(); initial_pair->depth = 1; /* Get enabled processes and insert them in the interleave set of the graph_state */ @@ -232,7 +231,8 @@ static void MC_pre_modelcheck_liveness(void) } } -static void MC_replay_liveness(xbt_fifo_t stack) + +void LivenessChecker::replay(xbt_fifo_t stack) { xbt_fifo_item_t item; simgrid::mc::Pair* pair = nullptr; @@ -302,8 +302,7 @@ static void MC_replay_liveness(xbt_fifo_t stack) /** * \brief Checks whether a given pair has already been visited by the algorithm. */ -static -int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) +int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) { if (_sg_mc_visited == 0) return -1; @@ -328,7 +327,7 @@ int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* p if (xbt_automaton_propositional_symbols_compare_value( pair_test->atomic_propositions.get(), new_visited_pair->atomic_propositions.get()) == 0) { - if (snapshot_compare(pair_test, new_visited_pair) == 0) { + if (this->compare(pair_test, new_visited_pair) == 0) { if (pair_test->other_num == -1) new_visited_pair->other_num = pair_test->num; else @@ -372,7 +371,28 @@ int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* p return -1; } -static int MC_modelcheck_liveness_main(void) +LivenessChecker::LivenessChecker(Session& session) : Checker(session) +{ +} + +LivenessChecker::~LivenessChecker() +{ +} + +void LivenessChecker::showAcceptanceCycle(std::size_t depth) +{ + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_record_dump_path(mc_stack); + this->showStack(mc_stack); + this->dumpStack(mc_stack); + MC_print_statistics(mc_stats); + XBT_INFO("Counter-example depth : %zd", depth); +} + +int LivenessChecker::main(void) { simgrid::mc::Pair* current_pair = nullptr; int value, res, visited_num = -1; @@ -382,7 +402,7 @@ static int MC_modelcheck_liveness_main(void) simgrid::mc::Pair* next_pair = nullptr; simgrid::xbt::unique_ptr prop_values; simgrid::mc::VisitedPair* reached_pair = nullptr; - + while(xbt_fifo_size(mc_stack) > 0){ /* Get current pair */ @@ -400,24 +420,15 @@ static int MC_modelcheck_liveness_main(void) if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) { /* If new acceptance pair, return new pair */ - if ((reached_pair = is_reached_acceptance_pair(current_pair)) == nullptr) { - int counter_example_depth = current_pair->depth; - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_record_dump_path(mc_stack); - simgrid::mc::show_stack_liveness(mc_stack); - simgrid::mc::dump_stack_liveness(mc_stack); - MC_print_statistics(mc_stats); - XBT_INFO("Counter-example depth : %d", counter_example_depth); + if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) { + this->showAcceptanceCycle(current_pair->depth); return SIMGRID_MC_EXIT_LIVENESS; } } /* Pair already visited ? stop the exploration on the current path */ if ((current_pair->exploration_started == 0) - && (visited_num = simgrid::mc::is_visited_pair( + && (visited_num = this->insertVisitedPair( reached_pair, current_pair)) != -1) { if (dot_output != nullptr){ @@ -428,7 +439,7 @@ static int MC_modelcheck_liveness_main(void) XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); current_pair->requests = 0; goto backtracking; - + }else{ req = MC_state_get_request(current_pair->graph_state, &value); @@ -459,15 +470,15 @@ static int MC_modelcheck_liveness_main(void) /* Answer the request */ simgrid::mc::handle_simcall(req, value); - + /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); current_pair->requests--; current_pair->exploration_started = 1; - /* Get values of atomic propositions (variables used in the property formula) */ - prop_values = get_atomic_propositions_values(); + /* Get values of atomic propositions (variables used in the property formula) */ + prop_values = this->getPropositionValues(); /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */ cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; @@ -478,7 +489,7 @@ static int MC_modelcheck_liveness_main(void) next_pair = new Pair(); next_pair->graph_state = MC_state_new(); next_pair->automaton_state = transition_succ->dst; - next_pair->atomic_propositions = get_atomic_propositions_values(); + next_pair->atomic_propositions = this->getPropositionValues(); next_pair->depth = current_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()) @@ -499,15 +510,15 @@ static int MC_modelcheck_liveness_main(void) } } /* End of visited_pair test */ - + } else { backtracking: if(visited_num == -1) XBT_DEBUG("No more request to execute. Looking for backtracking point."); - + prop_values.reset(); - + /* 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 ((current_pair = (simgrid::mc::Pair*) xbt_fifo_shift(mc_stack)) != nullptr) { @@ -515,20 +526,20 @@ static int MC_modelcheck_liveness_main(void) /* We found a backtracking point */ XBT_DEBUG("Backtracking to depth %d", current_pair->depth); xbt_fifo_unshift(mc_stack, current_pair); - MC_replay_liveness(mc_stack); + this->replay(mc_stack); XBT_DEBUG("Backtracking done"); break; }else{ /* Delete pair */ XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); - if (current_pair->automaton_state->type == 1) - remove_acceptance_pair(current_pair->num); + if (current_pair->automaton_state->type == 1) + this->removeAcceptancePair(current_pair->num); delete current_pair; } } } /* End of if (current_pair->requests > 0) else ... */ - + } /* End of while(xbt_fifo_size(mc_stack) > 0) */ XBT_INFO("No property violation found."); @@ -536,7 +547,7 @@ static int MC_modelcheck_liveness_main(void) return SIMGRID_MC_EXIT_SUCCESS; } -int modelcheck_liveness(void) +int LivenessChecker::run() { XBT_INFO("Check the liveness property %s", _sg_mc_property_file); MC_automaton_load(_sg_mc_property_file); @@ -551,10 +562,8 @@ int modelcheck_liveness(void) /* Create the initial state */ initial_global_state = xbt_new0(s_mc_global_t, 1); - MC_pre_modelcheck_liveness(); - int res = MC_modelcheck_liveness_main(); - - return res; + this->prepare(); + return this->main(); } } diff --git a/src/mc/mc_liveness.h b/src/mc/LivenessChecker.hpp similarity index 67% rename from src/mc/mc_liveness.h rename to src/mc/LivenessChecker.hpp index c722183695..918c855ded 100644 --- a/src/mc/mc_liveness.h +++ b/src/mc/LivenessChecker.hpp @@ -4,8 +4,8 @@ /* 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_LIVENESS_H -#define SIMGRID_MC_LIVENESS_H +#ifndef SIMGRID_MC_LIVENESS_CHECKER_HPP +#define SIMGRID_MC_LIVENESS_CHECKER_HPP #include @@ -16,6 +16,7 @@ #include #include #include "src/mc/mc_state.h" +#include "src/mc/Checker.hpp" SG_BEGIN_DECL() @@ -60,7 +61,24 @@ struct XBT_PRIVATE VisitedPair { ~VisitedPair(); }; -int modelcheck_liveness(void); +class LivenessChecker : public Checker { +public: + LivenessChecker(Session& session); + ~LivenessChecker(); + int run() override; +private: + int main(); + void prepare(); + int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2); + void dumpStack(xbt_fifo_t stack); + void showStack(xbt_fifo_t stack); + simgrid::xbt::unique_ptr getPropositionValues(); + simgrid::mc::VisitedPair* insertAcceptancePair(simgrid::mc::Pair* pair); + int insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair); + void showAcceptanceCycle(std::size_t depth); + void replay(xbt_fifo_t stack); + void removeAcceptancePair(int pair_num); +}; } } diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index ca77039b80..e0d636b490 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -30,7 +30,7 @@ #include "src/mc/mc_private.h" #include "src/mc/mc_ignore.h" #include "src/mc/mc_exit.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index 6d208ddbd4..fc84a15db9 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -15,7 +15,7 @@ #include "src/internal_config.h" #include "src/mc/mc_forward.hpp" #include "src/mc/mc_safety.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_private.h" #include "src/mc/mc_smx.h" #include "src/mc/mc_dwarf.hpp" diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 24d755c076..93defaf036 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -29,7 +29,7 @@ #include "src/mc/mc_request.h" #include "src/mc/mc_safety.h" #include "src/mc/mc_snapshot.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_private.h" #include "src/mc/mc_unw.h" #include "src/mc/mc_smx.h" diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index 479b8dc356..32702eb70c 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -26,7 +26,7 @@ #include "src/mc/mc_private.h" #include "src/mc/mc_state.h" #include "src/mc/mc_smx.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #endif XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 6f136ec18d..d26d7aef7e 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -19,7 +19,7 @@ #include "src/mc/mc_comm_pattern.h" #include "src/mc/mc_safety.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_private.h" #include "src/mc/Process.hpp" #include "src/mc/mc_smx.h" diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index b8b4b08e76..ac45108e7d 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -24,7 +24,7 @@ #include "src/mc/mc_protocol.h" #include "src/mc/mc_safety.h" #include "src/mc/mc_comm_pattern.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_exit.h" #include "src/mc/Session.hpp" #include "src/mc/Checker.hpp" @@ -55,8 +55,8 @@ std::unique_ptr createChecker(simgrid::mc::Session& sessio return std::unique_ptr( new simgrid::mc::SafetyChecker(session)); else - code = [](Session& session) { - return simgrid::mc::modelcheck_liveness(); }; + return std::unique_ptr( + new simgrid::mc::LivenessChecker(session)); return std::unique_ptr( new FunctionalChecker(session, std::move(code))); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index bb79408e80..ca3b2bedc4 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -598,11 +598,11 @@ set(MC_SRC src/mc/mc_hash.cpp src/mc/mc_ignore.h src/mc/mc_mmalloc.h - src/mc/mc_liveness.h + src/mc/LivenessChecker.hpp src/mc/LocationList.hpp src/mc/malloc.hpp src/mc/LocationList.cpp - src/mc/mc_liveness.cpp + src/mc/LivenessChecker.cpp src/mc/mc_record.cpp src/mc/mc_member.cpp src/mc/mc_memory.cpp