Commit 33f30786 authored by Etienne Renault's avatar Etienne Renault

mc: add swarmed deadlock-detection

* spot/mc/Makefile.am, spot/mc/deadlock.hh,
spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
parent 231016b2
......@@ -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
......
// -*- 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <atomic>
#include <chrono>
#include <bricks/brick-hashset>
#include <stdlib.h>
#include <thread>
#include <vector>
#include <spot/misc/common.hh>
#include <spot/kripke/kripke.hh>
#include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
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<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
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 <deadlock_pair,
pair_hasher>;
swarmed_deadlock(kripkecube<State, SuccIterator>& sys,
shared_map& map, unsigned tid, std::atomic<bool>& 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<int>(CLOSED))
return false;
// The state has already been visited by the current thread
if (it->colors[tid_] == static_cast<int>(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<State, SuccIterator>& sys_; ///< \brief The system to check
std::vector<todo__element> 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<bool>& 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<int*> refs_;
};
}
......@@ -19,13 +19,16 @@
#pragma once
#include <functional>
#include <string>
#include <thread>
#include <tuple>
#include <vector>
#include <spot/kripke/kripke.hh>
#include <spot/mc/ec.hh>
#include <spot/mc/deadlock.hh>
#include <spot/misc/common.hh>
#include <spot/misc/timer.hh>
namespace spot
{
......@@ -60,7 +63,7 @@ namespace spot
bool has_ctrx = false;
std::string trace = "";
std::vector<istats> stats;
std::vector<istats> 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<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
static std::tuple<bool, std::vector<deadlock_stats>, spot::timer_map>
has_deadlock(kripke_ptr sys)
{
spot::timer_map tm;
using algo_name = spot::swarmed_deadlock<State, Iterator, Hash, Equal>;
unsigned nbth = sys->get_threads();
typename algo_name::shared_map map;
std::atomic<bool> stop(false);
tm.start("Initialisation");
std::vector<algo_name*> 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<bool> barrier(true);
std::vector<std::thread> 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<std::mutex> 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<std::mutex> 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<deadlock_stats> 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);
}
}
......@@ -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<spot::ltsmin_kripkecube_ptr,
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>(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);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment