45 enum class uf_status { LIVE, LOCK, DEAD };
46 enum class list_status { BUSY, LOCK, DONE };
47 enum class claim_status { CLAIM_FOUND, CLAIM_NEW, CLAIM_DEAD };
63 std::atomic<list_status> list_status_;
74 brick::hash::hash128_t
79 unsigned u = hash(lhs->
st_) % (1<<30);
87 return equal(lhs->
st_, rhs->
st_);
92 using shared_map = brick::hashset::FastConcurrent <
uf_element*,
96 map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
97 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
103 map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
104 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
105 p_(sizeof(uf_element))
111 std::pair<claim_status, uf_element*>
114 unsigned w_id = (1U << tid_);
117 uf_element* v = (uf_element*) p_.
allocate();
122 v->uf_status_ = uf_status::LIVE;
123 v->list_status_ = list_status::BUSY;
125 auto it = map_.insert({v});
135 uf_element* a_root = find(*it);
136 if (a_root->uf_status_.load() == uf_status::DEAD)
137 return {claim_status::CLAIM_DEAD, *it};
139 if ((a_root->worker_.load() & w_id) != 0)
140 return {claim_status::CLAIM_FOUND, *it};
142 atomic_fetch_or(&(a_root->worker_), w_id);
143 while (a_root->parent.load() != a_root)
145 a_root = find(a_root);
146 atomic_fetch_or(&(a_root->worker_), w_id);
149 return {claim_status::CLAIM_NEW, *it};
152 uf_element* find(uf_element* a)
154 uf_element* parent = a->parent.load();
161 parent = y->parent.load();
164 x->parent.store(parent);
166 parent = x->parent.load();
171 bool sameset(uf_element* a, uf_element* b)
175 uf_element* a_root = find(a);
176 uf_element* b_root = find(b);
177 if (a_root == b_root)
180 if (a_root->parent.load() == a_root)
185 bool lock_root(uf_element* a)
187 uf_status expected = uf_status::LIVE;
188 if (a->uf_status_.load() == expected)
190 if (std::atomic_compare_exchange_strong
191 (&(a->uf_status_), &expected, uf_status::LOCK))
193 if (a->parent.load() == a)
201 inline void unlock_root(uf_element* a)
203 a->uf_status_.store(uf_status::LIVE);
206 uf_element* lock_list(uf_element* a)
208 uf_element* a_list = a;
211 bool dontcare =
false;
212 a_list = pick_from_list(a_list, &dontcare);
213 if (a_list ==
nullptr)
218 auto expected = list_status::BUSY;
219 bool b = std::atomic_compare_exchange_strong
220 (&(a_list->list_status_), &expected, list_status::LOCK);
225 a_list = a_list->next_.load();
229 void unlock_list(uf_element* a)
231 a->list_status_.store(list_status::BUSY);
234 void unite(uf_element* a, uf_element* b)
246 if (a_root == b_root)
249 r = std::max(a_root, b_root);
250 q = std::min(a_root, b_root);
258 uf_element* a_list = lock_list(a);
259 if (a_list ==
nullptr)
265 uf_element* b_list = lock_list(b);
266 if (b_list ==
nullptr)
273 SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
274 SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
277 uf_element* a_next = a_list->next_.load();
278 uf_element* b_next = b_list->next_.load();
279 SPOT_ASSERT(a_next !=
nullptr);
280 SPOT_ASSERT(b_next !=
nullptr);
282 a_list->next_.store(b_next);
283 b_list->next_.store(a_next);
287 unsigned q_worker = q->worker_.load();
288 unsigned r_worker = r->worker_.load();
289 if ((q_worker|r_worker) != r_worker)
291 atomic_fetch_or(&(r->worker_), q_worker);
292 while (r->parent.load() != r)
295 atomic_fetch_or(&(r->worker_), q_worker);
304 uf_element* pick_from_list(uf_element* u,
bool* sccfound)
309 list_status a_status;
312 a_status = a->list_status_.load();
314 if (a_status == list_status::BUSY)
319 if (a_status == list_status::DONE)
323 uf_element* b = a->next_.load();
344 uf_element* a_root = find(u);
345 uf_status status = a_root->uf_status_.load();
346 while (status != uf_status::DEAD)
348 if (status == uf_status::LIVE)
349 *sccfound = std::atomic_compare_exchange_strong
350 (&(a_root->uf_status_), &status, uf_status::DEAD);
351 status = a_root->uf_status_.load();
356 list_status b_status;
359 b_status = b->list_status_.load();
361 if (b_status == list_status::BUSY)
366 if (b_status == list_status::DONE)
370 SPOT_ASSERT(b_status == list_status::DONE);
371 SPOT_ASSERT(a_status == list_status::DONE);
373 uf_element* c = b->next_.load();
379 void remove_from_list(uf_element* a)
383 list_status a_status = a->list_status_.load();
385 if (a_status == list_status::DONE)
388 if (a_status == list_status::BUSY)
389 std::atomic_compare_exchange_strong
390 (&(a->list_status_), &a_status, list_status::DONE);
400 iterable_uf() =
default;
407 fixed_size_pool<pool_type::Unsafe> p_;
426 using shared_map =
typename uf::shared_map;
428 static shared_struct* make_shared_structure(shared_map m,
unsigned i)
438 std::atomic<bool>& stop):
439 sys_(sys), uf_(*
uf), tid_(tid),
440 nb_th_(std::thread::hardware_concurrency()),
444 State, SuccIterator>::value,
445 "error: does not match the kripkecube requirements");
451 State init = sys_.initial(tid_);
452 auto pair = uf_.make_claim(init);
453 todo_.push_back(pair.second);
454 Rp_.push_back(pair.second);
457 while (!todo_.empty())
459 bloemen_recursive_start:
460 while (!stop_.load(std::memory_order_relaxed))
462 bool sccfound =
false;
463 uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
464 if (v_prime ==
nullptr)
471 auto it = sys_.succ(v_prime->st_, tid_);
474 auto w = uf_.make_claim(it->state());
477 if (w.first == uf::claim_status::CLAIM_NEW)
479 todo_.push_back(w.second);
480 Rp_.push_back(w.second);
482 sys_.recycle(it, tid_);
483 goto bloemen_recursive_start;
485 else if (w.first == uf::claim_status::CLAIM_FOUND)
487 while (!uf_.sameset(todo_.back(), w.second))
489 uf_element* r = Rp_.back();
491 uf_.unite(r, Rp_.back());
495 uf_.remove_from_list(v_prime);
496 sys_.recycle(it, tid_);
499 if (todo_.back() == Rp_.back())
508 tm_.
start(
"DFS thread " + std::to_string(tid_));
513 bool tst_val =
false;
515 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
518 tm_.
stop(
"DFS thread " + std::to_string(tid_));
531 unsigned transitions()
538 return tm_.
timer(
"DFS thread " + std::to_string(tid_)).
walltime();
543 return "bloemen_scc";
564 std::vector<uf_element*> todo_;
565 std::vector<uf_element*> Rp_;
569 unsigned inserted_ = 0;
570 unsigned states_ = 0;
571 unsigned transitions_ = 0;
574 std::atomic<bool>& stop_;
575 bool finisher_ =
false;