diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index 693d2527a..73781eb32 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -21,7 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) mcdir = $(pkgincludedir)/mc -mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh mc.hh +mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\ + mc.hh deadlock.hh noinst_LTLIBRARIES = libmc.la diff --git a/spot/mc/deadlock.hh b/spot/mc/deadlock.hh new file mode 100644 index 000000000..0c951fa4b --- /dev/null +++ b/spot/mc/deadlock.hh @@ -0,0 +1,257 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015, 2016, 2017 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 + +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 + { + /// \brief Describes the status of a state + enum st_status + { + UNKNOWN = 1, // First time this state is discoverd by this thread + OPEN = 2, // The state is currently processed by this thread + CLOSED = 4, // All the successors of this state have been visited + }; + + /// \brief Describes the structure of a shared state + struct deadlock_pair + { + State st; ///< \brief the effective state + int* colors; ///< \brief the colors (one per thread) + }; + + /// \brief The haser for the previous state. + struct pair_hasher + { + pair_hasher(const deadlock_pair&) + { } + + pair_hasher() = default; + + brick::hash::hash128_t + hash(const deadlock_pair& lhs) const + { + StateHash hash; + // Not modulo 31 according to brick::hashset specifications. + unsigned u = hash(lhs.st) % (1<<30); + return {u, u}; + } + + bool equal(const deadlock_pair& lhs, + const deadlock_pair& rhs) const + { + StateEqual equal; + return equal(lhs.st, rhs.st); + } + }; + + public: + + ///< \brief Shortcut to ease shared map manipulation + using shared_map = brick::hashset::FastConcurrent ; + + swarmed_deadlock(kripkecube& sys, + shared_map& map, unsigned tid, std::atomic& stop): + sys_(sys), tid_(tid), map_(map), + nb_th_(std::thread::hardware_concurrency()), + p_(sizeof(int)*std::thread::hardware_concurrency()), stop_(stop) + { + SPOT_ASSERT(is_a_kripkecube(sys)); + } + + virtual ~swarmed_deadlock() + { + } + + void setup() + { + tm_.start("DFS thread " + std::to_string(tid_)); + } + + bool push(State s) + { + // Prepare data for a newer allocation + int* ref = (int*) p_.allocate(); + for (unsigned i = 0; i < nb_th_; ++i) + ref[i] = UNKNOWN; + + // Try to insert the new state in the shared map. + auto it = map_.insert({s, ref}); + bool b = it.isnew(); + + // Insertion failed, delete element + // FIXME Should we add a local cache to avoid useless allocations? + if (!b) + p_.deallocate(ref); + + // The state has been mark dead by another thread + for (unsigned i = 0; !b && i < nb_th_; ++i) + if (it->colors[i] == static_cast(CLOSED)) + return false; + + // The state has already been visited by the current thread + if (it->colors[tid_] == static_cast(OPEN)) + return false; + + // Keep a ptr over the array of colors + refs_.push_back(it->colors); + + // Mark state as visited. + it->colors[tid_] = OPEN; + ++states_; + return true; + } + + bool pop() + { + // Track maximum dfs size + dfs_ = todo_.size() > dfs_ ? todo_.size() : dfs_; + + // Don't avoid pop but modify the status of the state + // during backtrack + refs_.back()[tid_] = CLOSED; + refs_.pop_back(); + return true; + } + + void finalize() + { + stop_ = true; + tm_.stop("DFS thread " + std::to_string(tid_)); + } + + unsigned states() + { + return states_; + } + + unsigned transitions() + { + 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() + { + return {states(), transitions(), dfs_, has_deadlock(), walltime()}; + } + + private: + 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 + 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_; ///< \brief State Allocator + bool deadlock_ = false; ///< \brief Deadlock detected? + std::atomic& stop_; ///< \brief Stop-the-world boolean + /// \brief Stack that grows according to the todo stack. It avoid multiple + /// concurent access to the shared map. + std::vector refs_; + }; +} diff --git a/spot/mc/mc.hh b/spot/mc/mc.hh index 2a284ac94..85ce4aa1a 100644 --- a/spot/mc/mc.hh +++ b/spot/mc/mc.hh @@ -19,13 +19,16 @@ #pragma once +#include #include #include #include #include #include #include +#include #include +#include namespace spot { @@ -60,7 +63,7 @@ namespace spot bool has_ctrx = false; std::string trace = ""; - std::vector stats; + std::vector stats; for (unsigned i = 0; i < sys->get_threads(); ++i) { has_ctrx |= ecs[i].counterexample_found(); @@ -71,4 +74,82 @@ namespace spot } return std::make_tuple(has_ctrx, trace, stats); } + + /// \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::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) + { + 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; + 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); + } } diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 521d7340b..1d851cb2e 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -72,6 +72,7 @@ struct mc_options_ bool kripke_output = false; unsigned nb_threads = 1; bool csv = false; + bool has_deadlock = false; } mc_options; @@ -107,6 +108,10 @@ parse_opt_finput(int key, char* arg, struct argp_state*) case 'f': mc_options.formula = arg; break; + case 'h': + mc_options.has_deadlock = true; + mc_options.selfloopize = false; + break; case 'k': mc_options.kripke_output = true; break; @@ -147,6 +152,10 @@ static const argp_option options[] = "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 }, { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 }, { "selfloopize", 's', "STRING", 0, "use STRING as property for marking deadlock " @@ -280,7 +289,6 @@ static int checked_main() } } - if (mc_options.nb_threads == 1 && mc_options.formula != nullptr && mc_options.model != nullptr) @@ -503,6 +511,104 @@ static int checked_main() } } + + 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({}, deadf, mc_options.compress, + mc_options.nb_threads); + } + catch (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) + { + 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'; + } + } + safe_exit: if (mc_options.use_timer) tm.print(std::cout);