23#include <spot/bricks/brick-hashset>
28#include <spot/misc/common.hh>
29#include <spot/kripke/kripke.hh>
30#include <spot/misc/fixpool.hh>
31#include <spot/misc/timer.hh>
32#include <spot/twacube/twacube.hh>
33#include <spot/twacube/fwd.hh>
34#include <spot/mc/intersect.hh>
35#include <spot/mc/mc.hh>
39 template<
typename State,
46 enum class uf_status { LIVE, LOCK, DEAD };
47 enum class list_status { BUSY, LOCK, DONE };
48 enum class claim_status { CLAIM_FOUND, CLAIM_NEW, CLAIM_DEAD };
70 std::atomic<list_status> list_status_;
81 brick::hash::hash128_t
86 unsigned u = hash(lhs->
st_kripke) % (1<<30);
102 using shared_map = brick::hashset::FastConcurrent <
uf_element*,
106 map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
107 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
112 map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
113 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
114 p_(sizeof(uf_element))
119 std::pair<claim_status, uf_element*>
120 make_claim(State kripke,
unsigned prop)
122 unsigned w_id = (1U << tid_);
125 uf_element* v = (uf_element*) p_.
allocate();
126 new (v) (uf_element);
127 v->st_kripke = kripke;
133 v->uf_status_ = uf_status::LIVE;
134 v->list_status_ = list_status::BUSY;
136 auto it = map_.insert({v});
146 uf_element* a_root = find(*it);
147 if (a_root->uf_status_.load() == uf_status::DEAD)
148 return {claim_status::CLAIM_DEAD, *it};
150 if ((a_root->worker_.load() & w_id) != 0)
151 return {claim_status::CLAIM_FOUND, *it};
153 atomic_fetch_or(&(a_root->worker_), w_id);
154 while (a_root->parent.load() != a_root)
156 a_root = find(a_root);
157 atomic_fetch_or(&(a_root->worker_), w_id);
160 return {claim_status::CLAIM_NEW, *it};
163 uf_element* find(uf_element* a)
165 uf_element* parent = a->parent.load();
172 parent = y->parent.load();
175 x->parent.store(parent);
177 parent = x->parent.load();
182 bool sameset(uf_element* a, uf_element* b)
186 uf_element* a_root = find(a);
187 uf_element* b_root = find(b);
188 if (a_root == b_root)
191 if (a_root->parent.load() == a_root)
196 bool lock_root(uf_element* a)
198 uf_status expected = uf_status::LIVE;
199 if (a->uf_status_.load() == expected)
201 if (std::atomic_compare_exchange_strong
202 (&(a->uf_status_), &expected, uf_status::LOCK))
204 if (a->parent.load() == a)
212 inline void unlock_root(uf_element* a)
214 a->uf_status_.store(uf_status::LIVE);
217 uf_element* lock_list(uf_element* a)
219 uf_element* a_list = a;
222 bool dontcare =
false;
223 a_list = pick_from_list(a_list, &dontcare);
224 if (a_list ==
nullptr)
229 auto expected = list_status::BUSY;
230 bool b = std::atomic_compare_exchange_strong
231 (&(a_list->list_status_), &expected, list_status::LOCK);
236 a_list = a_list->next_.load();
240 void unlock_list(uf_element* a)
242 a->list_status_.store(list_status::BUSY);
246 unite(uf_element* a, uf_element* b, acc_cond::mark_t acc)
258 if (a_root == b_root)
262 std::lock_guard<std::mutex> rlock(a_root->acc_mutex_);
267 while (a_root->parent.load() != a_root)
269 a_root = find(a_root);
270 std::lock_guard<std::mutex> rlock(a_root->acc_mutex_);
277 r = std::max(a_root, b_root);
278 q = std::min(a_root, b_root);
280 while (!lock_root(q));
282 uf_element* a_list = lock_list(a);
283 if (a_list ==
nullptr)
289 uf_element* b_list = lock_list(b);
290 if (b_list ==
nullptr)
297 SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
298 SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
301 uf_element* a_next = a_list->next_.load();
302 uf_element* b_next = b_list->next_.load();
303 SPOT_ASSERT(a_next !=
nullptr);
304 SPOT_ASSERT(b_next !=
nullptr);
306 a_list->next_.store(b_next);
307 b_list->next_.store(a_next);
311 unsigned q_worker = q->worker_.load();
312 unsigned r_worker = r->worker_.load();
313 if ((q_worker|r_worker) != r_worker)
315 atomic_fetch_or(&(r->worker_), q_worker);
316 while (r->parent.load() != r)
319 atomic_fetch_or(&(r->worker_), q_worker);
325 std::lock_guard<std::mutex> rlock(r->acc_mutex_);
326 std::lock_guard<std::mutex> qlock(q->acc_mutex_);
327 acc |= r->acc | q->acc;
328 r->acc = q->acc = acc;
331 while (r->parent.load() != r)
334 std::lock_guard<std::mutex> rlock(r->acc_mutex_);
335 std::lock_guard<std::mutex> qlock(q->acc_mutex_);
336 acc |= r->acc | q->acc;
346 uf_element* pick_from_list(uf_element* u,
bool* sccfound)
351 list_status a_status;
354 a_status = a->list_status_.load();
356 if (a_status == list_status::BUSY)
359 if (a_status == list_status::DONE)
363 uf_element* b = a->next_.load();
384 uf_element* a_root = find(u);
385 uf_status status = a_root->uf_status_.load();
386 while (status != uf_status::DEAD)
388 if (status == uf_status::LIVE)
389 *sccfound = std::atomic_compare_exchange_strong
390 (&(a_root->uf_status_), &status, uf_status::DEAD);
391 status = a_root->uf_status_.load();
396 list_status b_status;
399 b_status = b->list_status_.load();
401 if (b_status == list_status::BUSY)
404 if (b_status == list_status::DONE)
408 SPOT_ASSERT(b_status == list_status::DONE);
409 SPOT_ASSERT(a_status == list_status::DONE);
411 uf_element* c = b->next_.load();
417 void remove_from_list(uf_element* a)
421 list_status a_status = a->list_status_.load();
423 if (a_status == list_status::DONE)
426 if (a_status == list_status::BUSY)
427 std::atomic_compare_exchange_strong
428 (&(a->list_status_), &a_status, list_status::DONE);
438 iterable_uf_ec() =
default;
445 fixed_size_pool<pool_type::Unsafe> p_;
451 template<
typename State,
typename SuccIterator,
452 typename StateHash,
typename StateEqual>
463 using shared_map =
typename uf::shared_map;
465 static shared_struct* make_shared_structure(shared_map m,
unsigned i)
475 std::atomic<bool>& stop):
476 sys_(sys), twa_(
twa), uf_(*
uf), tid_(tid),
477 nb_th_(std::thread::hardware_concurrency()),
481 State, SuccIterator>::value,
482 "error: does not match the kripkecube requirements");
490 State init_kripke = sys_.initial(tid_);
491 unsigned init_twa = twa_->get_initial();
492 auto pair = uf_.make_claim(init_kripke, init_twa);
493 todo_.push_back(pair.second);
494 Rp_.push_back(pair.second);
497 while (!todo_.empty())
499 bloemen_recursive_start:
500 while (!stop_.load(std::memory_order_relaxed))
502 bool sccfound =
false;
503 uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
504 if (v_prime ==
nullptr)
511 auto it_kripke = sys_.succ(v_prime->st_kripke, tid_);
512 auto it_prop = twa_->succ(v_prime->st_prop);
513 forward_iterators(sys_, twa_, it_kripke, it_prop,
true, tid_);
514 while (!it_kripke->done())
516 auto w = uf_.make_claim(it_kripke->state(),
517 twa_->trans_storage(it_prop, tid_)
519 auto trans_acc = twa_->trans_storage(it_prop, tid_).acc_;
521 if (w.first == uf::claim_status::CLAIM_NEW)
523 todo_.push_back(w.second);
524 Rp_.push_back(w.second);
526 sys_.recycle(it_kripke, tid_);
527 goto bloemen_recursive_start;
529 else if (w.first == uf::claim_status::CLAIM_FOUND)
537 scc_acc |= uf_.unite(w.second, w.second, scc_acc);
539 while (!uf_.sameset(todo_.back(), w.second))
541 uf_element* r = Rp_.back();
543 uf_.unite(r, Rp_.back(), scc_acc);
548 auto root = uf_.find(w.second);
549 std::lock_guard<std::mutex> lock(root->acc_mutex_);
554 if (twa_->acc().accepting(scc_acc))
556 sys_.recycle(it_kripke, tid_);
559 tm_.
stop(
"DFS thread " + std::to_string(tid_));
563 forward_iterators(sys_, twa_, it_kripke, it_prop,
566 uf_.remove_from_list(v_prime);
567 sys_.recycle(it_kripke, tid_);
570 if (todo_.back() == Rp_.back())
579 tm_.
start(
"DFS thread " + std::to_string(tid_));
584 bool tst_val =
false;
586 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
589 tm_.
stop(
"DFS thread " + std::to_string(tid_));
602 unsigned transitions()
609 return tm_.
timer(
"DFS thread " + std::to_string(tid_)).
walltime();
629 return "Not implemented";
635 std::vector<uf_element*> todo_;
636 std::vector<uf_element*> Rp_;
640 unsigned inserted_ = 0;
641 unsigned states_ = 0;
642 unsigned transitions_ = 0;
644 bool is_empty_ =
true;
646 std::atomic<bool>& stop_;
647 bool finisher_ =
false;
void deallocate(void *ptr)
Recycle size bytes of memory.
Definition: fixpool.hh:132
void * allocate()
Allocate size bytes of memory.
Definition: fixpool.hh:88
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
Definition: bloemen_ec.hh:43
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16....
Definition: bloemen_ec.hh:454
A map of timer, where each timer has a name.
Definition: timer.hh:225
void stop(const std::string &name)
Stop timer name.
Definition: timer.hh:245
void start(const std::string &name)
Start a timer with name name.
Definition: timer.hh:234
const spot::timer & timer(const std::string &name) const
Return the timer name.
Definition: timer.hh:270
std::chrono::milliseconds::rep walltime() const
Return cumulative wall time.
Definition: timer.hh:203
A Transition-based ω-Automaton.
Definition: twa.hh:619
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.
An acceptance mark.
Definition: acc.hh:84
The hasher for the previous uf_element. Shortcut to ease shared map manipulation.
Definition: bloemen_ec.hh:75
Represents a Union-Find element.
Definition: bloemen_ec.hh:52
State st_kripke
the kripke state handled by the element
Definition: bloemen_ec.hh:54
std::mutex acc_mutex_
mutex for acceptance condition
Definition: bloemen_ec.hh:60
std::atomic< uf_element * > parent
reference to the pointer
Definition: bloemen_ec.hh:62
std::atomic< unsigned > worker_
The set of worker for a given state.
Definition: bloemen_ec.hh:64
unsigned st_prop
the prop state handled by the element
Definition: bloemen_ec.hh:56
acc_cond::mark_t acc
acceptance conditions of the union
Definition: bloemen_ec.hh:58
std::atomic< uf_status > uf_status_
current status for the element
Definition: bloemen_ec.hh:68
std::atomic< uf_element * > next_
next element for work stealing
Definition: bloemen_ec.hh:66