24 #include <spot/bricks/brick-hashset>
29 #include <spot/misc/common.hh>
30 #include <spot/kripke/kripke.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/intersect.hh>
36 #include <spot/mc/mc.hh>
40 template<
typename State,
47 enum class uf_status { LIVE, LOCK, DEAD };
48 enum class list_status { BUSY, LOCK, DONE };
49 enum class claim_status { CLAIM_FOUND, CLAIM_NEW, CLAIM_DEAD };
71 std::atomic<list_status> list_status_;
82 brick::hash::hash128_t
87 unsigned u = hash(lhs->
st_kripke) % (1<<30);
103 using shared_map = brick::hashset::FastConcurrent <
uf_element*,
107 map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
108 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
113 map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
114 nb_th_(std::thread::hardware_concurrency()), inserted_(0),
115 p_(sizeof(uf_element))
120 std::pair<claim_status, uf_element*>
121 make_claim(State kripke,
unsigned prop)
123 unsigned w_id = (1U << tid_);
126 uf_element* v = (uf_element*) p_.
allocate();
127 new (v) (uf_element);
128 v->st_kripke = kripke;
134 v->uf_status_ = uf_status::LIVE;
135 v->list_status_ = list_status::BUSY;
137 auto it = map_.insert({v});
147 uf_element* a_root = find(*it);
148 if (a_root->uf_status_.load() == uf_status::DEAD)
149 return {claim_status::CLAIM_DEAD, *it};
151 if ((a_root->worker_.load() & w_id) != 0)
152 return {claim_status::CLAIM_FOUND, *it};
154 atomic_fetch_or(&(a_root->worker_), w_id);
155 while (a_root->parent.load() != a_root)
157 a_root = find(a_root);
158 atomic_fetch_or(&(a_root->worker_), w_id);
161 return {claim_status::CLAIM_NEW, *it};
164 uf_element* find(uf_element* a)
166 uf_element* parent = a->parent.load();
173 parent = y->parent.load();
176 x->parent.store(parent);
178 parent = x->parent.load();
183 bool sameset(uf_element* a, uf_element* b)
187 uf_element* a_root = find(a);
188 uf_element* b_root = find(b);
189 if (a_root == b_root)
192 if (a_root->parent.load() == a_root)
197 bool lock_root(uf_element* a)
199 uf_status expected = uf_status::LIVE;
200 if (a->uf_status_.load() == expected)
202 if (std::atomic_compare_exchange_strong
203 (&(a->uf_status_), &expected, uf_status::LOCK))
205 if (a->parent.load() == a)
213 inline void unlock_root(uf_element* a)
215 a->uf_status_.store(uf_status::LIVE);
218 uf_element* lock_list(uf_element* a)
220 uf_element* a_list = a;
223 bool dontcare =
false;
224 a_list = pick_from_list(a_list, &dontcare);
225 if (a_list ==
nullptr)
230 auto expected = list_status::BUSY;
231 bool b = std::atomic_compare_exchange_strong
232 (&(a_list->list_status_), &expected, list_status::LOCK);
237 a_list = a_list->next_.load();
241 void unlock_list(uf_element* a)
243 a->list_status_.store(list_status::BUSY);
247 unite(uf_element* a, uf_element* b, acc_cond::mark_t acc)
259 if (a_root == b_root)
263 std::lock_guard<std::mutex> rlock(a_root->acc_mutex_);
268 while (a_root->parent.load() != a_root)
270 a_root = find(a_root);
271 std::lock_guard<std::mutex> rlock(a_root->acc_mutex_);
278 r = std::max(a_root, b_root);
279 q = std::min(a_root, b_root);
281 while (!lock_root(q));
283 uf_element* a_list = lock_list(a);
284 if (a_list ==
nullptr)
290 uf_element* b_list = lock_list(b);
291 if (b_list ==
nullptr)
298 SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
299 SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
302 uf_element* a_next = a_list->next_.load();
303 uf_element* b_next = b_list->next_.load();
304 SPOT_ASSERT(a_next !=
nullptr);
305 SPOT_ASSERT(b_next !=
nullptr);
307 a_list->next_.store(b_next);
308 b_list->next_.store(a_next);
312 unsigned q_worker = q->worker_.load();
313 unsigned r_worker = r->worker_.load();
314 if ((q_worker|r_worker) != r_worker)
316 atomic_fetch_or(&(r->worker_), q_worker);
317 while (r->parent.load() != r)
320 atomic_fetch_or(&(r->worker_), q_worker);
326 std::lock_guard<std::mutex> rlock(r->acc_mutex_);
327 std::lock_guard<std::mutex> qlock(q->acc_mutex_);
328 acc |= r->acc | q->acc;
329 r->acc = q->acc = acc;
332 while (r->parent.load() != r)
335 std::lock_guard<std::mutex> rlock(r->acc_mutex_);
336 std::lock_guard<std::mutex> qlock(q->acc_mutex_);
337 acc |= r->acc | q->acc;
347 uf_element* pick_from_list(uf_element* u,
bool* sccfound)
352 list_status a_status;
355 a_status = a->list_status_.load();
357 if (a_status == list_status::BUSY)
360 if (a_status == list_status::DONE)
364 uf_element* b = a->next_.load();
385 uf_element* a_root = find(u);
386 uf_status status = a_root->uf_status_.load();
387 while (status != uf_status::DEAD)
389 if (status == uf_status::LIVE)
390 *sccfound = std::atomic_compare_exchange_strong
391 (&(a_root->uf_status_), &status, uf_status::DEAD);
392 status = a_root->uf_status_.load();
397 list_status b_status;
400 b_status = b->list_status_.load();
402 if (b_status == list_status::BUSY)
405 if (b_status == list_status::DONE)
409 SPOT_ASSERT(b_status == list_status::DONE);
410 SPOT_ASSERT(a_status == list_status::DONE);
412 uf_element* c = b->next_.load();
418 void remove_from_list(uf_element* a)
422 list_status a_status = a->list_status_.load();
424 if (a_status == list_status::DONE)
427 if (a_status == list_status::BUSY)
428 std::atomic_compare_exchange_strong
429 (&(a->list_status_), &a_status, list_status::DONE);
439 iterable_uf_ec() =
default;
446 fixed_size_pool<pool_type::Unsafe> p_;
452 template<
typename State,
typename SuccIterator,
453 typename StateHash,
typename StateEqual>
464 using shared_map =
typename uf::shared_map;
466 static shared_struct* make_shared_structure(shared_map m,
unsigned i)
476 std::atomic<bool>& stop):
477 sys_(sys), twa_(
twa), uf_(*
uf), tid_(tid),
478 nb_th_(std::thread::hardware_concurrency()),
482 State, SuccIterator>::value,
483 "error: does not match the kripkecube requirements");
491 State init_kripke = sys_.initial(tid_);
492 unsigned init_twa = twa_->get_initial();
493 auto pair = uf_.make_claim(init_kripke, init_twa);
494 todo_.push_back(pair.second);
495 Rp_.push_back(pair.second);
498 while (!todo_.empty())
500 bloemen_recursive_start:
501 while (!stop_.load(std::memory_order_relaxed))
503 bool sccfound =
false;
504 uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
505 if (v_prime ==
nullptr)
512 auto it_kripke = sys_.succ(v_prime->st_kripke, tid_);
513 auto it_prop = twa_->succ(v_prime->st_prop);
514 forward_iterators(sys_, twa_, it_kripke, it_prop,
true, tid_);
515 while (!it_kripke->done())
517 auto w = uf_.make_claim(it_kripke->state(),
518 twa_->trans_storage(it_prop, tid_)
520 auto trans_acc = twa_->trans_storage(it_prop, tid_).acc_;
522 if (w.first == uf::claim_status::CLAIM_NEW)
524 todo_.push_back(w.second);
525 Rp_.push_back(w.second);
527 sys_.recycle(it_kripke, tid_);
528 goto bloemen_recursive_start;
530 else if (w.first == uf::claim_status::CLAIM_FOUND)
538 scc_acc |= uf_.unite(w.second, w.second, scc_acc);
540 while (!uf_.sameset(todo_.back(), w.second))
542 uf_element* r = Rp_.back();
544 uf_.unite(r, Rp_.back(), scc_acc);
549 auto root = uf_.find(w.second);
550 std::lock_guard<std::mutex> lock(root->acc_mutex_);
555 if (twa_->acc().accepting(scc_acc))
557 sys_.recycle(it_kripke, tid_);
560 tm_.
stop(
"DFS thread " + std::to_string(tid_));
564 forward_iterators(sys_, twa_, it_kripke, it_prop,
567 uf_.remove_from_list(v_prime);
568 sys_.recycle(it_kripke, tid_);
571 if (todo_.back() == Rp_.back())
580 tm_.
start(
"DFS thread " + std::to_string(tid_));
585 bool tst_val =
false;
587 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
590 tm_.
stop(
"DFS thread " + std::to_string(tid_));
603 unsigned transitions()
610 return tm_.
timer(
"DFS thread " + std::to_string(tid_)).
walltime();
630 return "Not implemented";
636 std::vector<uf_element*> todo_;
637 std::vector<uf_element*> Rp_;
641 unsigned inserted_ = 0;
642 unsigned states_ = 0;
643 unsigned transitions_ = 0;
645 bool is_empty_ =
true;
647 std::atomic<bool>& stop_;
648 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_ec.hh:44
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_ec.hh:455
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
A Transition-based ω-Automaton.
Definition: twa.hh:623
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:41
Definition: automata.hh:27
mc_rvalue
Definition: mc.hh:44
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.
An acceptance mark.
Definition: acc.hh:85
The haser for the previous uf_element. Shortcut to ease shared map manipulation.
Definition: bloemen_ec.hh:76
Represents a Union-Find element.
Definition: bloemen_ec.hh:53
State st_kripke
the kripke state handled by the element
Definition: bloemen_ec.hh:55
std::mutex acc_mutex_
mutex for acceptance condition
Definition: bloemen_ec.hh:61
std::atomic< uf_element * > parent
reference to the pointer
Definition: bloemen_ec.hh:63
std::atomic< unsigned > worker_
The set of worker for a given state.
Definition: bloemen_ec.hh:65
unsigned st_prop
the prop state handled by the element
Definition: bloemen_ec.hh:57
acc_cond::mark_t acc
acceptance conditions of the union
Definition: bloemen_ec.hh:59
std::atomic< uf_status > uf_status_
current status for the element
Definition: bloemen_ec.hh:69
std::atomic< uf_element * > next_
next element for work stealing
Definition: bloemen_ec.hh:67