Commit b8cbe032 authored by Etienne Renault's avatar Etienne Renault

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.
parent b80d59c2
......@@ -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
......
// -*- 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 <atomic>
#include <chrono>
#include <spot/bricks/brick-hashset>
#include <stdlib.h>
#include <thread>
#include <vector>
#include <utility>
#include <spot/misc/common.hh>
#include <spot/bricks/brick-hashset>
#include <spot/kripke/kripke.hh>
#include <spot/misc/common.hh>
#include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
#include <spot/mc/mc.hh>
namespace spot
{
......@@ -405,16 +406,6 @@ namespace spot
fixed_size_pool<pool_type::Unsafe> 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<State, SuccIterator>& sys,
iterable_uf<State, StateHash, StateEqual>& uf,
unsigned tid):
sys_(sys), uf_(uf), tid_(tid),
using uf = iterable_uf<State, StateHash, StateEqual>;
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<State, SuccIterator>& sys,
twacube_ptr, /* useless here */
shared_map& map, /* useless here */
iterable_uf<State, StateHash, StateEqual>* uf,
unsigned tid,
std::atomic<bool>& /*useless here*/):
sys_(sys), uf_(*uf), tid_(tid),
nb_th_(std::thread::hardware_concurrency())
{
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
......@@ -437,13 +443,9 @@ namespace spot
"error: does not match the kripkecube requirements");
}
using uf = iterable_uf<State, StateHash, StateEqual>;
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 "bloemen_scc";
}
int sccs()
{
return sccs_;
}
mc_rvalue result()
{
return mc_rvalue::SUCCESS;
}
std::string trace()
{
return {uf_.inserted(), states_, transitions_, sccs_, walltime()};
// Returning a trace has no sense in this algorithm
return "";
}
private:
......
// -*- 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 <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/mc/intersect.hh>
namespace spot
{
......@@ -100,7 +101,6 @@ namespace spot
using shared_map = brick::hashset::FastConcurrent <uf_element*,
uf_element_hasher>;
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<pool_type::Unsafe> 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<State, StateHash, StateEqual>;
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<State, SuccIterator>& sys,
twacube_ptr twa,
iterable_uf_ec<State, StateHash, StateEqual>& uf,
shared_map& map, /* useless here */
iterable_uf_ec<State, StateHash, StateEqual>* uf,
unsigned tid,
std::atomic<bool>& 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<State, StateHash, StateEqual>;
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<trans_index> it_prop,
bool just_pushed)
unsigned states()
{
SPOT_ASSERT(!(it_prop->done() &&
it_kripke->done()));
// 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();
return states_;
}
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 "bloemen_ec";
}
int sccs()
{
return is_empty_;
return sccs_;
}
bloemen_ec_stats stats()
mc_rvalue result()
{
return {uf_.inserted(), states_, transitions_, sccs_, is_empty_,
walltime()};
return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
}
std::string trace()
......
This diff is collapsed.
// -*- 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<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
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 <deadlock_pair*,
pair_hasher>;
using shared_struct = shared_map;
static shared_struct* make_shared_st(shared_map, unsigned)
{
return nullptr; // Useless
}
swarmed_deadlock(kripkecube<State, SuccIterator>& sys,
shared_map& map, unsigned tid, std::atomic<bool>& stop):
twacube_ptr, /* useless here */
shared_map& map, shared_struct* /* useless here */,
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()),
......@@ -106,6 +105,7 @@ namespace spot
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::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()
unsigned walltime()
{
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();
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
}
if (SPOT_LIKELY(push(dst)))
{
todo_.back().it->next();
todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
}
else
{
todo_.back().it->next();
}
}
}
finalize();
std::string name()
{
return "deadlock";
}
bool has_deadlock()
int sccs()
{
return deadlock_;
return -1;
}
unsigned walltime()
mc_rvalue result()
{
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
}
deadlock_stats stats()
std::string trace()
{
return {states(), transitions(), dfs_, has_deadlock(), walltime()};
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<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
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
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
// -*- 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <string>
#include <thread>
#include <vector>
#include <utility>
#include <spot/kripke/kripke.hh>
#include <spot/mc/mc.hh>
#include <spot/mc/ec.hh>
#include <spot/mc/deadlock.hh>
#include <spot/mc/cndfs.hh>
#include <spot/mc/bloemen.hh>
#include <spot/mc/bloemen_ec.hh>
#include <spot/misc/common.hh>
#include <spot/misc/timer.hh>
namespace spot
{
template<typename algo_name, typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
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<bool> stop(false);
unsigned nbth = sys->get_threads();
typename algo_name::shared_map map;
std::vector<algo_name*> swarmed(nbth);
// The shared structure requires sometime one instance per thread
using struct_name = typename algo_name::shared_struct;
std::vector<struct_name*> 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<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");
// 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;
}
}
}