28 #include <spot/bricks/brick-hashset>
29 #include <spot/kripke/kripke.hh>
30 #include <spot/misc/common.hh>
31 #include <spot/misc/fixpool.hh>
32 #include <spot/misc/timer.hh>
33 #include <spot/twacube/twacube.hh>
34 #include <spot/twacube/fwd.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 };
64 std::atomic<list_status> list_status_;
75 brick::hash::hash128_t
80 unsigned u = hash(lhs->
st_) % (1<<30);
88 return equal(lhs->
st_, rhs->
st_);
93 using shared_map = brick::hashset::FastConcurrent <
uf_element*,
97 map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
98 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
104 map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
105 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
106 p_(sizeof(uf_element))
112 std::pair<claim_status, uf_element*>
115 unsigned w_id = (1U << tid_);
118 uf_element* v = (uf_element*) p_.
allocate();
123 v->uf_status_ = uf_status::LIVE;
124 v->list_status_ = list_status::BUSY;
126 auto it = map_.insert({v});
136 uf_element* a_root = find(*it);
137 if (a_root->uf_status_.load() == uf_status::DEAD)
138 return {claim_status::CLAIM_DEAD, *it};
140 if ((a_root->worker_.load() & w_id) != 0)
141 return {claim_status::CLAIM_FOUND, *it};
143 atomic_fetch_or(&(a_root->worker_), w_id);
144 while (a_root->parent.load() != a_root)
146 a_root = find(a_root);
147 atomic_fetch_or(&(a_root->worker_), w_id);
150 return {claim_status::CLAIM_NEW, *it};
153 uf_element* find(uf_element* a)
155 uf_element* parent = a->parent.load();
162 parent = y->parent.load();
165 x->parent.store(parent);
167 parent = x->parent.load();
172 bool sameset(uf_element* a, uf_element* b)
176 uf_element* a_root = find(a);
177 uf_element* b_root = find(b);
178 if (a_root == b_root)
181 if (a_root->parent.load() == a_root)
186 bool lock_root(uf_element* a)
188 uf_status expected = uf_status::LIVE;
189 if (a->uf_status_.load() == expected)
191 if (std::atomic_compare_exchange_strong
192 (&(a->uf_status_), &expected, uf_status::LOCK))
194 if (a->parent.load() == a)
202 inline void unlock_root(uf_element* a)
204 a->uf_status_.store(uf_status::LIVE);
207 uf_element* lock_list(uf_element* a)
209 uf_element* a_list = a;
212 bool dontcare =
false;
213 a_list = pick_from_list(a_list, &dontcare);
214 if (a_list ==
nullptr)
219 auto expected = list_status::BUSY;
220 bool b = std::atomic_compare_exchange_strong
221 (&(a_list->list_status_), &expected, list_status::LOCK);
226 a_list = a_list->next_.load();
230 void unlock_list(uf_element* a)
232 a->list_status_.store(list_status::BUSY);
235 void unite(uf_element* a, uf_element* b)
247 if (a_root == b_root)
250 r = std::max(a_root, b_root);
251 q = std::min(a_root, b_root);
259 uf_element* a_list = lock_list(a);
260 if (a_list ==
nullptr)
266 uf_element* b_list = lock_list(b);
267 if (b_list ==
nullptr)
274 SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
275 SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
278 uf_element* a_next = a_list->next_.load();
279 uf_element* b_next = b_list->next_.load();
280 SPOT_ASSERT(a_next !=
nullptr);
281 SPOT_ASSERT(b_next !=
nullptr);
283 a_list->next_.store(b_next);
284 b_list->next_.store(a_next);
288 unsigned q_worker = q->worker_.load();
289 unsigned r_worker = r->worker_.load();
290 if ((q_worker|r_worker) != r_worker)
292 atomic_fetch_or(&(r->worker_), q_worker);
293 while (r->parent.load() != r)
296 atomic_fetch_or(&(r->worker_), q_worker);
305 uf_element* pick_from_list(uf_element* u,
bool* sccfound)
310 list_status a_status;
313 a_status = a->list_status_.load();
315 if (a_status == list_status::BUSY)
320 if (a_status == list_status::DONE)
324 uf_element* b = a->next_.load();
345 uf_element* a_root = find(u);
346 uf_status status = a_root->uf_status_.load();
347 while (status != uf_status::DEAD)
349 if (status == uf_status::LIVE)
350 *sccfound = std::atomic_compare_exchange_strong
351 (&(a_root->uf_status_), &status, uf_status::DEAD);
352 status = a_root->uf_status_.load();
357 list_status b_status;
360 b_status = b->list_status_.load();
362 if (b_status == list_status::BUSY)
367 if (b_status == list_status::DONE)
371 SPOT_ASSERT(b_status == list_status::DONE);
372 SPOT_ASSERT(a_status == list_status::DONE);
374 uf_element* c = b->next_.load();
380 void remove_from_list(uf_element* a)
384 list_status a_status = a->list_status_.load();
386 if (a_status == list_status::DONE)
389 if (a_status == list_status::BUSY)
390 std::atomic_compare_exchange_strong
391 (&(a->list_status_), &a_status, list_status::DONE);
401 iterable_uf() =
default;
408 fixed_size_pool<pool_type::Unsafe> p_;
414 template<
typename State,
typename SuccIterator,
415 typename StateHash,
typename StateEqual>
427 using shared_map =
typename uf::shared_map;
429 static shared_struct* make_shared_structure(shared_map m,
unsigned i)
439 std::atomic<bool>& stop):
440 sys_(sys), uf_(*
uf), tid_(tid),
441 nb_th_(std::thread::hardware_concurrency()),
445 State, SuccIterator>::value,
446 "error: does not match the kripkecube requirements");
452 State init = sys_.initial(tid_);
453 auto pair = uf_.make_claim(init);
454 todo_.push_back(pair.second);
455 Rp_.push_back(pair.second);
458 while (!todo_.empty())
460 bloemen_recursive_start:
461 while (!stop_.load(std::memory_order_relaxed))
463 bool sccfound =
false;
464 uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
465 if (v_prime ==
nullptr)
472 auto it = sys_.succ(v_prime->st_, tid_);
475 auto w = uf_.make_claim(it->state());
478 if (w.first == uf::claim_status::CLAIM_NEW)
480 todo_.push_back(w.second);
481 Rp_.push_back(w.second);
483 sys_.recycle(it, tid_);
484 goto bloemen_recursive_start;
486 else if (w.first == uf::claim_status::CLAIM_FOUND)
488 while (!uf_.sameset(todo_.back(), w.second))
490 uf_element* r = Rp_.back();
492 uf_.unite(r, Rp_.back());
496 uf_.remove_from_list(v_prime);
497 sys_.recycle(it, tid_);
500 if (todo_.back() == Rp_.back())
509 tm_.
start(
"DFS thread " + std::to_string(tid_));
514 bool tst_val =
false;
516 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
519 tm_.
stop(
"DFS thread " + std::to_string(tid_));
532 unsigned transitions()
539 return tm_.
timer(
"DFS thread " + std::to_string(tid_)).
walltime();
544 return "bloemen_scc";
565 std::vector<uf_element*> todo_;
566 std::vector<uf_element*> Rp_;
570 unsigned inserted_ = 0;
571 unsigned states_ = 0;
572 unsigned transitions_ = 0;
575 std::atomic<bool>& stop_;
576 bool finisher_ =
false;
void * allocate()
Allocate size bytes of memory.
Definition: fixpool.hh:89
void deallocate(void *ptr)
Recycle size bytes of memory.
Definition: fixpool.hh:133
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:72
Definition: bloemen.hh:43
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16....
Definition: bloemen.hh:417
A map of timer, where each timer has a name.
Definition: timer.hh:229
void stop(const std::string &name)
Stop timer name.
Definition: timer.hh:249
void start(const std::string &name)
Start a timer with name name.
Definition: timer.hh:238
const spot::timer & timer(const std::string &name) const
Return the timer name.
Definition: timer.hh:274
std::chrono::milliseconds::rep walltime() const
Return cumulative wall time.
Definition: timer.hh:207
Definition: automata.hh:27
mc_rvalue
Definition: mc.hh:44
@ SUCCESS
The Algorithm finished normally.
The haser for the previous uf_element. Shortcut to ease shared map manipulation.
Definition: bloemen.hh:69
Represents a Union-Find element.
Definition: bloemen.hh:52
std::atomic< unsigned > worker_
The set of worker for a given state.
Definition: bloemen.hh:58
State st_
the state handled by the element
Definition: bloemen.hh:54
std::atomic< uf_element * > parent
reference to the pointer
Definition: bloemen.hh:56
std::atomic< uf_element * > next_
next element for work stealing
Definition: bloemen.hh:60
std::atomic< uf_status > uf_status_
current status for the element
Definition: bloemen.hh:62