From 5bb29d646b60d50cba45fbd654e7b08162370a8e Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Wed, 13 May 2020 11:06:38 +0200 Subject: [PATCH] mc: refactor parallel algorithms * spot/mc/Makefile.am, spot/mc/bloemen.hh, spot/mc/bloemen_ec.hh, spot/mc/cndfs.hh, spot/mc/deadlock.hh, spot/mc/ec.hh, spot/mc/intersect.hh, spot/mc/mc.hh, spot/mc/mc_instanciator.hh, spot/mc/utils.hh, tests/ltsmin/modelcheck.cc: Here. --- spot/mc/Makefile.am | 2 +- spot/mc/bloemen.hh | 86 +++-- spot/mc/bloemen_ec.hh | 113 +++---- spot/mc/cndfs.hh | 278 +++++++--------- spot/mc/deadlock.hh | 141 +++++---- spot/mc/ec.hh | 262 ++++++++++++---- spot/mc/intersect.hh | 285 +++-------------- spot/mc/mc.hh | 471 ++++++---------------------- spot/mc/mc_instanciator.hh | 198 ++++++++++++ spot/mc/utils.hh | 208 +++++++++++- tests/ltsmin/modelcheck.cc | 626 +++++++------------------------------ 11 files changed, 1169 insertions(+), 1501 deletions(-) create mode 100644 spot/mc/mc_instanciator.hh diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index 2ec1567c9..5307399bc 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -22,7 +22,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) mcdir = $(pkgincludedir)/mc mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\ - mc.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh + mc.hh mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh noinst_LTLIBRARIES = libmc.la diff --git a/spot/mc/bloemen.hh b/spot/mc/bloemen.hh index f2c9fa9d7..aee32418c 100644 --- a/spot/mc/bloemen.hh +++ b/spot/mc/bloemen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -21,15 +21,16 @@ #include #include -#include #include #include #include #include -#include +#include #include +#include #include #include +#include namespace spot { @@ -405,16 +406,6 @@ namespace spot fixed_size_pool p_; ///< \brief The allocator }; - /// \brief This object is returned by the algorithm below - struct SPOT_API bloemen_stats - { - unsigned inserted; ///< \brief Number of states inserted - unsigned states; ///< \brief Number of states visited - unsigned transitions; ///< \brief Number of transitions visited - unsigned sccs; ///< \brief Number of SCCs visited - unsigned walltime; ///< \brief Walltime for this thread in ms - }; - /// \brief This class implements the SCC decomposition algorithm of bloemen /// as described in PPOPP'16. It uses a shared union-find augmented to manage /// work stealing between threads. @@ -426,10 +417,25 @@ namespace spot swarmed_bloemen() = delete; public: - swarmed_bloemen(kripkecube& sys, - iterable_uf& uf, - unsigned tid): - sys_(sys), uf_(uf), tid_(tid), + + using uf = iterable_uf; + using uf_element = typename uf::uf_element; + + using shared_struct = uf; + using shared_map = typename uf::shared_map; + + static shared_struct* make_shared_st(shared_map m, unsigned i) + { + return new uf(m, i); + } + + swarmed_bloemen(kripkecube& sys, + twacube_ptr, /* useless here */ + shared_map& map, /* useless here */ + iterable_uf* uf, + unsigned tid, + std::atomic& /*useless here*/): + sys_(sys), uf_(*uf), tid_(tid), nb_th_(std::thread::hardware_concurrency()) { static_assert(spot::is_a_kripkecube_ptr; - using uf_element = typename uf::uf_element; - void run() { - tm_.start("DFS thread " + std::to_string(tid_)); - + setup(); State init = sys_.initial(tid_); auto pair = uf_.make_claim(init); todo_.push_back(pair.second); @@ -496,17 +498,53 @@ namespace spot Rp_.pop_back(); todo_.pop_back(); } + finalize(); + } + + void setup() + { + tm_.start("DFS thread " + std::to_string(tid_)); + } + + void finalize() + { tm_.stop("DFS thread " + std::to_string(tid_)); } + unsigned states() + { + return states_; + } + + unsigned transitions() + { + return transitions_; + } + unsigned walltime() { return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); } - bloemen_stats stats() + std::string name() { - return {uf_.inserted(), states_, transitions_, sccs_, walltime()}; + return "bloemen_scc"; + } + + int sccs() + { + return sccs_; + } + + mc_rvalue result() + { + return mc_rvalue::SUCCESS; + } + + std::string trace() + { + // Returning a trace has no sense in this algorithm + return ""; } private: diff --git a/spot/mc/bloemen_ec.hh b/spot/mc/bloemen_ec.hh index d80f9cd89..6be971ad4 100644 --- a/spot/mc/bloemen_ec.hh +++ b/spot/mc/bloemen_ec.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -31,6 +31,7 @@ #include #include #include +#include namespace spot { @@ -100,7 +101,6 @@ namespace spot using shared_map = brick::hashset::FastConcurrent ; - iterable_uf_ec(shared_map& map, unsigned tid): map_(map), tid_(tid), size_(std::thread::hardware_concurrency()), nb_th_(std::thread::hardware_concurrency()), inserted_(0), @@ -446,17 +446,6 @@ namespace spot fixed_size_pool p_; ///< \brief The allocator }; - /// \brief This object is returned by the algorithm below - struct SPOT_API bloemen_ec_stats - { - unsigned inserted; ///< \brief Number of states inserted - unsigned states; ///< \brief Number of states visited - unsigned transitions; ///< \brief Number of transitions visited - unsigned sccs; ///< \brief Number of SCCs visited - bool is_empty; ///< \brief Is the model empty - unsigned walltime; ///< \brief Walltime for this thread in ms - }; - /// \brief This class implements the SCC decomposition algorithm of bloemen /// as described in PPOPP'16. It uses a shared union-find augmented to manage /// work stealing between threads. @@ -466,12 +455,24 @@ namespace spot { public: + using uf = iterable_uf_ec; + using uf_element = typename uf::uf_element; + + using shared_struct = uf; + using shared_map = typename uf::shared_map; + + static shared_struct* make_shared_st(shared_map m, unsigned i) + { + return new uf(m, i); + } + swarmed_bloemen_ec(kripkecube& sys, twacube_ptr twa, - iterable_uf_ec& uf, + shared_map& map, /* useless here */ + iterable_uf_ec* uf, unsigned tid, std::atomic& stop): - sys_(sys), twa_(twa), uf_(uf), tid_(tid), + sys_(sys), twa_(twa), uf_(*uf), tid_(tid), nb_th_(std::thread::hardware_concurrency()), stop_(stop) { @@ -480,12 +481,9 @@ namespace spot "error: does not match the kripkecube requirements"); } - using uf = iterable_uf_ec; - using uf_element = typename uf::uf_element; - void run() { - tm_.start("DFS thread " + std::to_string(tid_)); + setup(); State init_kripke = sys_.initial(tid_); unsigned init_twa = twa_->get_initial(); auto pair = uf_.make_claim(init_kripke, init_twa); @@ -509,7 +507,7 @@ namespace spot auto it_kripke = sys_.succ(v_prime->st_kripke, tid_); auto it_prop = twa_->succ(v_prime->st_prop); - forward_iterators(it_kripke, it_prop, true); + forward_iterators(sys_, twa_, it_kripke, it_prop, true, tid_); while (!it_kripke->done()) { auto w = uf_.make_claim(it_kripke->state(), @@ -558,7 +556,8 @@ namespace spot return; } } - forward_iterators(it_kripke, it_prop, false); + forward_iterators(sys_, twa_, it_kripke, it_prop, + false, tid_); } uf_.remove_from_list(v_prime); sys_.recycle(it_kripke, tid_); @@ -568,53 +567,27 @@ namespace spot Rp_.pop_back(); todo_.pop_back(); } + finalize(); + } + + void setup() + { + tm_.start("DFS thread " + std::to_string(tid_)); + } + + void finalize() + { tm_.stop("DFS thread " + std::to_string(tid_)); } - /// \brief Find the first couple of iterator (from the top of the - /// todo stack) that intersect. The \a parameter indicates wheter - /// the state has just been pushed since the underlying job is - /// slightly different. - void forward_iterators(SuccIterator* it_kripke, - std::shared_ptr it_prop, - bool just_pushed) + unsigned states() { - SPOT_ASSERT(!(it_prop->done() && - it_kripke->done())); + return states_; + } - // Sometimes kripke state may have no successors. - if (it_kripke->done()) - return; - - // The state has just been push and the 2 iterators intersect. - // There is no need to move iterators forward. - SPOT_ASSERT(!(it_prop->done())); - if (just_pushed && twa_->get_cubeset() - .intersect(twa_->trans_data(it_prop, tid_).cube_, - it_kripke->condition())) - return; - - // Otherwise we have to compute the next valid successor (if it exits). - // This requires two loops. The most inner one is for the twacube since - // its costless - if (it_prop->done()) - it_prop->reset(); - else - it_prop->next(); - - while (!it_kripke->done()) - { - while (!it_prop->done()) - { - if (SPOT_UNLIKELY(twa_->get_cubeset() - .intersect(twa_->trans_data(it_prop, tid_).cube_, - it_kripke->condition()))) - return; - it_prop->next(); - } - it_prop->reset(); - it_kripke->next(); - } + unsigned transitions() + { + return transitions_; } unsigned walltime() @@ -622,15 +595,19 @@ namespace spot return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); } - bool is_empty() + std::string name() { - return is_empty_; + return "bloemen_ec"; } - bloemen_ec_stats stats() + int sccs() { - return {uf_.inserted(), states_, transitions_, sccs_, is_empty_, - walltime()}; + return sccs_; + } + + mc_rvalue result() + { + return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY; } std::string trace() diff --git a/spot/mc/cndfs.hh b/spot/mc/cndfs.hh index d84daf88a..b35ff6e70 100644 --- a/spot/mc/cndfs.hh +++ b/spot/mc/cndfs.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -29,22 +29,13 @@ #include #include #include +#include namespace spot { - /// \brief This object is returned by the algorithm below - struct SPOT_API cndfs_stats - { - unsigned states; ///< \brief Number of states visited - unsigned transitions; ///< \brief Number of transitions visited - unsigned instack_dfs; ///< \brief Maximum DFS stack - bool is_empty; ///< \brief Is the model empty - unsigned walltime; ///< \brief Walltime for this thread in ms - }; - template - class swarmed_cndfs + class SPOT_API swarmed_cndfs { struct local_colors { @@ -95,7 +86,7 @@ namespace spot } }; - struct todo__element + struct todo_element { product_state st; SuccIterator* it_kripke; @@ -108,9 +99,16 @@ namespace spot ///< \brief Shortcut to ease shared map manipulation using shared_map = brick::hashset::FastConcurrent ; + using shared_struct = shared_map; + + static shared_struct* make_shared_st(shared_map m, unsigned i) + { + return nullptr; // Useless here. + } swarmed_cndfs(kripkecube& sys, twacube_ptr twa, - shared_map& map, unsigned tid, std::atomic& stop): + shared_map& map, shared_struct* /* useless here*/, + unsigned tid, std::atomic& stop): sys_(sys), twa_(twa), tid_(tid), map_(map), nb_th_(std::thread::hardware_concurrency()), p_colors_(sizeof(cndfs_colors) + @@ -120,6 +118,7 @@ namespace spot static_assert(spot::is_a_kripkecube_ptr::value, "error: does not match the kripkecube requirements"); + SPOT_ASSERT(nb_th_ > tid); } virtual ~swarmed_cndfs() @@ -136,6 +135,13 @@ namespace spot } } + void run() + { + setup(); + blue_dfs(); + finalize(); + } + void setup() { tm_.start("DFS thread " + std::to_string(tid_)); @@ -180,17 +186,6 @@ namespace spot return {true, *it}; } - bool pop_blue() - { - // Track maximum dfs size - dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_; - - todo_blue_.back().st.colors->l[tid_].cyan = false; - sys_.recycle(todo_blue_.back().it_kripke, tid_); - todo_blue_.pop_back(); - return true; - } - std::pair push_red(product_state s, bool ignore_cyan) { @@ -216,6 +211,17 @@ namespace spot return {true, *it}; } + bool pop_blue() + { + // Track maximum dfs size + dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_; + + todo_blue_.back().st.colors->l[tid_].cyan = false; + sys_.recycle(todo_blue_.back().it_kripke, tid_); + todo_blue_.pop_back(); + return true; + } + bool pop_red() { // Track maximum dfs size @@ -243,13 +249,73 @@ namespace spot return transitions_; } - void run() + unsigned walltime() { - setup(); - blue_dfs(); - finalize(); + return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); } + std::string name() + { + return "cndfs"; + } + + int sccs() + { + return -1; + } + + mc_rvalue result() + { + return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY; + } + + std::string trace() + { + SPOT_ASSERT(!is_empty_); + StateEqual equal; + auto state_equal = [equal](product_state a, product_state b) + { + return a.st_prop == b.st_prop + && equal(a.st_kripke, b.st_kripke); + }; + + std::string res = "Prefix:\n"; + + auto it = todo_blue_.begin(); + while (it != todo_blue_.end()) + { + if (state_equal(((*it)).st, cycle_start_)) + break; + res += " " + std::to_string(((*it)).st.st_prop) + + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n"; + ++it; + } + + res += "Cycle:\n"; + while (it != todo_blue_.end()) + { + res += " " + std::to_string(((*it)).st.st_prop) + + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n"; + ++it; + } + + if (!todo_red_.empty()) + { + it = todo_red_.begin() + 1; // skip first element, also in blue + while (it != todo_red_.end()) + { + res += " " + std::to_string(((*it)).st.st_prop) + + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n"; + ++it; + } + } + res += " " + std::to_string(cycle_start_.st_prop) + + "*" + sys_.to_string(cycle_start_.st_kripke) + "\n"; + + return res; + } + + private: void blue_dfs() { product_state initial = {sys_.initial(tid_), @@ -262,7 +328,8 @@ namespace spot if (todo_blue_.back().it_prop->done()) return; - forward_iterators(todo_blue_, true); + forward_iterators(sys_, twa_, todo_blue_.back().it_kripke, + todo_blue_.back().it_prop, true, tid_); while (!todo_blue_.empty() && !stop_.load(std::memory_order_relaxed)) { @@ -278,11 +345,13 @@ namespace spot }; bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_; - forward_iterators(todo_blue_, false); + forward_iterators(sys_, twa_, todo_blue_.back().it_kripke, + todo_blue_.back().it_prop, false, tid_); auto tmp = push_blue(s, acc); if (tmp.first) - forward_iterators(todo_blue_, true); + forward_iterators(sys_, twa_, todo_blue_.back().it_kripke, + todo_blue_.back().it_prop, true, tid_); else if (acc) { // The state cyan and we can reach it throught an @@ -324,14 +393,14 @@ namespace spot void post_red_dfs() { - for (product_state& s : Rp_acc_) + for (product_state& s: Rp_acc_) { while (s.colors->red.load() && !stop_.load()) { // await } } - for (product_state& s : Rp_) + for (product_state& s: Rp_) { s.colors->red.store(true); s.colors->l[tid_].is_in_Rp = false; // empty Rp @@ -349,7 +418,8 @@ namespace spot if (!init_push.first) return; - forward_iterators(todo_red_, true); + forward_iterators(sys_, twa_, todo_red_.back().it_kripke, + todo_red_.back().it_prop, true, tid_); while (!todo_red_.empty() && !stop_.load(std::memory_order_relaxed)) { @@ -364,12 +434,14 @@ namespace spot nullptr }; bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_; - forward_iterators(todo_red_, false); + forward_iterators(sys_, twa_, todo_red_.back().it_kripke, + todo_red_.back().it_prop, false, tid_); auto res = push_red(s, false); if (res.first) // could push properly { - forward_iterators(todo_red_, true); + forward_iterators(sys_, twa_, todo_red_.back().it_kripke, + todo_red_.back().it_prop, true, tid_); SPOT_ASSERT(res.second.colors->blue); @@ -419,130 +491,22 @@ namespace spot } } - std::string trace() - { - SPOT_ASSERT(!is_empty()); - StateEqual equal; - auto state_equal = [equal](product_state a, product_state b) - { - return a.st_prop == b.st_prop - && equal(a.st_kripke, b.st_kripke); - }; - - std::string res = "Prefix:\n"; - - auto it = todo_blue_.begin(); - while (it != todo_blue_.end()) - { - if (state_equal(((*it)).st, cycle_start_)) - break; - res += " " + std::to_string(((*it)).st.st_prop) - + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n"; - ++it; - } - - res += "Cycle:\n"; - while (it != todo_blue_.end()) - { - res += " " + std::to_string(((*it)).st.st_prop) - + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n"; - ++it; - } - - if (!todo_red_.empty()) - { - it = todo_red_.begin() + 1; // skip first element, also in blue - while (it != todo_red_.end()) - { - res += " " + std::to_string(((*it)).st.st_prop) - + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n"; - ++it; - } - } - res += " " + std::to_string(cycle_start_.st_prop) - + "*" + sys_.to_string(cycle_start_.st_kripke) + "\n"; - - return res; - } - - bool is_empty() - { - return is_empty_; - } - - unsigned walltime() - { - return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); - } - - cndfs_stats stats() - { - return {states(), transitions(), dfs_, is_empty(), walltime()}; - } - - protected: - void forward_iterators(std::vector& todo, bool just_pushed) - { - SPOT_ASSERT(!todo.empty()); - - auto top = todo.back(); - - SPOT_ASSERT(!(top.it_prop->done() && - top.it_kripke->done())); - - // Sometimes kripke state may have no successors. - if (top.it_kripke->done()) - return; - - // The state has just been push and the 2 iterators intersect. - // There is no need to move iterators forward. - SPOT_ASSERT(!(top.it_prop->done())); - if (just_pushed && twa_->get_cubeset() - .intersect(twa_->trans_data(top.it_prop, tid_).cube_, - top.it_kripke->condition())) - return; - - // Otherwise we have to compute the next valid successor (if it exits). - // This requires two loops. The most inner one is for the twacube since - // its costless - if (top.it_prop->done()) - top.it_prop->reset(); - else - top.it_prop->next(); - - while (!top.it_kripke->done()) - { - while (!top.it_prop->done()) - { - if (twa_->get_cubeset() - .intersect(twa_->trans_data(top.it_prop, tid_).cube_, - top.it_kripke->condition())) - return; - top.it_prop->next(); - } - top.it_prop->reset(); - top.it_kripke->next(); - } - } - - private: - kripkecube& sys_; - twacube_ptr twa_; - std::vector todo_blue_; - std::vector todo_red_; - unsigned transitions_ = 0; ///< \brief Number of transitions - unsigned tid_; ///< \brief Thread's current ID + kripkecube& sys_; ///< \brief The system to check + twacube_ptr twa_; ///< \brief The propertu to check + std::vector todo_blue_; ///< \brief Blue Stack + std::vector todo_red_; ///< \ brief Red Stack + unsigned transitions_ = 0; ///< \brief Number of transitions + unsigned tid_; ///< \brief Thread's current ID shared_map map_; ///< \brief Map shared by threads spot::timer_map tm_; ///< \brief Time execution unsigned states_ = 0; ///< \brief Number of states unsigned dfs_ = 0; ///< \brief Maximum DFS stack size - /// \brief Maximum number of threads that can be handled by this algorithm - unsigned nb_th_ = 0; - fixed_size_pool p_colors_; - bool is_empty_ = true; ///< \brief Accepting cycle detected? + unsigned nb_th_ = 0; /// \brief Maximum number of threads + fixed_size_pool p_colors_; /// \brief Memory pool + bool is_empty_ = true; ///< \brief Accepting cycle detected? std::atomic& stop_; ///< \brief Stop-the-world boolean - std::vector Rp_; - std::vector Rp_acc_; - product_state cycle_start_; + std::vector Rp_; ///< \brief Rp stack + std::vector Rp_acc_; ///< \brief Rp acc stack + product_state cycle_start_; ///< \brief Begining of a cycle }; } diff --git a/spot/mc/deadlock.hh b/spot/mc/deadlock.hh index ebd465040..a8c9946ff 100644 --- a/spot/mc/deadlock.hh +++ b/spot/mc/deadlock.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -32,22 +32,12 @@ namespace spot { - /// \brief This object is returned by the algorithm below - struct SPOT_API deadlock_stats - { - unsigned states; ///< \brief Number of states visited - unsigned transitions; ///< \brief Number of transitions visited - unsigned instack_dfs; ///< \brief Maximum DFS stack - bool has_deadlock; ///< \brief Does the model contains a deadlock - unsigned walltime; ///< \brief Walltime for this thread in ms - }; - /// \brief This class aims to explore a model to detect wether it /// contains a deadlock. This deadlock detection performs a DFS traversal /// sharing information shared among multiple threads. template - class swarmed_deadlock + class SPOT_API swarmed_deadlock { /// \brief Describes the status of a state enum st_status @@ -94,9 +84,18 @@ namespace spot ///< \brief Shortcut to ease shared map manipulation using shared_map = brick::hashset::FastConcurrent ; + using shared_struct = shared_map; + + static shared_struct* make_shared_st(shared_map, unsigned) + { + return nullptr; // Useless + } swarmed_deadlock(kripkecube& sys, - shared_map& map, unsigned tid, std::atomic& stop): + twacube_ptr, /* useless here */ + shared_map& map, shared_struct* /* useless here */, + unsigned tid, + std::atomic& stop): sys_(sys), tid_(tid), map_(map), nb_th_(std::thread::hardware_concurrency()), p_(sizeof(int)*std::thread::hardware_concurrency()), @@ -106,6 +105,7 @@ namespace spot static_assert(spot::is_a_kripkecube_ptr::value, "error: does not match the kripkecube requirements"); + SPOT_ASSERT(nb_th_ > tid); } virtual ~swarmed_deadlock() @@ -117,6 +117,46 @@ namespace spot } } + void run() + { + setup(); + State initial = sys_.initial(tid_); + if (SPOT_LIKELY(push(initial))) + { + todo_.push_back({initial, sys_.succ(initial, tid_), transitions_}); + } + while (!todo_.empty() && !stop_.load(std::memory_order_relaxed)) + { + if (todo_.back().it->done()) + { + if (SPOT_LIKELY(pop())) + { + deadlock_ = todo_.back().current_tr == transitions_; + if (deadlock_) + break; + sys_.recycle(todo_.back().it, tid_); + todo_.pop_back(); + } + } + else + { + ++transitions_; + State dst = todo_.back().it->state(); + + if (SPOT_LIKELY(push(dst))) + { + todo_.back().it->next(); + todo_.push_back({dst, sys_.succ(dst, tid_), transitions_}); + } + else + { + todo_.back().it->next(); + } + } + } + finalize(); + } + void setup() { tm_.start("DFS thread " + std::to_string(tid_)); @@ -187,72 +227,45 @@ namespace spot return transitions_; } - void run() - { - setup(); - State initial = sys_.initial(tid_); - if (SPOT_LIKELY(push(initial))) - { - todo_.push_back({initial, sys_.succ(initial, tid_), transitions_}); - } - while (!todo_.empty() && !stop_.load(std::memory_order_relaxed)) - { - if (todo_.back().it->done()) - { - if (SPOT_LIKELY(pop())) - { - deadlock_ = todo_.back().current_tr == transitions_; - if (deadlock_) - break; - sys_.recycle(todo_.back().it, tid_); - todo_.pop_back(); - } - } - else - { - ++transitions_; - State dst = todo_.back().it->state(); - - if (SPOT_LIKELY(push(dst))) - { - todo_.back().it->next(); - todo_.push_back({dst, sys_.succ(dst, tid_), transitions_}); - } - else - { - todo_.back().it->next(); - } - } - } - finalize(); - } - - bool has_deadlock() - { - return deadlock_; - } - unsigned walltime() { return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); } - deadlock_stats stats() + std::string name() { - return {states(), transitions(), dfs_, has_deadlock(), walltime()}; + return "deadlock"; + } + + int sccs() + { + return -1; + } + + mc_rvalue result() + { + return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK; + } + + std::string trace() + { + std::string result; + for (auto& e: todo_) + result += sys_.to_string(e.s, tid_); + return result; } private: - struct todo__element + struct todo_element { State s; SuccIterator* it; unsigned current_tr; }; kripkecube& sys_; ///< \brief The system to check - std::vector todo_; ///< \brief The DFS stack - unsigned transitions_ = 0; ///< \brief Number of transitions - unsigned tid_; ///< \brief Thread's current ID + std::vector todo_; ///< \brief The DFS stack + unsigned transitions_ = 0; ///< \brief Number of transitions + unsigned tid_; ///< \brief Thread's current ID shared_map map_; ///< \brief Map shared by threads spot::timer_map tm_; ///< \brief Time execution unsigned states_ = 0; ///< \brief Number of states diff --git a/spot/mc/ec.hh b/spot/mc/ec.hh index 16dd64a07..8f1b7e1cb 100644 --- a/spot/mc/ec.hh +++ b/spot/mc/ec.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2018, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -22,6 +22,7 @@ #include #include #include +#include namespace spot { @@ -32,50 +33,148 @@ namespace spot /// the Gabow's one. template - class ec_renault13lpar : public intersect> + class SPOT_API ec_renault13lpar { - // Ease the manipulation - using typename intersect>::product_state; + struct product_state + { + State st_kripke; + unsigned st_prop; + }; + + struct product_state_equal + { + bool + operator()(const product_state lhs, + const product_state rhs) const + { + StateEqual equal; + return (lhs.st_prop == rhs.st_prop) && + equal(lhs.st_kripke, rhs.st_kripke); + } + }; + + struct product_state_hash + { + size_t + operator()(const product_state that) const noexcept + { + // FIXME! wang32_hash(that.st_prop) could have + // been pre-calculated! + StateHash hasher; + return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); + } + }; public: - ec_renault13lpar() = delete; - ec_renault13lpar(const ec_renault13lpar&) = default; - ec_renault13lpar(ec_renault13lpar&) = delete; + using shared_map = int; // Useless here. + using shared_struct = int; // Useless here. + + static shared_struct* make_shared_st(shared_map m, unsigned i) + { + return nullptr; // Useless + } ec_renault13lpar(kripkecube& sys, - twacube_ptr twa, unsigned tid, bool stop) - : intersect>(sys, twa, tid, stop), - acc_(twa->acc()), sccs_(0U) + twacube_ptr twa, + shared_map& map, /* useless here */ + shared_struct*, /* useless here */ + unsigned tid, + std::atomic& stop) + : sys_(sys), twa_(twa), tid_(tid), stop_(stop), + acc_(twa->acc()), sccs_(0U) { + static_assert(spot::is_a_kripkecube_ptr::value, + "error: does not match the kripkecube requirements"); } virtual ~ec_renault13lpar() { - + map.clear(); + } + + bool run() + { + setup(); + product_state initial = {sys_.initial(tid_), twa_->get_initial()}; + if (SPOT_LIKELY(push_state(initial, dfs_number+1, {}))) + { + todo.push_back({initial, sys_.succ(initial.st_kripke, tid_), + twa_->succ(initial.st_prop)}); + + // Not going further! It's a product with a single state. + if (todo.back().it_prop->done()) + return false; + + forward_iterators(sys_, twa_, todo.back().it_kripke, + todo.back().it_prop, true, 0); + map[initial] = ++dfs_number; + } + while (!todo.empty() && !stop_.load(std::memory_order_relaxed)) + { + // Check the kripke is enough since it's the outer loop. More + // details in forward_iterators. + if (todo.back().it_kripke->done()) + { + bool is_init = todo.size() == 1; + auto newtop = is_init? todo.back().st: todo[todo.size() -2].st; + if (SPOT_LIKELY(pop_state(todo.back().st, + map[todo.back().st], + is_init, + newtop, + map[newtop]))) + { + sys_.recycle(todo.back().it_kripke, tid_); + // FIXME a local storage for twacube iterator? + todo.pop_back(); + if (SPOT_UNLIKELY(found_)) + { + finalize(); + return true; + } + } + } + else + { + ++trans_; + product_state dst = + { + todo.back().it_kripke->state(), + twa_->trans_storage(todo.back().it_prop, tid_).dst + }; + auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_; + forward_iterators(sys_, twa_, todo.back().it_kripke, + todo.back().it_prop, false, 0); + auto it = map.find(dst); + if (it == map.end()) + { + if (SPOT_LIKELY(push_state(dst, dfs_number+1, acc))) + { + map[dst] = ++dfs_number; + todo.push_back({dst, sys_.succ(dst.st_kripke, tid_), + twa_->succ(dst.st_prop)}); + forward_iterators(sys_, twa_, todo.back().it_kripke, + todo.back().it_prop, true, 0); + } + } + else if (SPOT_UNLIKELY(update(todo.back().st, + dfs_number, + dst, map[dst], acc))) + { + finalize(); + return true; + } + } + } + return false; } - /// \brief This method is called at the begining of the exploration. - /// here we do not need to setup any information. void setup() { + tm_.start("DFS thread " + std::to_string(tid_)); } - /// \brief This method is called to notify the emptiness checks - /// that a new state has been discovered. If this method return - /// false, the state will not be explored. The parameter \a dfsnum - /// specify a unique id for the state. Parameter \a cond represents - /// The value on the ingoing edge to \a s. bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond) { uf_.makeset(dfsnum); @@ -99,7 +198,7 @@ namespace spot ++sccs_; uf_.markdead(top_dfsnum); } - dfs_ = this->todo.size() > dfs_ ? this->todo.size() : dfs_; + dfs_ = todo.size() > dfs_ ? todo.size() : dfs_; return true; } @@ -122,24 +221,54 @@ namespace spot roots_.back().acc |= cond; found_ = acc_.accepting(roots_.back().acc); if (SPOT_UNLIKELY(found_)) - this->stop_ = true; + stop_ = true; return found_; } - bool counterexample_found() + void finalize() { - return found_; + tm_.stop("DFS thread " + std::to_string(tid_)); + } + + unsigned int states() + { + return dfs_number; + } + + unsigned int transitions() + { + return trans_; + } + + unsigned walltime() + { + return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); + } + + std::string name() + { + return "renault_lpar13"; + } + + int sccs() + { + return sccs_; + } + + mc_rvalue result() + { + return !found_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY; } std::string trace() { - SPOT_ASSERT(counterexample_found()); + SPOT_ASSERT(found_); std::string res = "Prefix:\n"; // Compute the prefix of the accepting run - for (auto& s : this->todo) + for (auto& s : todo) res += " " + std::to_string(s.st.st_prop) + - + "*" + this->sys_.to_string(s.st.st_kripke) + "\n"; + + "*" + sys_.to_string(s.st.st_kripke) + "\n"; // Compute the accepting cycle res += "Cycle:\n"; @@ -155,9 +284,9 @@ namespace spot acc_cond::mark_t acc = {}; - bfs.push(new ctrx_element({&this->todo.back().st, nullptr, - this->sys_.succ(this->todo.back().st.st_kripke, this->tid_), - this->twa_->succ(this->todo.back().st.st_prop)})); + bfs.push(new ctrx_element({&todo.back().st, nullptr, + sys_.succ(todo.back().st.st_kripke, tid_), + twa_->succ(todo.back().st.st_prop)})); while (true) { here: @@ -168,20 +297,20 @@ namespace spot { while (!front->it_prop->done()) { - if (this->twa_->get_cubeset().intersect - (this->twa_->trans_data(front->it_prop, this->tid_).cube_, + if (twa_->get_cubeset().intersect + (twa_->trans_data(front->it_prop, tid_).cube_, front->it_kripke->condition())) { const product_state dst = { front->it_kripke->state(), - this->twa_->trans_storage(front->it_prop).dst + twa_->trans_storage(front->it_prop).dst }; // Skip Unknown states or not same SCC - auto it = this->map.find(dst); - if (it == this->map.end() || + auto it = map.find(dst); + if (it == map.end() || !uf_.sameset(it->second, - this->map[this->todo.back().st])) + map[todo.back().st])) { front->it_prop->next(); continue; @@ -190,8 +319,8 @@ namespace spot // This is a valid transition. If this transition // is the one we are looking for, update the counter- // -example and flush the bfs queue. - auto mark = this->twa_->trans_data(front->it_prop, - this->tid_).acc_; + auto mark = twa_->trans_data(front->it_prop, + tid_).acc_; if (!(acc & mark)) { ctrx_element* current = front; @@ -201,8 +330,7 @@ namespace spot res = res + " " + std::to_string(current->prod_st->st_prop) + + "*" + - this->sys_. to_string(current->prod_st - ->st_kripke) + + sys_. to_string(current->prod_st->st_kripke) + "\n"; current = current->parent_st; } @@ -217,14 +345,14 @@ namespace spot // update acceptance acc |= mark; - if (this->twa_->acc().accepting(acc)) + if (twa_->acc().accepting(acc)) return res; const product_state* q = &(it->first); ctrx_element* root = new ctrx_element({ q , nullptr, - this->sys_.succ(q->st_kripke, this->tid_), - this->twa_->succ(q->st_prop) + sys_.succ(q->st_kripke, tid_), + twa_->succ(q->st_prop) }); bfs.push(root); goto here; @@ -234,8 +362,8 @@ namespace spot const product_state* q = &(it->first); ctrx_element* root = new ctrx_element({ q , nullptr, - this->sys_.succ(q->st_kripke, this->tid_), - this->twa_->succ(q->st_prop) + sys_.succ(q->st_kripke, tid_), + twa_->succ(q->st_prop) }); bfs.push(root); } @@ -250,15 +378,14 @@ namespace spot return res; } - virtual istats stats() override - { - return {this->states(), this->trans(), sccs_, - (unsigned) roots_.size(), dfs_, found_}; - } - private: - bool found_ = false; ///< \brief A counterexample is detected? + struct todo_element + { + product_state st; + SuccIterator* it_kripke; + std::shared_ptr it_prop; + }; struct root_element { unsigned dfsnum; @@ -266,11 +393,24 @@ namespace spot acc_cond::mark_t acc; }; - /// \brief the root stack. + typedef std::unordered_map visited_map; + + kripkecube& sys_; + twacube_ptr twa_; + std::vector todo; + visited_map map; + unsigned int dfs_number = 0; + unsigned int trans_ = 0; + unsigned tid_; + std::atomic& stop_; ///< \brief Stop-the-world boolean + bool found_ = false; std::vector roots_; int_unionfind uf_; acc_cond acc_; unsigned sccs_; unsigned dfs_; + spot::timer_map tm_; }; } diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh index 9b619329b..378bcf638 100644 --- a/spot/mc/intersect.hh +++ b/spot/mc/intersect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018, 2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2018, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -25,251 +25,54 @@ namespace spot { - /// \brief Wrapper to accumulate results from intersection - /// and emptiness checks - struct SPOT_API istats + /// \brief Find the first couple of iterator (from a given pair of + /// interators) that intersect. This method can be used in any + /// DFS/BFS-like exploration algorithm. The \a parameter indicates + /// wheter the state has just been visited since the underlying job + /// is slightly different. + template + static void forward_iterators(kripkecube& sys, + twacube_ptr twa, + SuccIterator* it_kripke, + std::shared_ptr it_prop, + bool just_visited, + unsigned tid) { - unsigned states; - unsigned transitions; - unsigned sccs; - unsigned instack_sccs; - unsigned instack_item; - bool is_empty; - }; + (void) sys; // System is useless, but the API is clearer + SPOT_ASSERT(!(it_prop->done() && it_kripke->done())); - /// \brief This class explores (with a DFS) a product between a - /// system and a twa. This exploration is performed on-the-fly. - /// Since this exploration aims to be a generic we need to define - /// hooks to the various emptiness checks. - /// Actually, we use "mixins templates" in order to efficiently - /// call emptiness check procedure. This means that we add - /// a template \a EmptinessCheck that will be called though - /// four functions: - /// - setup: called before any operation - /// - push: called for every new state - /// - pop: called every time a state leave the DFS stack - /// - update: called for every closing edge - /// - trace: must return a counterexample (if exists) - /// - /// The other template parameters allows to consider any kind - /// of state (and so any kind of kripke structures). - template - class SPOT_API intersect - { - public: - intersect(const intersect& i) = default; + // Sometimes kripke state may have no successors. + if (it_kripke->done()) + return; - intersect(kripkecube& sys, - twacube_ptr twa, unsigned tid, bool& stop): - sys_(sys), twa_(twa), tid_(tid), stop_(stop) - { - static_assert(spot::is_a_kripkecube_ptr::value, - "error: does not match the kripkecube requirements"); - map.reserve(2000000); - todo.reserve(100000); - } + // The state has just been visited and the 2 iterators intersect. + // There is no need to move iterators forward. + SPOT_ASSERT(!(it_prop->done())); + if (just_visited && twa->get_cubeset() + .intersect(twa->trans_data(it_prop, tid).cube_, + it_kripke->condition())) + return; - ~intersect() - { - map.clear(); - } + // Otherwise we have to compute the next valid successor (if it exits). + // This requires two loops. The most inner one is for the twacube since + // its costless + if (it_prop->done()) + it_prop->reset(); + else + it_prop->next(); - /// \brief In order to implement "mixin paradigm", we - /// must be abble to access the acual definition of - /// the emptiness check that, in turn, has to access - /// local variables. - EmptinessCheck& self() - { - return static_cast(*this); - } - - /// \brief The main function that will perform the - /// product on-the-fly and call the emptiness check - /// when necessary. - bool run() - { - self().setup(); - product_state initial = {sys_.initial(tid_), twa_->get_initial()}; - if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, {}))) - { - todo.push_back({initial, sys_.succ(initial.st_kripke, tid_), - twa_->succ(initial.st_prop)}); - - // Not going further! It's a product with a single state. - if (todo.back().it_prop->done()) - return false; - - forward_iterators(true); - map[initial] = ++dfs_number; - } - while (!todo.empty() && !stop_) - { - // Check the kripke is enough since it's the outer loop. More - // details in forward_iterators. - if (todo.back().it_kripke->done()) - { - bool is_init = todo.size() == 1; - auto newtop = is_init? todo.back().st: todo[todo.size() -2].st; - if (SPOT_LIKELY(self().pop_state(todo.back().st, - map[todo.back().st], - is_init, - newtop, - map[newtop]))) - { - sys_.recycle(todo.back().it_kripke, tid_); - // FIXME a local storage for twacube iterator? - todo.pop_back(); - if (SPOT_UNLIKELY(self().counterexample_found())) - return true; - } - } - else - { - ++transitions; - product_state dst = { - todo.back().it_kripke->state(), - twa_->trans_storage(todo.back().it_prop, tid_).dst - }; - auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_; - forward_iterators(false); - auto it = map.find(dst); - if (it == map.end()) - { - if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc))) - { - map[dst] = ++dfs_number; - todo.push_back({dst, sys_.succ(dst.st_kripke, tid_), - twa_->succ(dst.st_prop)}); - forward_iterators(true); - } - } - else if (SPOT_UNLIKELY(self().update(todo.back().st, - dfs_number, - dst, map[dst], acc))) - return true; - } - } - return false; - } - - unsigned int states() - { - return dfs_number; - } - - unsigned int trans() - { - return transitions; - } - - std::string counterexample() - { - return self().trace(); - } - - virtual istats stats() - { - return {dfs_number, transitions, 0U, 0U, 0U, false}; - } - - protected: - - /// \brief Find the first couple of iterator (from the top of the - /// todo stack) that intersect. The \a parameter indicates wheter - /// the state has just been pushed since the underlying job - /// is slightly different. - void forward_iterators(bool just_pushed) - { - SPOT_ASSERT(!todo.empty()); - SPOT_ASSERT(!(todo.back().it_prop->done() && - todo.back().it_kripke->done())); - - // Sometimes kripke state may have no successors. - if (todo.back().it_kripke->done()) - return; - - // The state has just been push and the 2 iterators intersect. - // There is no need to move iterators forward. - SPOT_ASSERT(!(todo.back().it_prop->done())); - if (just_pushed && twa_->get_cubeset() - .intersect(twa_->trans_data(todo.back().it_prop, tid_).cube_, - todo.back().it_kripke->condition())) - return; - - // Otherwise we have to compute the next valid successor (if it exits). - // This requires two loops. The most inner one is for the twacube since - // its costless - if (todo.back().it_prop->done()) - todo.back().it_prop->reset(); - else - todo.back().it_prop->next(); - - while (!todo.back().it_kripke->done()) - { - while (!todo.back().it_prop->done()) - { - if (SPOT_UNLIKELY(twa_->get_cubeset() - .intersect(twa_->trans_data(todo.back().it_prop, tid_).cube_, - todo.back().it_kripke->condition()))) - return; - todo.back().it_prop->next(); - } - todo.back().it_prop->reset(); - todo.back().it_kripke->next(); - } - } - - public: - struct product_state - { - State st_kripke; - unsigned st_prop; - }; - - struct product_state_equal - { - bool - operator()(const product_state lhs, - const product_state rhs) const + while (!it_kripke->done()) { - StateEqual equal; - return (lhs.st_prop == rhs.st_prop) && - equal(lhs.st_kripke, rhs.st_kripke); + while (!it_prop->done()) + { + if (SPOT_UNLIKELY(twa->get_cubeset() + .intersect(twa->trans_data(it_prop, tid).cube_, + it_kripke->condition()))) + return; + it_prop->next(); + } + it_prop->reset(); + it_kripke->next(); } - }; - - struct product_state_hash - { - size_t - operator()(const product_state that) const noexcept - { - // FIXME! wang32_hash(that.st_prop) could have - // been pre-calculated! - StateHash hasher; - return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); - } - }; - - struct todo_element - { - product_state st; - SuccIterator* it_kripke; - std::shared_ptr it_prop; - }; - kripkecube& sys_; - twacube_ptr twa_; - std::vector todo; - typedef std::unordered_map visited_map; - visited_map map; - unsigned int dfs_number = 0; - unsigned int transitions = 0; - unsigned tid_; - bool& stop_; // Do not need to be atomic. - }; + } } diff --git a/spot/mc/mc.hh b/spot/mc/mc.hh index 14a2c34b7..2cabd17a7 100644 --- a/spot/mc/mc.hh +++ b/spot/mc/mc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017, 2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -19,398 +19,133 @@ #pragma once -#include #include -#include -#include #include #include -#include -#include -#include -#include -#include -#include -#include -#include namespace spot { - /// \brief Check for the emptiness between a system and a twa. - /// Return a pair containing a boolean indicating wether a counterexample - /// has been found and a string representing the counterexample if the - /// computation have been required - template - static std::tuple> - modelcheck(kripke_ptr sys, spot::twacube_ptr twa, bool compute_ctrx = false) + /// \brief The list of parallel model-checking algorithms available + enum SPOT_API class mc_algorithm + { + BLOEMEN_EC, ///< \brief Bloemen.16.hvc emptiness check + BLOEMEN_SCC, ///< \brief Bloemen.16.ppopp SCC computation + CNDFS, ///< \brief Evangelista.12.atva emptiness check + DEADLOCK, ///< \brief Check wether there is a deadlock + SWARMING, ///< \brief Holzmann.11.ieee applied to renault.13.lpar + }; + + enum SPOT_API class mc_rvalue + { + DEADLOCK, ///< \brief A deadlock has been found + EMPTY, ///< \brief The product is empty + FAILURE, ///< \brief The Algorithm finished abnormally + NO_DEADLOCK, ///< \brief No deadlock has been found + NOT_EMPTY, ///< \brief The product is not empty + SUCCESS, ///< \brief The Algorithm finished normally + }; + + /// \brief This structure contains, for each thread, the collected information + /// during the traversal + struct SPOT_API ec_stats { - // Must ensure that the two automata are working on the same - // set of atomic propositions. - SPOT_ASSERT(sys->get_ap().size() == twa->get_ap().size()); - for (unsigned int i = 0; i < sys->get_ap().size(); ++i) - SPOT_ASSERT(sys->get_ap()[i].compare(twa->get_ap()[i]) == 0); + std::vector name; ///< \brief The name of the algorithm used + std::vector walltime; ///< \brief Walltime for this thread in ms + std::vector states; ///< \brief Number of states visited + std::vector transitions; ///< \brief Number of transitions visited + std::vector sccs; ///< \brief Number of SCCs or -1 + std::vector value; ///< \brief The return status + std::string trace; ///< \brief The output trace + }; - bool stop = false; - std::vector> ecs; - for (unsigned i = 0; i < sys->get_threads(); ++i) - ecs.push_back({*sys, twa, i, stop}); - - std::vector threads; - for (unsigned i = 0; i < sys->get_threads(); ++i) - threads.push_back - (std::thread(&ec_renault13lpar::run, - &ecs[i])); - - for (unsigned i = 0; i < sys->get_threads(); ++i) - threads[i].join(); - - bool has_ctrx = false; - std::string trace = ""; - std::vector stats; - for (unsigned i = 0; i < sys->get_threads(); ++i) + SPOT_API std::ostream& operator<<(std::ostream& os, const mc_algorithm& ma) + { + switch (ma) { - has_ctrx |= ecs[i].counterexample_found(); - if (compute_ctrx && ecs[i].counterexample_found() - && trace.compare("") == 0) - trace = ecs[i].trace(); // Pick randomly one ! - stats.push_back(ecs[i].stats()); + case mc_algorithm::BLOEMEN_EC: + os << "bloemen_ec"; break; + case mc_algorithm::BLOEMEN_SCC: + os << "bloemen_scc"; break; + case mc_algorithm::CNDFS: + os << "cndfs"; break; + case mc_algorithm::DEADLOCK: + os << "deadlock"; break; + case mc_algorithm::SWARMING: + os << "swarming"; break; } - return std::make_tuple(has_ctrx, trace, stats); + return os; } - /// \bief Check wether the system contains a deadlock. The algorithm - /// spawns multiple threads performing a classical swarming DFS. As - /// soon one thread detects a deadlock all the other threads are stopped. - template - static std::tuple, spot::timer_map> - has_deadlock(kripke_ptr sys) + SPOT_API std::ostream& operator<<(std::ostream& os, const mc_rvalue& mr) { - spot::timer_map tm; - using algo_name = spot::swarmed_deadlock; - - unsigned nbth = sys->get_threads(); - typename algo_name::shared_map map; - std::atomic stop(false); - - tm.start("Initialisation"); - std::vector swarmed(nbth); - for (unsigned i = 0; i < nbth; ++i) - swarmed[i] = new algo_name(*sys, map, i, stop); - tm.stop("Initialisation"); - - std::mutex iomutex; - std::atomic barrier(true); - std::vector threads(nbth); - for (unsigned i = 0; i < nbth; ++i) + switch (mr) { - threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier] - { -#if defined(unix) || defined(__unix__) || defined(__unix) - { - std::lock_guard iolock(iomutex); - std::cout << "Thread #" << i - << ": on CPU " << sched_getcpu() << '\n'; - } -#endif - - // Wait all threads to be instanciated. - while (barrier) - continue; - swarmed[i]->run(); - }); - -#if defined(unix) || defined(__unix__) || defined(__unix) - // Pins threads to a dedicated core. - cpu_set_t cpuset; - CPU_ZERO(&cpuset); - CPU_SET(i, &cpuset); - int rc = pthread_setaffinity_np(threads[i].native_handle(), - sizeof(cpu_set_t), &cpuset); - if (rc != 0) - { - std::lock_guard iolock(iomutex); - std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n'; - } -#endif + case mc_rvalue::DEADLOCK: + os << "deadlock"; break; + case mc_rvalue::EMPTY: + os << "empty"; break; + case mc_rvalue::FAILURE: + os << "failure"; break; + case mc_rvalue::NO_DEADLOCK: + os << "no_deadlock"; break; + case mc_rvalue::NOT_EMPTY: + os << "not_empty"; break; + case mc_rvalue::SUCCESS: + os << "success"; break; } - - tm.start("Run"); - barrier.store(false); - - for (auto& t : threads) - t.join(); - tm.stop("Run"); - - std::vector stats; - bool has_deadlock = false; - for (unsigned i = 0; i < sys->get_threads(); ++i) - { - has_deadlock |= swarmed[i]->has_deadlock(); - stats.push_back(swarmed[i]->stats()); - } - - for (unsigned i = 0; i < nbth; ++i) - delete swarmed[i]; - - return std::make_tuple(has_deadlock, stats, tm); + return os; } - /// \brief Perform the SCC computation algorithm of bloemen.16.ppopp - template - static std::pair, spot::timer_map> - bloemen(kripke_ptr sys) + SPOT_API std::ostream& operator<<(std::ostream& os, const ec_stats& es) { - spot::timer_map tm; - using algo_name = spot::swarmed_bloemen; - using uf_name = spot::iterable_uf; - - unsigned nbth = sys->get_threads(); - typename uf_name::shared_map map; - - tm.start("Initialisation"); - std::vector swarmed(nbth); - std::vector ufs(nbth); - for (unsigned i = 0; i < nbth; ++i) + for (unsigned i = 0; i < es.name.size(); ++i) { - ufs[i] = new uf_name(map, i); - swarmed[i] = new algo_name(*sys, *ufs[i], i); + os << "---- Thread number:\t" << i << '\n' + << " - Algorithm:\t\t" << es.name[i] << '\n' + << " - Walltime (ms):\t" << es.walltime[i] <<'\n' + << " - States:\t\t" << es.states[i] << '\n' + << " - Transitions:\t" << es.transitions[i] << '\n' + << " - Result:\t\t" << es.value[i] << '\n'; + + os << "CSV: tid,algorithm,walltime,states,transitions,result\n" + << "@th_" << i << ',' << es.name[i] << ',' << es.walltime[i] << ',' + << es.states[i] << ',' << es.transitions[i] << ',' + << es.value[i] << "\n\n"; } - tm.stop("Initialisation"); - - std::mutex iomutex; - std::atomic barrier(true); - std::vector threads(nbth); - for (unsigned i = 0; i < nbth; ++i) - { - threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier] - { -#if defined(unix) || defined(__unix__) || defined(__unix) - { - std::lock_guard iolock(iomutex); - std::cout << "Thread #" << i - << ": on CPU " << sched_getcpu() << '\n'; - } -#endif - - // Wait all threads to be instanciated. - while (barrier) - continue; - swarmed[i]->run(); - }); - -#if defined(unix) || defined(__unix__) || defined(__unix) - // Pins threads to a dedicated core. - cpu_set_t cpuset; - CPU_ZERO(&cpuset); - CPU_SET(i, &cpuset); - int rc = pthread_setaffinity_np(threads[i].native_handle(), - sizeof(cpu_set_t), &cpuset); - if (rc != 0) - { - std::lock_guard iolock(iomutex); - std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n'; - } -#endif - } - - tm.start("Run"); - barrier.store(false); - - for (auto& t : threads) - t.join(); - tm.stop("Run"); - - std::vector stats; - for (unsigned i = 0; i < sys->get_threads(); ++i) - stats.push_back(swarmed[i]->stats()); - - for (unsigned i = 0; i < nbth; ++i) - { - delete swarmed[i]; - delete ufs[i]; - } - return std::make_pair(stats, tm); + return os; } - /// \brief Perform the SCC computation algorithm of bloemen.16.ppopp - /// with emptiness check - template - static std::tuple, - spot::timer_map> - bloemen_ec(kripke_ptr sys, spot::twacube_ptr prop, bool compute_ctrx = false) + /// \brief This function helps to find the output value from a set of threads + /// that may have different values. + SPOT_API const mc_rvalue operator|(const mc_rvalue& lhs, const mc_rvalue& rhs) { - spot::timer_map tm; - using algo_name = spot::swarmed_bloemen_ec; - using uf_name = spot::iterable_uf_ec; + // Handle Deadlocks + if (lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::DEADLOCK) + return mc_rvalue::DEADLOCK; + if (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) + return mc_rvalue::NO_DEADLOCK; + if ((lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) || + (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::DEADLOCK)) + return mc_rvalue::DEADLOCK; - unsigned nbth = sys->get_threads(); - typename uf_name::shared_map map; + // Handle Emptiness + if (lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::EMPTY) + return mc_rvalue::EMPTY; + if (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::NOT_EMPTY) + return mc_rvalue::NOT_EMPTY; + if ((lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::NOT_EMPTY) || + (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::EMPTY)) + return mc_rvalue::EMPTY; - tm.start("Initialisation"); - std::vector swarmed(nbth); - std::vector ufs(nbth); - std::atomic stop(false); - for (unsigned i = 0; i < nbth; ++i) - { - ufs[i] = new uf_name(map, i); - swarmed[i] = new algo_name(*sys, prop, *ufs[i], i, stop); - } - tm.stop("Initialisation"); + // Handle Failure / Success + if (lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::FAILURE) + return mc_rvalue::FAILURE; + if (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::SUCCESS) + return mc_rvalue::SUCCESS; + if ((lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::SUCCESS) || + (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::FAILURE)) + return mc_rvalue::FAILURE; - std::mutex iomutex; - std::atomic barrier(true); - std::vector threads(nbth); - for (unsigned i = 0; i < nbth; ++i) - { - threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier] - { -#if defined(unix) || defined(__unix__) || defined(__unix) - { - std::lock_guard iolock(iomutex); - std::cout << "Thread #" << i - << ": on CPU " << sched_getcpu() << '\n'; - } -#endif - - // Wait all threads to be instanciated. - while (barrier) - continue; - swarmed[i]->run(); - }); - -#if defined(unix) || defined(__unix__) || defined(__unix) - // Pins threads to a dedicated core. - cpu_set_t cpuset; - CPU_ZERO(&cpuset); - CPU_SET(i, &cpuset); - int rc = pthread_setaffinity_np(threads[i].native_handle(), - sizeof(cpu_set_t), &cpuset); - if (rc != 0) - { - std::lock_guard iolock(iomutex); - std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n'; - } -#endif - } - - tm.start("Run"); - barrier.store(false); - - for (auto& t : threads) - t.join(); - tm.stop("Run"); - - std::string trace; - std::vector stats; - bool is_empty = true; - for (unsigned i = 0; i < sys->get_threads(); ++i) - { - if (!swarmed[i]->is_empty()) - { - is_empty = false; - if (compute_ctrx) - trace = swarmed[i]->trace(); - } - - stats.push_back(swarmed[i]->stats()); - } - - for (unsigned i = 0; i < nbth; ++i) - { - delete swarmed[i]; - delete ufs[i]; - } - return std::make_tuple(is_empty, trace, stats, tm); - } - - /// \brief CNDFS - template - static std::tuple, - spot::timer_map> - cndfs(kripke_ptr sys, twacube_ptr prop, bool compute_ctrx = false) - { - spot::timer_map tm; - using algo_name = spot::swarmed_cndfs; - - unsigned nbth = sys->get_threads(); - typename algo_name::shared_map map; - std::atomic stop(false); - - tm.start("Initialisation"); - std::vector swarmed(nbth); - for (unsigned i = 0; i < nbth; ++i) - swarmed[i] = new algo_name(*sys, prop, map, i, stop); - tm.stop("Initialisation"); - - std::mutex iomutex; - std::atomic barrier(true); - std::vector threads(nbth); - for (unsigned i = 0; i < nbth; ++i) - { - threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier] - { -#if defined(unix) || defined(__unix__) || defined(__unix) - { - std::lock_guard iolock(iomutex); - std::cout << "Thread #" << i - << ": on CPU " << sched_getcpu() << '\n'; - } -#endif - - // Wait all threads to be instanciated. - while (barrier) - continue; - swarmed[i]->run(); - }); - -#if defined(unix) || defined(__unix__) || defined(__unix) - // Pins threads to a dedicated core. - cpu_set_t cpuset; - CPU_ZERO(&cpuset); - CPU_SET(i, &cpuset); - int rc = pthread_setaffinity_np(threads[i].native_handle(), - sizeof(cpu_set_t), &cpuset); - if (rc != 0) - { - std::lock_guard iolock(iomutex); - std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n'; - } -#endif - } - - tm.start("Run"); - barrier.store(false); - - for (auto& t : threads) - t.join(); - tm.stop("Run"); - - std::string trace; - std::vector stats; - bool is_empty = true; - for (unsigned i = 0; i < sys->get_threads(); ++i) - { - if (!swarmed[i]->is_empty()) - { - is_empty = false; - if (compute_ctrx) - trace = swarmed[i]->trace(); - } - - stats.push_back(swarmed[i]->stats()); - } - for (unsigned i = 0; i < nbth; ++i) - delete swarmed[i]; - - return std::make_tuple(is_empty, trace, stats, tm); + throw std::runtime_error("Unable to compare these elements!"); } } diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh new file mode 100644 index 000000000..5f9267235 --- /dev/null +++ b/spot/mc/mc_instanciator.hh @@ -0,0 +1,198 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2019, 2020 Laboratoire de Recherche et +// Developpement de l'Epita +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + + template + static SPOT_API ec_stats instanciate(kripke_ptr sys, + spot::twacube_ptr prop = nullptr, + bool trace = false) + { + // FIXME ensure that algo_name contains all methods + + spot::timer_map tm; + std::atomic stop(false); + unsigned nbth = sys->get_threads(); + + typename algo_name::shared_map map; + std::vector swarmed(nbth); + + // The shared structure requires sometime one instance per thread + using struct_name = typename algo_name::shared_struct; + std::vector ss(nbth); + + tm.start("Initialisation"); + for (unsigned i = 0; i < nbth; ++i) + { + ss[i] = algo_name::make_shared_st(map, i); + swarmed[i] = new algo_name(*sys, prop, map, ss[i], i, stop); + } + tm.stop("Initialisation"); + + // Spawn Threads + std::mutex iomutex; + std::atomic barrier(true); + std::vector threads(nbth); + for (unsigned i = 0; i < nbth; ++i) + { + threads[i] = std::thread ([&swarmed, &iomutex, i, &barrier] + { +#if defined(unix) || defined(__unix__) || defined(__unix) + { + std::lock_guard iolock(iomutex); + std::cout << "Thread #" << i + << ": on CPU " << sched_getcpu() << '\n'; + } +#endif + + // Wait all threads to be instanciated. + while (barrier) + continue; + swarmed[i]->run(); + }); + +#if defined(unix) || defined(__unix__) || defined(__unix) + // Pins threads to a dedicated core. + cpu_set_t cpuset; + CPU_ZERO(&cpuset); + CPU_SET(i, &cpuset); + int rc = pthread_setaffinity_np(threads[i].native_handle(), + sizeof(cpu_set_t), &cpuset); + if (rc != 0) + { + std::lock_guard iolock(iomutex); + std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n'; + } +#endif + } + + tm.start("Run"); + barrier.store(false); + + for (auto& t: threads) + t.join(); + tm.stop("Run"); + + // Build the result + ec_stats result; + for (unsigned i = 0; i < nbth; ++i) + { + result.name.emplace_back(swarmed[i]->name()); + result.walltime.emplace_back(swarmed[i]->walltime()); + result.states.emplace_back(swarmed[i]->states()); + result.transitions.emplace_back(swarmed[i]->transitions()); + result.sccs.emplace_back(swarmed[i]->sccs()); + result.value.emplace_back(swarmed[i]->result()); + } + + if (trace) + { + bool go_on = true; + for (unsigned i = 0; i < nbth && go_on; ++i) + { + // Enumerate cases where a trace can be extraced + // Here we use a switch so that adding new algortihm + // with new return status will trigger an error that + // should the be fixed here. + switch (result.value[i]) + { + // A (partial?) trace has been computed + case mc_rvalue::DEADLOCK: + case mc_rvalue::NOT_EMPTY: + result.trace = swarmed[i]->trace(); + go_on = false; + break; + + // Nothing to do here. + case mc_rvalue::NO_DEADLOCK: + case mc_rvalue::EMPTY: + case mc_rvalue::SUCCESS: + case mc_rvalue::FAILURE: + break; + } + } + } + + for (unsigned i = 0; i < nbth; ++i) + { + delete swarmed[i]; + delete ss[i]; + } + + return result; + } + + template + static ec_stats ec_instanciator(const mc_algorithm algo, kripke_ptr sys, + spot::twacube_ptr prop = nullptr, + bool trace = false) + { + if (algo == mc_algorithm::BLOEMEN_EC || algo == mc_algorithm::CNDFS || + algo == mc_algorithm::SWARMING) + { + SPOT_ASSERT(prop != nullptr); + SPOT_ASSERT(sys->get_ap().size() == prop->get_ap().size()); + for (unsigned int i = 0; i < sys->get_ap().size(); ++i) + SPOT_ASSERT(sys->get_ap()[i].compare(prop->get_ap()[i]) == 0); + } + + switch (algo) + { + case mc_algorithm::BLOEMEN_SCC: + return instanciate, + kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); + + case mc_algorithm::BLOEMEN_EC: + return + instanciate, + kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); + + case mc_algorithm::CNDFS: + return instanciate, + kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); + + case mc_algorithm::DEADLOCK: + return instanciate, + kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); + + case mc_algorithm::SWARMING: + return instanciate, + kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); + } + } +} diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh index 1baa895fe..7e708f87e 100644 --- a/spot/mc/utils.hh +++ b/spot/mc/utils.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et +// Copyright (C) 2016, 2020 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -97,6 +97,212 @@ namespace spot std::unordered_map reverse_binder_; }; + // FIXME: should be merge into the next algorithm. + /// \brief This class explores (with a DFS) a product between a + /// system and a twa. This exploration is performed on-the-fly. + /// Since this exploration aims to be a generic we need to define + /// hooks to the various emptiness checks. + /// Actually, we use "mixins templates" in order to efficiently + /// call emptiness check procedure. This means that we add + /// a template \a EmptinessCheck that will be called though + /// four functions: + /// - setup: called before any operation + /// - push: called for every new state + /// - pop: called every time a state leave the DFS stack + /// - update: called for every closing edge + /// - trace: must return a counterexample (if exists) + /// + /// The other template parameters allows to consider any kind + /// of state (and so any kind of kripke structures). + template + class SPOT_API intersect + { + public: + intersect(const intersect& i) = default; + + intersect(kripkecube& sys, + twacube_ptr twa, unsigned tid, bool& stop): + sys_(sys), twa_(twa), tid_(tid), stop_(stop) + { + static_assert(spot::is_a_kripkecube_ptr::value, + "error: does not match the kripkecube requirements"); + map.reserve(2000000); + todo.reserve(100000); + } + + ~intersect() + { + map.clear(); + } + + /// \brief In order to implement "mixin paradigm", we + /// must be abble to access the acual definition of + /// the emptiness check that, in turn, has to access + /// local variables. + EmptinessCheck& self() + { + return static_cast(*this); + } + + /// \brief The main function that will perform the + /// product on-the-fly and call the emptiness check + /// when necessary. + bool run() + { + self().setup(); + product_state initial = {sys_.initial(tid_), twa_->get_initial()}; + if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, {}))) + { + todo.push_back({initial, sys_.succ(initial.st_kripke, tid_), + twa_->succ(initial.st_prop)}); + + // Not going further! It's a product with a single state. + if (todo.back().it_prop->done()) + return false; + + forward_iterators(sys_, twa_, todo.back().it_kripke, + todo.back().it_prop, true, 0); + map[initial] = ++dfs_number; + } + while (!todo.empty() && !stop_) + { + // Check the kripke is enough since it's the outer loop. More + // details in forward_iterators. + if (todo.back().it_kripke->done()) + { + bool is_init = todo.size() == 1; + auto newtop = is_init? todo.back().st: todo[todo.size() -2].st; + if (SPOT_LIKELY(self().pop_state(todo.back().st, + map[todo.back().st], + is_init, + newtop, + map[newtop]))) + { + sys_.recycle(todo.back().it_kripke, tid_); + // FIXME a local storage for twacube iterator? + todo.pop_back(); + if (SPOT_UNLIKELY(self().counterexample_found())) + return true; + } + } + else + { + ++transitions; + product_state dst = { + todo.back().it_kripke->state(), + twa_->trans_storage(todo.back().it_prop, tid_).dst + }; + auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_; + forward_iterators(sys_, twa_, todo.back().it_kripke, + todo.back().it_prop, false, 0); + auto it = map.find(dst); + if (it == map.end()) + { + if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc))) + { + map[dst] = ++dfs_number; + todo.push_back({dst, sys_.succ(dst.st_kripke, tid_), + twa_->succ(dst.st_prop)}); + forward_iterators(sys_, twa_, todo.back().it_kripke, + todo.back().it_prop, true, 0); + } + } + else if (SPOT_UNLIKELY(self().update(todo.back().st, + dfs_number, + dst, map[dst], acc))) + return true; + } + } + return false; + } + + unsigned int states() + { + return dfs_number; + } + + unsigned int trans() + { + return transitions; + } + + std::string counterexample() + { + return self().trace(); + } + + public: + struct product_state + { + State st_kripke; + unsigned st_prop; + }; + + struct product_state_equal + { + bool + operator()(const product_state lhs, + const product_state rhs) const + { + StateEqual equal; + return (lhs.st_prop == rhs.st_prop) && + equal(lhs.st_kripke, rhs.st_kripke); + } + }; + + struct product_state_hash + { + size_t + operator()(const product_state that) const noexcept + { + // FIXME! wang32_hash(that.st_prop) could have + // been pre-calculated! + StateHash hasher; + return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); + } + }; + + struct todo_element + { + product_state st; + SuccIterator* it_kripke; + std::shared_ptr it_prop; + }; + kripkecube& sys_; + twacube_ptr twa_; + std::vector todo; + typedef std::unordered_map visited_map; + visited_map map; + unsigned int dfs_number = 0; + unsigned int transitions = 0; + unsigned tid_; + bool& stop_; // Do not need to be atomic. + }; + + + + + + + + + + + + + + + + + + + template #include -#include +#include #include #include #include @@ -40,6 +40,7 @@ #include #include +#include #include #include #include @@ -70,13 +71,10 @@ struct mc_options_ char* dead_ap = nullptr; bool use_timer = false; unsigned compress = 0; - bool kripke_output = false; unsigned nb_threads = 1; bool csv = false; - bool has_deadlock = false; - bool bloemen = false; - bool bloemen_ec = false; - bool cndfs = false; + spot::mc_algorithm algorithm = spot::mc_algorithm::BLOEMEN_EC; + bool force_parallel = false; } mc_options; @@ -90,16 +88,20 @@ parse_opt_finput(int key, char* arg, struct argp_state*) mc_options.csv = true; break; case 'B': - mc_options.bloemen_ec = true; + mc_options.algorithm = spot::mc_algorithm::BLOEMEN_EC; + mc_options.force_parallel = true; break; case 'b': - mc_options.bloemen = true; + // FIXME Differenciate bloemen and bloemen_ec: -b/-B is not enough + mc_options.algorithm = spot::mc_algorithm::BLOEMEN_SCC; + mc_options.force_parallel = true; break; case 'c': mc_options.compute_counterexample = true; break; case 'C': - mc_options.cndfs = true; + mc_options.algorithm = spot::mc_algorithm::CNDFS; + mc_options.force_parallel = true; break; case 'd': if (strcmp(arg, "model") == 0) @@ -122,17 +124,16 @@ parse_opt_finput(int key, char* arg, struct argp_state*) mc_options.formula = arg; break; case 'h': - mc_options.has_deadlock = true; + mc_options.algorithm = spot::mc_algorithm::DEADLOCK; + mc_options.force_parallel = true; mc_options.selfloopize = false; break; - case 'k': - mc_options.kripke_output = true; - break; case 'm': mc_options.model = arg; break; case 'p': mc_options.nb_threads = to_unsigned(arg, "-p/--parallel"); + mc_options.force_parallel = true; break; case 's': mc_options.dead_ap = arg; @@ -140,6 +141,10 @@ parse_opt_finput(int key, char* arg, struct argp_state*) case 't': mc_options.use_timer = true; break; + case 'w': + mc_options.algorithm = spot::mc_algorithm::SWARMING; + mc_options.force_parallel = true; + break; case 'z': mc_options.compress = to_unsigned(arg, "-z/--compress"); break; @@ -160,35 +165,41 @@ static const argp_option options[] = // ------------------------------------------------------------ { nullptr, 0, nullptr, 0, "Process options:", 2 }, { "bloemen-ec", 'B', nullptr, 0, - "run the SCC computation of Bloemen et al. (PPOPP'16) with EC", 0}, + "run the emptiness-check of Bloemen et al. (HVC'16). Return 1 " + "if a counterexample is found.", 0}, { "bloemen", 'b', nullptr, 0, - "run the SCC computation of Bloemen et al. (PPOPP'16)", 0 }, + "run the SCC computation of Bloemen et al. (PPOPP'16). Return 1 " + "if a counterexample is found.", 0 }, { "cndfs", 'C', nullptr, 0, - "run CNDFS", 0 }, + "run the emptiness check of Evangelista et al. (ATVA'12). Return 1 " + "if a counterexample is found.", 0 }, { "counterexample", 'c', nullptr, 0, "compute an accepting counterexample (if it exists)", 0 }, - { "is-empty", 'e', nullptr, 0, - "check if the model meets its specification. " - "Return 1 if a counterexample is found." - , 0 }, { "has-deadlock", 'h', nullptr, 0, "check if the model has a deadlock. " "Return 1 if the model contains a deadlock." , 0 }, + { "is-empty", 'e', nullptr, 0, + "check if the model meets its specification. Uses Cou99 in sequential " + "and bloemen-ec in pallel (option -p). Return 1 if a counterexample " + "is found." + , 0 }, { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 }, { "selfloopize", 's', "STRING", 0, "use STRING as property for marking deadlock " "states (by default selfloopize is activated with STRING='true')", 0 }, + { "swarming", 'w', nullptr, 0, + "run the technique of of Holzmann et al. (IEEE'11) with the emptiness-" + "check of Renault et al. (LPAR'13). Returns 1 if a counterexample " + "is found.", 0 }, { "timer", 't', nullptr, 0, "time the different phases of the execution", 0 }, // ------------------------------------------------------------ { nullptr, 0, nullptr, 0, "Output options:", 3 }, - { "dot", 'd', "[model|product|formula]", 0, - "output the associated automaton in dot format", 0 }, - { "kripke", 'k', nullptr, 0, - "output the associated automaton in (internal) kripke format", 0 }, { "csv", CSV, nullptr, 0, "output a CSV containing interesting values", 0 }, + { "dot", 'd', "[model|product|formula]", 0, + "output the associated automaton in dot format", 0 }, // ------------------------------------------------------------ { nullptr, 0, nullptr, 0, "Optimization options:", 4 }, { "compress", 'z', "INT", 0, "specify the level of compression\n" @@ -210,16 +221,14 @@ const struct argp_child children[] = { nullptr, 0, nullptr, 0 } }; -static std::string split_filename(const std::string& str) { +static std::string split_filename(const std::string& str) { unsigned found = str.find_last_of("/"); return str.substr(found+1); } static int checked_main() { - spot::default_environment& env = - spot::default_environment::instance(); - + spot::default_environment& env = spot::default_environment::instance(); spot::atomic_prop_set ap; auto dict = spot::make_bdd_dict(); spot::const_kripke_ptr model = nullptr; @@ -243,7 +252,6 @@ static int checked_main() deadf = env.require(mc_options.dead_ap); } - if (mc_options.formula != nullptr) { tm.start("parsing formula"); @@ -299,20 +307,14 @@ static int checked_main() spot::print_dot(std::cout, model); tm.stop("dot output"); } - if (mc_options.kripke_output) - { - tm.start("kripke output"); - spot::print_hoa(std::cout, model); - tm.stop("kripke output"); - } } - if (mc_options.nb_threads == 1 && + if (mc_options.force_parallel == false && mc_options.formula != nullptr && - mc_options.model != nullptr && - !mc_options.bloemen_ec && - !mc_options.cndfs) + mc_options.model != nullptr) { + std::cout << "Warning : using sequential algorithms (BDD-based)\n\n"; + product = spot::otf_product(model, prop); if (mc_options.is_empty) @@ -419,230 +421,45 @@ static int checked_main() tm.stop("dot output"); } } - - if (mc_options.nb_threads != 1 && - mc_options.formula != nullptr && - mc_options.model != nullptr && - !mc_options.bloemen_ec && - !mc_options.cndfs) + // FIXME : handle here swarming + else if (mc_options.force_parallel && mc_options.model != nullptr) { - unsigned int hc = std::thread::hardware_concurrency(); - if (mc_options.nb_threads > hc) - std::cerr << "Warning: you require " << mc_options.nb_threads - << " threads, but your computer only support " << hc - << ". This could slow down parallel algorithms.\n"; + std::cout << "Warning : using parallel algorithms (CUBE-based)\n\n"; - tm.start("twa to twacube"); - auto propcube = spot::twa_to_twacube(prop); - tm.stop("twa to twacube"); - - tm.start("load kripkecube"); - spot::ltsmin_kripkecube_ptr modelcube = nullptr; - try - { - modelcube = spot::ltsmin_model::load(mc_options.model) - .kripkecube(propcube->get_ap(), deadf, mc_options.compress, - mc_options.nb_threads); - } - catch (const std::runtime_error& e) - { - std::cerr << e.what() << '\n'; - } - tm.stop("load kripkecube"); - - int memused = spot::memusage(); - tm.start("emptiness check"); - auto res = spot::modelcheck - (modelcube, propcube, mc_options.compute_counterexample); - tm.stop("emptiness check"); - memused = spot::memusage() - memused; - - if (!modelcube) + if (mc_options.dot_output & DOT_PRODUCT) { + std::cerr << "\nERROR: Parallel algorithm doesn't support DOT" + " output for the synchronous product.\n" + " Please consider removing '-p' option\n"; exit_code = 2; goto safe_exit; } - // Display statistics - unsigned smallest = 0; - for (unsigned i = 0; i < std::get<2>(res).size(); ++i) - { - if (std::get<2>(res)[i].states < std::get<2>(res)[smallest].states) - smallest = i; - - std::cout << "\n---- Thread number : " << i << '\n'; - std::cout << std::get<2>(res)[i].states << " unique states visited\n"; - std::cout << std::get<2>(res)[i].instack_sccs - << " strongly connected components in search stack\n"; - std::cout << std::get<2>(res)[i].transitions - << " transitions explored\n"; - std::cout << std::get<2>(res)[i].instack_item - << " items max in DFS search stack\n"; - - // FIXME: produce walltime for each threads. - if (mc_options.csv) - { - std::cout << "Find following the csv: " - << "thread_id,walltimems,type," - << "states,transitions\n"; - std::cout << "@th_" << i << ',' - << tm.timer("emptiness check").walltime() << ',' - << (!std::get<2>(res)[i].is_empty ? - "EMPTY," : "NONEMPTY,") - << std::get<2>(res)[i].states << ',' - << std::get<2>(res)[i].transitions - << std::endl; - } - } - - - if (mc_options.csv) - { - std::cout << "\nSummary :\n"; - if (!std::get<0>(res)) - std::cout << "no accepting run found\n"; - else if (!mc_options.compute_counterexample) - { - std::cout << "an accepting run exists " - << "(use -c to print it)" << std::endl; - exit_code = 1; - } - else - std::cout << "an accepting run exists!\n" << std::get<1>(res) - << '\n'; - - std::cout << "Find following the csv: " - << "model,formula,walltimems,memused,type" - << "states,transitions\n"; - - std::cout << '#' - << split_filename(mc_options.model) - << ',' - << mc_options.formula << ',' - << tm.timer("emptiness check").walltime() << ',' - << memused << ',' - << (!std::get<0>(res) ? "EMPTY," : "NONEMPTY,") - << std::get<2>(res)[smallest].states << ',' - << std::get<2>(res)[smallest].transitions - << '\n'; - } - } - - - if (mc_options.has_deadlock && mc_options.model != nullptr) - { - assert(!mc_options.selfloopize); - unsigned int hc = std::thread::hardware_concurrency(); - if (mc_options.nb_threads > hc) - std::cerr << "Warning: you require " << mc_options.nb_threads - << " threads, but your computer only support " << hc - << ". This could slow down parallel algorithms.\n"; - - tm.start("load kripkecube"); - spot::ltsmin_kripkecube_ptr modelcube = nullptr; - try - { - modelcube = spot::ltsmin_model::load(mc_options.model) - .kripkecube({}, spot::formula::ff(), mc_options.compress, - mc_options.nb_threads); - } - catch (const std::runtime_error& e) - { - std::cerr << e.what() << '\n'; - } - tm.stop("load kripkecube"); - - int memused = spot::memusage(); - tm.start("deadlock check"); - auto res = spot::has_deadlock(modelcube); - tm.stop("deadlock check"); - memused = spot::memusage() - memused; - - if (!modelcube) + if (prop == nullptr && + (mc_options.algorithm == spot::mc_algorithm::CNDFS || + mc_options.algorithm == spot::mc_algorithm::BLOEMEN_EC || + mc_options.algorithm == spot::mc_algorithm::SWARMING)) { + std::cerr << "\nERROR: Algorithm " << mc_options.algorithm + << " requires to provide a formula (--formula)\n"; exit_code = 2; goto safe_exit; } - // Display statistics - unsigned smallest = 0; - for (unsigned i = 0; i < std::get<1>(res).size(); ++i) - { - if (std::get<1>(res)[i].states < std::get<1>(res)[smallest].states) - smallest = i; - - std::cout << "\n---- Thread number : " << i << '\n'; - std::cout << std::get<1>(res)[i].states << " unique states visited\n"; - std::cout << std::get<1>(res)[i].transitions - << " transitions explored\n"; - std::cout << std::get<1>(res)[i].instack_dfs - << " items max in DFS search stack\n"; - std::cout << std::get<1>(res)[i].walltime - << " milliseconds\n"; - - if (mc_options.csv) - { - std::cout << "Find following the csv: " - << "thread_id,walltimems,type," - << "states,transitions\n"; - std::cout << "@th_" << i << ',' - << std::get<1>(res)[i].walltime << ',' - << (std::get<1>(res)[i].has_deadlock ? - "DEADLOCK," : "NO-DEADLOCK,") - << std::get<1>(res)[i].states << ',' - << std::get<1>(res)[i].transitions - << std::endl; - } - } - - if (mc_options.csv) - { - std::cout << "\nSummary :\n"; - if (!std::get<0>(res)) - std::cout << "No no deadlock found!\n"; - else - { - std::cout << "A deadlock exists!\n"; - exit_code = 1; - } - - std::cout << "Find following the csv: " - << "model,walltimems,memused,type," - << "states,transitions\n"; - - std::cout << '#' - << split_filename(mc_options.model) - << ',' - << tm.timer("deadlock check").walltime() << ',' - << memused << ',' - << (std::get<0>(res) ? "DEADLOCK," : "NO-DEADLOCK,") - << std::get<1>(res)[smallest].states << ',' - << std::get<1>(res)[smallest].transitions - << '\n'; - } - } - - if (mc_options.cndfs && - mc_options.model != nullptr && mc_options.formula != nullptr) - { unsigned int hc = std::thread::hardware_concurrency(); if (mc_options.nb_threads > hc) std::cerr << "Warning: you require " << mc_options.nb_threads << " threads, but your computer only support " << hc << ". This could slow down parallel algorithms.\n"; - // Only support Single Acceptance Conditions - tm.start("degeneralize"); - auto prop_degen = spot::degeneralize_tba(prop); - tm.stop("degeneralize"); + auto prop_degen = prop; + if (mc_options.algorithm == spot::mc_algorithm::CNDFS) + { + // Only support Single Acceptance Conditions + tm.start("degeneralize"); + prop_degen = spot::degeneralize_tba(prop); + tm.stop("degeneralize"); + } tm.start("twa to twacube"); auto propcube = spot::twa_to_twacube(prop_degen); @@ -652,9 +469,12 @@ static int checked_main() spot::ltsmin_kripkecube_ptr modelcube = nullptr; try { + std::vector aps = {}; + if (propcube != nullptr) + aps = propcube->get_ap(); + modelcube = spot::ltsmin_model::load(mc_options.model) - .kripkecube(propcube->get_ap(), deadf, mc_options.compress, - mc_options.nb_threads); + .kripkecube(aps, deadf, mc_options.compress, mc_options.nb_threads); } catch (const std::runtime_error& e) { @@ -663,14 +483,16 @@ static int checked_main() tm.stop("load kripkecube"); int memused = spot::memusage(); - tm.start("cndfs"); - auto res = spot::cndfs - (modelcube, propcube, mc_options.compute_counterexample); - tm.stop("cndfs"); + tm.start("exploration"); + + auto result = + spot::ec_instanciator + (mc_options.algorithm, modelcube, propcube, + mc_options.compute_counterexample); + + tm.stop("exploration"); memused = spot::memusage() - memused; if (!modelcube) @@ -680,41 +502,22 @@ static int checked_main() } // Display statistics - unsigned smallest = 0; - for (unsigned i = 0; i < std::get<2>(res).size(); ++i) - { - if (std::get<2>(res)[i].states < std::get<2>(res)[smallest].states) - smallest = i; + std::cout << result << '\n'; + std::cout << memused << " pages allocated for " + << mc_options.algorithm << '\n'; - std::cout << "\n---- Thread number : " << i << '\n'; - std::cout << std::get<2>(res)[i].states << " unique states visited\n"; - std::cout << std::get<2>(res)[i].transitions - << " transitions explored\n"; - std::cout << std::get<2>(res)[i].instack_dfs - << " items max in DFS search stack\n"; - std::cout << std::get<2>(res)[i].walltime - << " milliseconds\n"; - - if (mc_options.csv) - { - std::cout << "Find following the csv: " - << "thread_id,walltimems,type," - << "states,transitions\n"; - std::cout << "@th_" << i << ',' - << std::get<2>(res)[i].walltime << ',' - << (std::get<2>(res)[i].is_empty ? - "EMPTY," : "NONEMPTY,") - << std::get<2>(res)[i].states << ',' - << std::get<2>(res)[i].transitions - << std::endl; - } - } if (mc_options.csv) { std::cout << "\nSummary :\n"; - if (std::get<0>(res)) - std::cout << "no accepting run found\n"; + auto rval = result.value[0]; + std::for_each(result.value.rbegin(), result.value.rend(), + [&](spot::mc_rvalue n) { rval = rval | n; }); + + if (rval == spot::mc_rvalue::NO_DEADLOCK || + rval == spot::mc_rvalue::EMPTY || + rval == spot::mc_rvalue::SUCCESS) + std::cout << "no accepting run / counterexample found\n"; else if (!mc_options.compute_counterexample) { std::cout << "an accepting run exists " @@ -722,241 +525,33 @@ static int checked_main() exit_code = 1; } else - std::cout << "an accepting run exists\n" - << std::get<1>(res) << '\n'; + std::cout << "an accepting run exists\n" << result.trace << '\n'; + + + // Grab The informations to display into the CSV + // FIXME: The CSV can be inconsistent since it may return + // time of one thread and SCC of another. + auto walltime = std::min_element(result.walltime.rbegin(), + result.walltime.rend()); + auto states = std::min_element(result.states.rbegin(), + result.states.rend()); + auto trans = std::min_element(result.transitions.rbegin(), + result.transitions.rend()); + auto sccs = std::max_element(result.sccs.rbegin(), + result.sccs.rend()); std::cout << "Find following the csv: " - << "model,walltimems,memused,type," - << "states,transitions\n"; - + << "model,formula,walltimems,memused,type," + << "states,transitions,sccs\n"; std::cout << '#' - << split_filename(mc_options.model) - << ',' - << tm.timer("cndfs").walltime() << ',' - << memused << ',' - << (std::get<0>(res) ? "EMPTY," : "NONEMPTY,") - << std::get<2>(res)[smallest].states << ',' - << std::get<2>(res)[smallest].transitions - << '\n'; + << split_filename(mc_options.model) << ',' + << mc_options.formula << ',' + << *walltime << ',' << memused << ',' + << rval << ',' << *states << ',' << *trans << ',' + << *sccs << '\n'; } } - if (mc_options.bloemen && mc_options.model != nullptr) - { - unsigned int hc = std::thread::hardware_concurrency(); - if (mc_options.nb_threads > hc) - std::cerr << "Warning: you require " << mc_options.nb_threads - << " threads, but your computer only support " << hc - << ". This could slow down parallel algorithms.\n"; - - tm.start("load kripkecube"); - spot::ltsmin_kripkecube_ptr modelcube = nullptr; - try - { - modelcube = spot::ltsmin_model::load(mc_options.model) - .kripkecube({}, deadf, mc_options.compress, - mc_options.nb_threads); - } - catch (const std::runtime_error& e) - { - std::cerr << e.what() << '\n'; - } - tm.stop("load kripkecube"); - - int memused = spot::memusage(); - tm.start("bloemen"); - auto res = spot::bloemen(modelcube); - tm.stop("bloemen"); - memused = spot::memusage() - memused; - - if (!modelcube) - { - exit_code = 2; - goto safe_exit; - } - - // Display statistics - unsigned sccs = 0; - unsigned st = 0; - unsigned tr = 0; - unsigned inserted = 0; - for (unsigned i = 0; i < res.first.size(); ++i) - { - std::cout << "\n---- Thread number : " << i << '\n'; - std::cout << res.first[i].states << " unique states visited\n"; - std::cout << res.first[i].inserted << " unique states inserted\n"; - std::cout << res.first[i].transitions - << " transitions explored\n"; - std::cout << res.first[i].sccs << " sccs found\n"; - std::cout << res.first[i].walltime - << " milliseconds\n"; - - sccs += res.first[i].sccs; - st += res.first[i].states; - tr += res.first[i].transitions; - inserted += res.first[i].inserted; - - if (mc_options.csv) - { - std::cout << "Find following the csv: " - << "thread_id,walltimems," - << "states,transitions,sccs\n"; - std::cout << "@th_" << i << ',' - << res.first[i].walltime << ',' - << res.first[i].states << ',' - << res.first[i].inserted << ',' - << res.first[i].transitions << ',' - << res.first[i].sccs - << std::endl; - } - } - - if (mc_options.csv) - { - std::cout << "\nSummary :\n"; - std::cout << "Find following the csv: " - << "model,walltimems,memused," - << "inserted_states," - << "cumulated_states,cumulated_transitions," - << "cumulated_sccs\n"; - - std::cout << '#' - << split_filename(mc_options.model) - << ',' - << tm.timer("bloemen").walltime() << ',' - << memused << ',' - << inserted << ',' - << st << ',' - << tr << ',' - << sccs - << '\n'; - } - } - - if (mc_options.bloemen_ec - && mc_options.model != nullptr && mc_options.formula != nullptr) - { - unsigned int hc = std::thread::hardware_concurrency(); - if (mc_options.nb_threads > hc) - std::cerr << "Warning: you require " << mc_options.nb_threads - << " threads, but your computer only support " << hc - << ". This could slow down parallel algorithms.\n"; - - tm.start("twa to twacube"); - auto propcube = spot::twa_to_twacube(prop); - tm.stop("twa to twacube"); - - tm.start("load kripkecube"); - spot::ltsmin_kripkecube_ptr modelcube = nullptr; - try - { - modelcube = spot::ltsmin_model::load(mc_options.model) - .kripkecube(propcube->get_ap(), deadf, mc_options.compress, - mc_options.nb_threads); - } - catch (const std::runtime_error& e) - { - std::cerr << e.what() << '\n'; - } - tm.stop("load kripkecube"); - - int memused = spot::memusage(); - tm.start("bloemen emptiness check"); - auto res = spot::bloemen_ec - (modelcube, propcube); - tm.stop("bloemen emptiness check"); - memused = spot::memusage() - memused; - - if (!modelcube) - { - exit_code = 2; - goto safe_exit; - } - - // Display statistics - unsigned sccs = 0; - unsigned st = 0; - unsigned tr = 0; - unsigned inserted = 0; - for (unsigned i = 0; i < std::get<2>(res).size(); ++i) - { - std::cout << "\n---- Thread number : " << i << '\n'; - std::cout << std::get<2>(res)[i].states - << " unique states visited\n"; - std::cout << std::get<2>(res)[i].inserted - << " unique states inserted\n"; - std::cout << std::get<2>(res)[i].transitions - << " transitions explored\n"; - std::cout << std::get<2>(res)[i].sccs << " sccs found\n"; - std::cout << std::get<2>(res)[i].walltime - << " milliseconds\n"; - - sccs += std::get<2>(res)[i].sccs; - st += std::get<2>(res)[i].states; - tr += std::get<2>(res)[i].transitions; - inserted += std::get<2>(res)[i].inserted; - - if (mc_options.csv) - { - std::cout << "Find following the csv: " - << "thread_id,walltimems,type," - << "states,transitions,sccs\n"; - std::cout << "@th_" << i << ',' - << std::get<2>(res)[i].walltime << ',' - << (std::get<2>(res)[i].is_empty ? - "EMPTY," : "NONEMPTY,") - << std::get<2>(res)[i].states << ',' - << std::get<2>(res)[i].inserted << ',' - << std::get<2>(res)[i].transitions << ',' - << std::get<2>(res)[i].sccs - << std::endl; - } - } - - if (mc_options.csv) - { - std::cout << "\nSummary :\n"; - if (std::get<0>(res)) - std::cout << "no accepting run found\n"; - else if (!mc_options.compute_counterexample) - { - std::cout << "an accepting run exists " - << "(use -c to print it)" << std::endl; - exit_code = 1; - } - else - std::cout << "an accepting run exists\n" - << std::get<1>(res) << '\n'; - - - std::cout << "Find following the csv: " - << "model,walltimems,memused," - << "type,inserted_states," - << "cumulated_states,cumulated_transitions," - << "cumulated_sccs\n"; - - std::cout << '#' - << split_filename(mc_options.model) - << ',' - << tm.timer("bloemen emptiness check").walltime() << ',' - << memused << ',' - << (std::get<0>(res) ? "EMPTY," : "NONEMPTY,") - << inserted << ',' - << st << ',' - << tr << ',' - << sccs - << '\n'; - } - } - safe_exit: if (mc_options.use_timer) tm.print(std::cout); @@ -964,7 +559,6 @@ static int checked_main() return exit_code; } - int main(int argc, char** argv) {